space_translation_invariance_implies_momentum_conservation
plain-language theorem explainer
Space translation invariance of a J-action functional on real trajectories implies that the functional is conserved along the space translation flow, with the conserved quantity read as total momentum. Researchers applying Noether's theorem to cost functionals in variational mechanics would cite this for deriving momentum laws from spatial symmetries. The proof is a one-line wrapper applying the core noether_core lemma to the given invariance hypothesis.
Claim. If a functional $S$ on real-valued trajectories satisfies that for every displacement $dx$ the space-translation flow by $dx$ is a symmetry of $S$, then $S$ is conserved along the space-translation flow.
background
The module applies the abstract Noether theorem (from QFT.NoetherTheorem.noether_core) to J-action cost functionals. RealAction is the type of J-action functionals on real trajectories, i.e., maps from paths $ℝ → ℝ$ to $ℝ$. spaceTranslationFlow is the one-parameter group whose flow shifts trajectories by a fixed spatial displacement $dx$ while preserving the functional form.
proof idea
The proof is a one-line wrapper that applies noether_core to the invariance hypothesis h_inv.
why it matters
This result supplies the momentum-conservation corollary for space-translation invariance of the J-action, sitting alongside the time-translation case that yields energy conservation. It fills the space-translation slot in the paper companion section on Noether Conservation Laws as Corollaries. Within Recognition Science it connects continuous symmetries of the cost functional to conserved quantities, consistent with the derivation of three spatial dimensions from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.