timeShift
plain-language theorem explainer
The timeShift definition supplies the operator shifting a real trajectory γ by dt, so that the new path evaluates at t + dt. Researchers formalizing Noether theorems for the J-action cite it to express time-translation symmetry before deriving energy conservation. The definition is a direct pointwise functional shift with no lemmas or reductions required.
Claim. Let γ : ℝ → ℝ be a real-valued trajectory. The time translation by dt ∈ ℝ produces the shifted trajectory γ_dt defined by γ_dt(t) := γ(t + dt).
background
In the Action.Noether module the J-action is obtained by specializing the abstract noether_core theorem from QFT.NoetherTheorem to cost functionals on trajectories. RealAction is the type of maps ℝ → ℝ that represent real-valued paths on which the J-cost is evaluated. The module records that continuous symmetries of this cost yield conserved quantities along trajectories, with time translation corresponding to energy conservation.
proof idea
This is a direct definition: timeShift dt γ is the function that evaluates the original γ at the shifted argument t + dt. No upstream lemmas are invoked; the body is the explicit pointwise shift.
why it matters
timeShift is the primitive used to define isTimeTranslationInvariant, which states that a J-action S satisfies S(γ ∘ timeShift dt) = S(γ) for every dt, and to construct the one-parameter group timeTranslationFlow. It therefore supplies the concrete symmetry map that the module applies to the abstract noether_core result, yielding the energy-conservation corollary for the J-action as stated in papers/RS_Least_Action.tex, Section 'Noether Conservation Laws as Corollaries'.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.