isTimeTranslationInvariant
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.