invariant_is_noether_charge
plain-language theorem explainer
Any function invariant under every element of a one-parameter group action on a space X is itself a Noether charge for that group. Researchers deriving conserved quantities from symmetries in cost-based formulations of QFT would cite this result. The proof is a one-line term construction that invokes the noether_core lemma to witness conservation along the flow and then packages the given J as the required subtype.
Claim. Let $X$ be a space equipped with a one-parameter group $G$ whose flow satisfies the group axioms. Let $J: X → ℝ$ satisfy $J(G.flow(t,x)) = J(x)$ for every real $t$ and every $x$. Then there exists a Noether charge $Q$ for $G$ (i.e., a real-valued function conserved along the flow of $G$) such that $Q = J$.
background
The module derives Noether's theorem from cost stationarity: a symmetry is a transformation that leaves the J-cost unchanged, and conservation follows from ledger balance under that symmetry. OneParamGroup is the structure supplying a flow map ℝ → X → X obeying flow(0,x) = x and the additive group law. IsSymmetryOf(T,J) is the proposition that J(T x) = J x for all x, i.e., invariance of J under the map T. NoetherCharge G is the subtype of functions X → ℝ that are conserved along G.flow, written {Q : X → ℝ // IsConservedAlong Q G.flow}. The local setting is QFT-006, which lists time translation to energy, space translation to momentum, and U(1) phase to electric charge as concrete instances.
proof idea
The proof is a direct term-mode wrapper. It applies the noether_core lemma (which converts the family of invariance hypotheses hinv into the single statement IsConservedAlong J G.flow) and constructs the subtype element ⟨J, noether_core hinv⟩. The final rfl discharges the equality Q.val = J by reflexivity.
why it matters
This theorem supplies the general bridge from invariance to conservation that the module uses to obtain energy as the Noether charge of time translation. It realizes the paper proposition that Noether's theorem follows from the ledger structure of Recognition Science rather than from an independent action principle. The result sits inside the QFT development that begins from the cost functional equation and the eight-tick octave, and it is the immediate predecessor of the TimeTranslation section that follows in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.