time_invariance_implies_conservation
Time-translation invariance of a real-valued function E implies E remains constant along the time-translation flow. Researchers reconstructing Noether's theorem from cost stationarity in Recognition Science cite this specialization. The argument is a direct one-line application of the general noether_core result to the time-translation group.
claimLet $E : ℝ → ℝ$. If $E$ is invariant under the time-translation flow, i.e., $E(x + t) = E(x)$ for all real $x, t$, then $E$ is conserved along that flow: $E(x + t_1) = E(x + t_2)$ for all real $x, t_1, t_2$.
background
In the QFT-006 module, Noether's theorem emerges from cost stationarity: a symmetry leaves the J-cost unchanged and the corresponding charge stays constant along solutions. IsSymmetryOf states that a map T on X leaves J invariant when J(Tx) = Jx for every x. TimeTranslation is the one-parameter group whose flow is addition: flow t x := x + t. IsConservedAlong requires that a quantity Q takes identical values at all points on any orbit under the flow φ.
proof idea
This is a one-line wrapper that applies the noether_core theorem, substituting the given invariance hypothesis hinv directly into the general statement for an arbitrary one-parameter group.
why it matters in Recognition Science
The declaration supplies the time-translation case required by the module target of deriving Noether's theorem from ledger balance under symmetries. It directly yields the energy-conservation entry in the module's key-examples table and aligns with the Recognition Science emphasis on stationarity of the cost functional. No downstream uses are recorded yet.
scope and limits
- Does not derive the cost-stationarity premise itself.
- Does not identify E with a specific energy functional beyond the invariance hypothesis.
- Does not treat other symmetries such as spatial translations or rotations.
- Does not supply explicit forms or bounds for the conserved quantity.
formal statement (Lean)
137theorem time_invariance_implies_conservation {E : ℝ → ℝ}
138 (hinv : ∀ t, IsSymmetryOf (TimeTranslation.flow t) E) :
139 IsConservedAlong E TimeTranslation.flow :=
proof body
Term-mode proof.
140 noether_core hinv
141
142/-! ## Space Translation and Momentum -/
143
144/-- Space translation by dx. -/