space_invariance_implies_conservation
plain-language theorem explainer
Space translation invariance of a real-valued function P implies P is constant along translation orbits. Researchers deriving conservation laws from cost stationarity in Recognition Science QFT would cite this specialization. The proof is a direct one-line application of the general invariance-implies-conservation lemma to the translation group.
Claim. If $P : ℝ → ℝ$ satisfies $P(x + dx) = P(x)$ for all real $dx$ and all $x$, then $P(x + t_1) = P(x + t_2)$ for all real $t_1, t_2$ and $x$.
background
In this QFT module the cost functional is written P. A map T is a symmetry of P when P(Tx) equals P(x) for every x. The space translation flow is the one-parameter group whose action is addition by a fixed real displacement dx. A quantity Q is conserved along a flow φ when Q(φ(t1, x)) equals Q(φ(t2, x)) for all parameters t1, t2 and base point x.
proof idea
This is a one-line wrapper that applies the noether_core theorem to the supplied invariance hypothesis for the space translation group.
why it matters
The declaration specializes the general noether_core result to spatial translations, yielding momentum conservation from invariance of the cost functional. It fills one concrete case in the module's derivation of Noether's theorem from ledger balance under symmetries, as described in the module documentation. The surrounding framework links such conservations to the eight-tick phase structure and the emergence of three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.