noether_core
plain-language theorem explainer
If a real-valued function J on space X is invariant under every map in the flow of a one-parameter group G, then J takes the same value at any two points along the same orbit. Researchers deriving conservation laws from symmetries in QFT or classical mechanics cite this as the algebraic core of Noether's theorem. The proof is a direct term-mode substitution that rewrites the goal using the invariance hypothesis at the two parameter values.
Claim. Let $X$ be a type and $G$ a one-parameter group on $X$ whose flow is denoted $G.flow$. Let $J:X→ℝ$. If $J$ is invariant under each flow map, i.e., $J((G.flow t)x)=J(x)$ for all $t$ and $x$, then $J$ is constant along orbits: $J((G.flow t_1)x)=J((G.flow t_2)x)$ for all $x,t_1,t_2$.
background
The module QFT.NoetherTheorem derives Noether's theorem from cost stationarity in Recognition Science. A one-parameter group is a structure equipped with a flow map $ℝ→X→X$ obeying the identity and additivity axioms. A map $T$ is a symmetry of $J$ precisely when $J(Tx)=Jx$ for every $x$. A quantity is conserved along a flow when its value is independent of the flow parameter on each orbit.
proof idea
The term-mode proof introduces the orbit point $x$ and the two times $t_1,t_2$, then rewrites the goal by substituting the invariance hypothesis once at $t_1$ and once at $t_2$. No auxiliary lemmas are required; the equality follows immediately from the two rewrites.
why it matters
This is the central lemma feeding every concrete conservation statement in the module. It is applied verbatim to obtain energy conservation from time-translation invariance and momentum conservation from space-translation invariance, and it supplies the witness for the Noether-charge construction and the summary theorem. In the Recognition Science setting it realizes the general claim that invariance of the J-cost under a continuous symmetry implies conservation of the associated charge, consistent with the ledger-balance mechanism described in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.