One phase survives every change of convention, the phase of the product of three overlaps taken around a cycle, and it's also the fingerprint that tells a unitary symmetry from an anti-unitary one.
exists_continuous_phase_trivialisationA quantum state is described by a list of complex numbers, its amplitudes. A complex number has a size and a direction, and the direction is called its phase. If you multiply every amplitude of a state by the same complex number of size one, which rotates all the phases by the same angle, no measurement on that state changes, so the overall phase of a state is pure convention and phases look like bookkeeping to be discarded. Yet geometric phases, the phases a state picks up when it's carried around a loop, are measurable physics, so you can ask which phases are real.
Bargmann's invariant is the minimal answer. Any two states have an overlap, a complex number that records how much they resemble each other, and its size fixes how easily the two states can be confused while its phase depends on the conventions chosen for both. Take three states and multiply their overlaps around the cycle, first to second, second to third, third back to first. Each state's arbitrary phase enters that product twice, once as itself and once with its sign reversed, so the two appearances cancel and what remains is independent of every convention. It's the smallest phase that's genuinely there.
This is the ancestor of every geometric phase. Carry a state slowly around a loop and the extra phase it acquires is this invariant, applied step by step along the edges of the loop.
The corpus uses the invariant as a fingerprint in its Wigner analysis. A symmetry of quantum mechanics is a transformation of states that preserves every measurement probability, and Wigner's theorem says such symmetries come in exactly two families, the unitary ones, which preserve phases, and the anti-unitary ones, which reverse them, as time reversal does. The invariant tells the families apart, because unitaries leave it unchanged while anti-unitaries reverse it, and that's what lets the choice between the two branches in the rigidity theorem be decided at each point rather than assumed.
Bargmann's theorem is a separate result, and the corpus gets what it needs from it without proving the general case. Wigner's theorem hands you each symmetry with an undetermined phase, and when two symmetries are applied in succession the phases needn't match up, so the mismatch is a leftover factor that can spoil any attempt to assign one consistent phase to every symmetry. Bargmann's theorem says continuity removes the leftover, so a family of symmetries defined only up to phase lifts to a genuine family with consistent phases. In general that's hard to prove. The corpus only ever needs it for a one-parameter group, a family of symmetries labelled by a single continuous number such as time, and there the obstruction isn't merely surmountable but absent.
The reason is that the real line has no loops. Any continuous phase along it can be unwound without obstruction, and the only freedom left over is a quantity that can take finitely many values yet must vary continuously, so it can't vary at all and is absorbed by a rescaling. The consequence for the programme is that a phase consistency condition which would otherwise have to be assumed is proved instead. Together with the finite-dimensional Stone theorem, which turns a continuous one- parameter family of unitary symmetries into a Hamiltonian generator, this means continuity of the flow alone delivers Schrodinger evolution.
For rays u, v, w the invariant is the phase of the product of pairwise overlaps around the cycle. It's invariant under independent rescaling of each representative, since each scale factor appears once plainly and once conjugated, and it's preserved by unitaries and 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 as `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), and b0 = exp(-i theta / N) then leaves a residual with Nth power one, which is constant by connectedness and absorbed by rescaling. The coboundary datum is thereby discharged rather than carried as a hypothesis of the phase lift, and the proof depends only on the foundational axiom triple.
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. He emigrated in 1937 and joined the Institute for Advanced Study as Einstein's assistant, working with him daily, before moving to the Princeton faculty for the rest of his career.
His 1954 paper on projective representations answered the question Wigner's theorem leaves open, as the theorem hands you a symmetry with an undetermined phase and Bargmann settled when the phases can all be chosen consistently. He also worked out representations of the Lorentz group with Wigner, and he was by all accounts a concert-grade pianist who had considered the other career.
CsdLean4/Mathlib/Analysis/Matrix/ProjectiveLift.leanSource 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.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.