time_translation_invariance_implies_energy_conservation
plain-language theorem explainer
Time-translation invariance of a J-action functional S on real trajectories implies S is conserved along the time-translation flow, interpreted as energy conservation. Researchers deriving Noether laws from symmetries in the Recognition Science least-action setting would cite this. The proof is a direct one-line application of the abstract noether_core theorem to the supplied invariance hypothesis.
Claim. If a functional $S: (ℝ → ℝ) → ℝ$ satisfies $S(φ_t(γ)) = S(γ)$ for all real $t$ and trajectories $γ$, where $φ$ denotes the time-translation flow, then $S(φ_{t_1}(γ)) = S(φ_{t_2}(γ))$ for all $t_1, t_2$.
background
The module specializes the abstract Noether theorem to the J-action cost-functional setting on real trajectories. RealAction is the type of maps from real-valued trajectories to reals. timeTranslationFlow is the one-parameter group whose flow acts by time shifts on these trajectories, satisfying the group axioms flow_zero and flow_add by direct simplification of the shift operation.
proof idea
The proof is a one-line wrapper that applies noether_core to the invariance hypothesis h_inv. noether_core states that invariance of J under all flows of a one-parameter group G implies J is conserved along G.flow; here G is timeTranslationFlow and the hypothesis supplies the required symmetry condition for every t.
why it matters
This declaration supplies the energy-conservation corollary of noether_core in the J-action setting, directly filling the time-translation case in the paper section on Noether Conservation Laws as Corollaries. It supports the Recognition framework's derivation of conserved quantities from continuous symmetries of the least-action functional, consistent with the forcing chain's emphasis on J-uniqueness and self-similar structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.