U1_identity
plain-language theorem explainer
The U(1) gauge transformation with zero phase angle coincides with the identity map on complex fields. Researchers deriving gauge symmetries from ledger redundancy cite this as the neutral element required for the U(1) group. The proof applies function extensionality followed by simplification using the exponential at zero.
Claim. The U(1) transformation with phase angle zero equals the identity map: $U_1(0)(z) = z$ for all $z$ in the complex plane, where $U_1(θ)(z) := z · e^{iθ}$.
background
The QFT.GaugeInvariance module derives gauge invariance from ledger redundancy, where distinct representations encode identical physical states. The U(1) transformation is defined by pointwise multiplication with the complex phase factor $e^{iθ}$. Upstream identity morphisms appear in CostAlgebra, ArithmeticOf, and Octave, each supplying the neutral element for their respective algebraic structures.
proof idea
Function extensionality reduces the equality of maps to pointwise identity. Simplification then invokes the definition of U1Transform together with the fact that exp(0) equals one.
why it matters
This supplies the identity element for the U(1) group, completing one axiom in the derivation of gauge invariance from information redundancy. The module targets a Nature Physics paper on this origin; the result anchors the neutral element before composition and inverse lemmas are applied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.