spaceTranslationFlow
plain-language theorem explainer
The space-translation flow is the one-parameter group on real-valued trajectories that applies constant spatial shifts, acting as the symmetry generator whose invariance implies momentum conservation under the J-action. Researchers deriving Noether corollaries in Recognition Science cite this construction when linking spatial symmetries to conserved quantities. The definition directly wraps the spaceShift map and verifies the additive group axioms via extensionality and algebraic simplification.
Claim. The space translation flow is the one-parameter group on trajectories $γ : ℝ → ℝ$ defined by $(flow dx)(γ)(t) = γ(t) + dx$, satisfying the group laws $flow 0 = id$ and $flow (s + t) = flow s ∘ flow t$.
background
RealAction is the type of real-valued trajectories, abbreviated as $ℝ → ℝ$, on which the J-action functional is defined. The spaceShift map translates any such trajectory by a fixed amount dx, sending $γ$ to the function $t ↦ γ(t) + dx$. This module specializes the abstract noether_core theorem from QFT.NoetherTheorem to the cost-functional setting of the J-action, where continuous symmetries produce conserved quantities along trajectories.
proof idea
The definition sets flow dx γ := spaceShift dx γ. The two group axioms are discharged by function extensionality followed by simplification on the zero-shift case and by simplification plus the ring tactic on the additivity case.
why it matters
This supplies the flow object used by space_translation_invariance_implies_momentum_conservation, which invokes noether_core to obtain conservation of the J-action along spatial shifts and interprets the conserved quantity as total momentum. It completes the spatial case of the Noether corollaries listed in the module documentation, complementing the time-translation case for energy and aligning with the paper companion RS_Least_Action.tex section on conservation laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.