timeShift
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.
claimLet γ : ℝ → ℝ 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 in Recognition Science
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'.
scope and limits
- Does not prove any invariance or conservation statement.
- Does not apply to complex-valued trajectories or phase rotations.
- Does not reference the phi-ladder, mass formulas, or D = 3.
- Does not incorporate the eight-tick octave or RCL identity.
Lean usage
example (dt : ℝ) (γ : RealAction) : RealAction := timeShift dt γformal statement (Lean)
43def timeShift (dt : ℝ) : RealAction → RealAction :=
proof body
Definition body.
44 fun γ t => γ (t + dt)
45
46/-- A J-action `S` on `RealAction` is time-translation invariant if
47 `S(γ ∘ t-shift) = S(γ)` for every shift. -/