spaceTranslationFlow
spaceTranslationFlow supplies the one-parameter group of spatial translations acting on real-valued trajectories in the J-action setting. Noether applications in Recognition Science cite it when converting translation invariance into momentum conservation via the abstract noether_core result. The definition installs spaceShift as the flow map and discharges the group axioms by direct simplification and ring arithmetic.
claimThe one-parameter group of space translations on trajectories $γ : ℝ → ℝ$ is the map sending displacement $dx$ to the shifted trajectory $t ↦ γ(t) + dx$.
background
The Noether module specializes the abstract noether_core theorem to J-action cost functionals on real trajectories. RealAction is the type ℝ → ℝ of such trajectories. spaceShift(dx, γ) is the concrete translation that adds the constant dx to every value of γ, leaving the time parameter untouched.
proof idea
The definition installs flow dx γ := spaceShift dx γ. flow_zero is discharged by funext followed by simp on the spaceShift definition. flow_add is discharged by funext, simp, and ring normalization of the resulting arithmetic identity.
why it matters in Recognition Science
This flow is the spatial generator fed directly into space_translation_invariance_implies_momentum_conservation, which applies noether_core to obtain the conserved momentum. It realizes the spatial-translation symmetry in the module's treatment of Noether conservation laws as corollaries of the J-action, consistent with the framework's derivation of D = 3 dimensions and momentum as the associated charge.
scope and limits
- Does not prove that any concrete J-action functional is invariant under the flow.
- Does not derive the explicit form of the conserved momentum.
- Does not treat time-translation or phase-rotation symmetries.
- Does not extend the construction beyond real-valued one-dimensional trajectories.
Lean usage
theorem momentum_conservation (S : RealAction → ℝ) (h_inv : ∀ dx, IsSymmetryOf (spaceTranslationFlow.flow dx) S) : IsConservedAlong S spaceTranslationFlow.flow := noether_core h_invformal statement (Lean)
81def spaceTranslationFlow : OneParamGroup RealAction where
82 flow dx γ := spaceShift dx γ
proof body
Definition body.
83 flow_zero γ := by funext s; simp [spaceShift]
84 flow_add s t γ := by funext u; simp [spaceShift]; ring
85
86/-- **Momentum conservation from space-translation invariance.**
87
88 If a J-action functional is space-translation invariant, then by
89 `noether_core` it is itself conserved along the space-translation
90 flow. The conserved quantity is interpreted as the total momentum. -/