phase_invariance_implies_conservation
plain-language theorem explainer
Phase invariance of a real-valued function on complex space implies it remains constant along the U(1) phase rotation flow. Quantum field theorists cite this when deriving electric charge conservation from U(1) symmetry inside the Recognition Science cost framework. The argument is a direct one-line application of the general noether_core lemma to the PhaseRotation group.
Claim. If a function $Q : ℂ → ℝ$ satisfies $Q(e^{iθ} z) = Q(z)$ for every real $θ$ and every $z ∈ ℂ$, then $Q$ is conserved along the phase rotation flow, meaning $Q(e^{iθ} z)$ is independent of $θ$.
background
The module derives Noether's theorem from cost stationarity: a transformation T is a symmetry of J when J(Tx) = Jx for all x, and Q is conserved along flow φ when Q(φ(t,x)) does not depend on t. PhaseRotation is the one-parameter group on ℂ whose flow multiplies by $e^{iθ}$. The upstream noether_core theorem states that invariance under any one-parameter group implies conservation along its flow.
proof idea
The proof is a one-line wrapper that applies the noether_core theorem to the hypothesis that Q is invariant under PhaseRotation.flow θ for every θ.
why it matters
This specializes the general noether_core result to U(1) phase symmetry, yielding the electric charge conservation entry in the module's symmetry table. It supports the module's target of deriving Noether's theorem from ledger balance under cost stationarity and connects to the Recognition Science framework's treatment of continuous symmetries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.