SpaceTranslation
plain-language theorem explainer
SpaceTranslation realizes spatial translations as the additive flow on the real line within the one-parameter group structure. Researchers deriving Noether's theorem from cost stationarity in Recognition Science cite this construction to link invariance under shifts to momentum conservation. The definition supplies the explicit flow map and discharges the group axioms by direct ring computation.
Claim. The space translation is the one-parameter group action on $ℝ$ given by $ϕ(dx, x) := x + dx$, which satisfies $ϕ(0, x) = x$ and $ϕ(s + t, x) = ϕ(s, ϕ(t, x))$.
background
In the QFT module, Noether's theorem is derived from cost stationarity, where symmetries of the J-cost functional yield conserved quantities. Space translation corresponds to momentum conservation, as listed in the module's table of symmetries. OneParamGroup is the structure consisting of a flow map from reals to transformations on a space X, together with the identity and composition axioms.
proof idea
The definition sets the flow to addition and verifies the two axioms using the ring tactic for algebraic simplification of the additive group on reals.
why it matters
This definition supplies the concrete symmetry for the space-translation case in the Noether theorem derivation. It is used by space_invariance_implies_conservation to conclude that invariant functions are conserved along the flow, via the noether_core lemma. In the Recognition Science framework this fills the space-translation entry in the symmetry-to-charge table, linking to momentum as the conserved quantity from the RSNativeUnits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.