noether_summary
plain-language theorem explainer
Noether's theorem summary in Recognition Science asserts that invariance of a cost function J under the flow of a one-parameter group implies J is constant along flow orbits. Physicists deriving conservation laws such as energy from time translation or charge from phase rotation would cite this as the RS derivation from cost stationarity. The proof is a one-line wrapper that applies the core Noether lemma to the invariance hypothesis.
Claim. If a function $J: X → ℝ$ is invariant under each map in the flow of a one-parameter group $G$ on $X$ (i.e., $J(G.flow(t,x)) = J(x)$ for all real $t$ and all $x ∈ X$), then $J$ is conserved along the flow: $J(G.flow(t_1,x)) = J(G.flow(t_2,x))$ for all real $t_1,t_2$ and $x ∈ X$.
background
The QFT-006 module derives Noether's theorem from Recognition Science cost stationarity. A OneParamGroup consists of a flow map ℝ → X → X obeying the identity at t=0 and the additive group law. IsSymmetryOf holds for a transformation T when J(Tx) = J(x) for all x. IsConservedAlong requires the quantity to remain constant on every orbit of the flow.
proof idea
The proof is a one-line wrapper that applies noether_core to the supplied invariance hypothesis.
why it matters
This theorem summarizes the Noether correspondence within the Recognition Science framework, linking J-cost symmetries to conserved quantities as targeted by the module's derivation from ledger balance under transformations. It directly supports the listed standard-model examples (energy from time translation, momentum from space translation, charge from phase rotation). The result sits inside the broader cost-functional structure but does not yet connect to the forcing chain steps T5–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.