U1_composition
plain-language theorem explainer
U(1) gauge transformations compose by adding phases: the result of applying one after another equals a single transformation by the summed angle. Researchers deriving gauge symmetries from Recognition Science ledger redundancy would cite this to establish the group structure. The proof reduces directly to associativity of complex multiplication and the exponential addition formula.
Claim. $U_1(U_2(z)) = U_{1+2}(z)$ where $U_θ(z) := z · exp(iθ)$ for phases $θ_1, θ_2 ∈ ℝ$ and field value $z ∈ ℂ$.
background
Gauge invariance in Recognition Science emerges from ledger redundancy: distinct ledger encodings of the same physical state are related by gauge transformations. The module derives U(1) symmetry specifically as phase multiplication on complex fields. The referenced definition states that a U(1) gauge transformation is multiplication by $e^{iθ}$.
proof idea
Unfolds the definition of U1Transform via simp, rewrites the nested products with mul_assoc, invokes the exponential addition formula, then applies congruency and ring to equate the phases.
why it matters
Completes the composition axiom for the U(1) group, a required step toward showing that gauge symmetry originates from ledger redundancy as targeted in the module for a Nature Physics paper. It supplies the algebraic closure property that lets equivalent representations be treated as physically identical without altering observables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.