PhaseRotation
plain-language theorem explainer
PhaseRotation supplies the explicit U(1) flow on complex scalars via multiplication by exp(iθ). Recognition Science researchers working on Noether derivations cite it to realize phase symmetry for electric charge conservation. The definition satisfies the OneParamGroup structure by direct verification of the zero and additivity axioms using complex exponential identities.
Claim. The phase rotation is the one-parameter group on the complex numbers whose flow is given by the map φ(θ, z) = exp(i θ) z.
background
The QFT module derives Noether's theorem from cost stationarity, where a symmetry is any transformation leaving the J-cost unchanged and conservation follows from ledger balance along the flow. OneParamGroup is the structure with a flow map ℝ → X → X obeying flow(0, x) = x and the group law flow(s + t, x) = flow(s, flow(t, x)). Upstream results supply RS-native units with c = 1 and the eight-tick phase definitions used to anchor periodic symmetries.
proof idea
The definition constructs the flow directly and discharges the two axioms in the OneParamGroup structure. flow_zero follows from exp(0) = 1 by simp. flow_add rewrites via the exponential addition formula, pushes the cast, and closes by ring arithmetic on the angle sum.
why it matters
This definition instantiates the U(1) symmetry case in the Noether derivation. It is applied by phase_invariance_implies_conservation to obtain IsConservedAlong Q PhaseRotation.flow from the core noether_core lemma, yielding electric charge conservation. The construction sits inside the eight-tick octave framework and the ledger-based mechanism that replaces the classical action principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.