isTimeTranslationInvariant
A J-action functional S on real-valued trajectories is time-translation invariant when it remains unchanged under every real time shift of its argument. Researchers deriving energy conservation from symmetries in the Recognition Science cost-functional setting would cite this definition as the precise hypothesis for the Noether argument. It is a direct definition that applies the invariance predicate to the family of time-shift maps.
claimA functional $S: (ℝ → ℝ) → ℝ$ is time-translation invariant if for every real $dt$ the shifted trajectory satisfies $S(γ ∘ τ_{dt}) = S(γ)$ for all trajectories $γ$, where $τ_{dt}$ is the map $t ↦ t + dt$.
background
RealAction denotes the space of real-valued trajectories, i.e., maps from ℝ to ℝ that serve as the domain for J-action functionals. The timeShift operation translates the time argument of any such trajectory by a fixed real amount dt. IsSymmetryOf states that a transformation T leaves a functional J invariant precisely when J(Tx) equals J(x) for every input x.
proof idea
This is a definition that directly encodes the invariance condition by quantifying over all real shifts dt and requiring that each timeShift dt is a symmetry of S according to the IsSymmetryOf predicate.
why it matters in Recognition Science
This definition supplies the exact statement of time-translation invariance for the J-action, which functions as the hypothesis for energy conservation in the module's application of the abstract noether_core theorem. It underpins the main result time_translation_J_invariant described in the module documentation as the standard Noether-conservation hypothesis for energy, with the paper companion in papers/RS_Least_Action.tex, Section Noether Conservation Laws as Corollaries. In the Recognition Science framework it connects the least-action principle to conserved quantities arising from continuous symmetries.
scope and limits
- Does not establish that time-translation invariance holds for any concrete action functional.
- Does not derive the associated conserved energy quantity from the invariance.
- Does not extend the statement to complex-valued or higher-dimensional trajectories.
- Does not address discrete time shifts or non-continuous symmetries.
formal statement (Lean)
48def isTimeTranslationInvariant (S : RealAction → ℝ) : Prop :=
proof body
Definition body.
49 ∀ dt : ℝ, IsSymmetryOf (timeShift dt) S
50
51/-- The time-translation flow on `RealAction`. -/