timeTranslationFlow
plain-language theorem explainer
The definition of the one-parameter group of time translations on real-valued trajectories in the J-action setting. Researchers deriving conservation laws from symmetries would cite this when applying the abstract Noether theorem to obtain energy conservation. It is realized by assigning the time-shift operator to the flow, with the group laws verified by direct simplification and ring normalization.
Claim. Let a real-valued trajectory be a map $γ : ℝ → ℝ$. The time-translation flow is the map $ϕ : ℝ → (ℝ → ℝ) → (ℝ → ℝ)$ given by $(ϕ_t γ)(s) := γ(s + t)$, satisfying the one-parameter group axioms $ϕ_0 = id$ and $ϕ_{s+t} = ϕ_s ∘ ϕ_t$.
background
RealAction denotes the type of real-valued trajectories $ℝ → ℝ$ on which a J-action functional is defined. The time-shift operator implements a constant time displacement on such trajectories by adding a fixed offset to the argument. The module specializes the abstract noether_core theorem from the QFT module to the J-cost functional setting, producing conserved quantities for continuous symmetries of the cost functional. Upstream results include the definition of RealAction and the time-shift operator, along with foundational structures from PrimitiveDistinction and SimplicialLedger that ground the continuum action.
proof idea
The definition constructs an instance of the one-parameter group by setting the flow component to the time-shift operator. The zero-flow property follows by function extensionality and simplification with the time-shift definition. The additivity property uses function extensionality, simplification, and ring normalization to verify that successive shifts compose additively.
why it matters
This supplies the concrete flow for the downstream theorem on time-translation invariance implying energy conservation, which invokes noether_core to conclude that time-translation invariant J-actions are conserved along the flow, with the conserved quantity identified as energy. It realizes one of the main results listed in the module documentation for Noether conservation laws as corollaries of the abstract theorem, linking to the paper section on Noether Conservation Laws. In the broader framework it provides the symmetry generator for energy in the least-action principle derived from the J-functional.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.