Bargmann invariant

One phase survives every convention: multiply three overlaps around a cycle. It is also the fingerprint that tells unitary from anti-unitary.

proved in corpus · proved here, no imported axiomsLean exists_continuous_phase_trivialisation

In plain terms

Here is the problem. A quantum state's overall phase is pure convention -- multiply by any unit complex number and no measurement changes. So phases seem like bookkeeping trash. Yet somehow geometric phases are measurable physics. Which phases are real?

Bargmann's invariant is the minimal answer. Take three states. Multiply their overlaps around the cycle: one to two, two to three, three back to one. Each state's arbitrary phase enters that product once plainly and once conjugated -- and cancels. What remains survives every convention. It is the smallest phase that is genuinely there.

It is the ancestor of every geometric phase: carry a state slowly around a loop and the extra phase it picks up is this invariant, iterated around the loop's edges.

In CSD

The corpus uses it as a fingerprint in the Wigner analysis. Symmetries come in two families -- unitary and anti-unitary -- and the invariant tells them apart: unitaries preserve it, anti-unitaries conjugate it. That is what lets the branch alternative in the rigidity theorem be decided pointwise instead of assumed.

Bargmann's THEOREM is a separate thing, and the corpus now gets what it needs from it without proving it. The theorem says continuity kills the projective cocycle, so projective representations lift to genuine ones. In general that is hard. But the corpus only ever needs it for a ONE-PARAMETER group, and there the obstruction is not hard -- it is absent.

The proof is three moves. Take determinants, which turns N unknown phases into one number on the circle. Lift that through the exponential, which works because the real line is simply connected and has no loops to obstruct you. What is left over is an Nth root of unity varying continuously on a connected space, so it cannot vary at all. Rescale it away. The coboundary datum the phase lift used to carry as a hypothesis is now discharged, and with the finite-dimensional Stone theorem beside it, continuity of the flow alone delivers Schrodinger evolution.

Mathematically

For rays u, v, w: the invariant is the phase of the product of pairwise overlaps around the cycle. Invariant under independent rescaling of each representative -- each scale factor appears once and once conjugated. Preserved by unitaries, conjugated by anti-unitaries, which is exactly the discriminator the rigidity proof needs.

The one-parameter lift is a separate statement, proved in the corpus: `exists_continuous_phase_trivialisation`. Given a continuous U with U(s+t) = c(s,t) U(s) U(t), it produces a continuous unit-modulus b with c(s,t) b(s+t) = b(s) b(t). Determinants give d(s+t) = c(s,t)^N d(s) d(t) on the circle; the covering lift through `Circle.exp` gives a continuous theta with d = exp(i theta); b0 = exp(-i theta / N) then leaves a residual with Nth power one, constant by connectedness, and absorbed by rescaling. Foundational triple only.

The name

Valentine Bargmann (1908-1989) was born in Berlin, left in 1933 when the dismissals began, and finished his doctorate in Zurich under Wentzel and Pauli. Emigrating in 1937, he landed at the Institute for Advanced Study as Einstein's assistant -- calculating with the great man daily -- then joined the Princeton faculty for good.

The 1954 paper on projective representations answered the question Wigner's theorem leaves open: the theorem hands you a symmetry with an undetermined phase; Bargmann settled when the phases can all be chosen consistently. He also worked out Lorentz- group representations with Wigner, and was by all accounts a concert-grade pianist who had considered the other career.

Module
CsdLean4/Mathlib/Analysis/Matrix/ProjectiveLift.lean
Background
Overview and history
Referenced
Wikipedia

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy