timeTranslationFlow
The time-translation flow on real-valued trajectories is the one-parameter group generated by shifting the time argument of each path function. Researchers deriving conservation laws from symmetries in the J-action setting would reference this when invoking Noether's theorem for energy. The definition directly instantiates the OneParamGroup structure by delegating to the timeShift map and verifying the flow axioms with simplification tactics.
claimThe one-parameter group of time translations on the space of real-valued trajectories $γ : ℝ → ℝ$ is given by $(ϕ_t γ)(s) := γ(s + t)$.
background
In the Noether module for the J-action, RealAction denotes the type of real-valued trajectory functions $ℝ → ℝ$. The timeShift operation translates such a trajectory by a fixed amount dt in its argument: timeShift dt γ t := γ(t + dt). This module specializes the abstract noether_core theorem from the QFT.NoetherTheorem library to the cost-functional setting of Recognition Science, where continuous symmetries of the J-action yield conserved quantities along trajectories.
proof idea
The definition constructs the OneParamGroup instance by setting the flow map to timeShift and then proving the zero-flow and additivity properties. The zero case follows by function extensionality and simplification of the shift. Additivity is shown by extensionality, simplification, and ring normalization on the real numbers.
why it matters in Recognition Science
This supplies the concrete flow for the theorem time_translation_invariance_implies_energy_conservation, which states that time-translation invariance implies the action is conserved along the flow, interpreted as energy conservation. It realizes the time-translation symmetry case in the paper companion section on Noether Conservation Laws as Corollaries, connecting to the abstract noether_core result in the Recognition Science framework.
scope and limits
- Does not establish invariance of any particular J-action under the flow.
- Does not compute the conserved quantity explicitly.
- Does not extend to discrete time or quantum settings.
- Applies only to real-valued trajectories.
formal statement (Lean)
52def timeTranslationFlow : OneParamGroup RealAction where
53 flow t γ := timeShift t γ
proof body
Definition body.
54 flow_zero γ := by funext s; simp [timeShift]
55 flow_add s t γ := by funext u; simp [timeShift]; ring_nf
56
57/-- **Energy conservation from time-translation invariance.**
58
59 If a J-action functional is time-translation invariant, then by
60 `noether_core` it is itself conserved along the time-translation flow.
61 The conserved quantity is interpreted as the total energy. -/