Action Noether Time Translation Flow

The time-translation flow

In classical mechanics, a trajectory is a path through space over time. Shifting that path forward or backward in time, so that the same motion happens later or earlier, is a symmetry of many physical systems. The time-translation flow is the mathematical name for the family of all such shifts, one for every possible duration. The declaration timeTranslationFlow in the Recognition Science library defines this family precisely: it takes a trajectory and a shift amount, and produces the trajectory whose value at any time is the original trajectory's value at the shifted time. It also records the two properties that make this family a flow: shifting by zero changes nothing, and shifting by one amount and then another equals shifting by their sum.

The definition itself is modest, but it supports a classical result. In 1918, Emmy Noether proved that continuous symmetries of a system's action correspond to conserved quantities. The Recognition Science library specializes this theorem to its own cost functional, which it calls the J-action, a measure of the total cost of a trajectory. The library proves that if a J-action is unchanged by every time shift, then the action itself is conserved along the flow. The conserved quantity is interpreted as total energy. A separate theorem, proved directly rather than through Noether's theorem, shows that for the standard mechanical Lagrangian, kinetic energy minus potential energy, a time-independent potential guarantees this invariance and hence energy conservation.

What the declaration does not claim is just as important. It does not assert that any particular physical system is time-translation invariant. It only defines the flow and proves the conditional statement: if invariance holds, then conservation follows. It does not claim that the J-action is the unique action for mechanics, nor that energy is conserved in all circumstances. The theorem about the standard Lagrangian assumes differentiability and the Euler-Lagrange equations, conditions that real systems may fail. The flow is a tool, not a physical law on its own.

/-- The time-translation flow on `RealAction`. -/
def timeTranslationFlow : OneParamGroup RealAction where
  flow t γ := timeShift t γ
  flow_zero γ := by funext s; simp [timeShift]
  flow_add s t γ := by funext u; simp [timeShift]; ring_nf

/-- **Energy conservation from time-translation invariance.**

    If a J-action functional is time-translation invariant, then by
    `noether_core` it is itself conserved along the time-translation flow.
    The conserved quantity is interpreted as the total energy. -/
theorem time_translation_invariance_implies_energy_conservation
    (S : RealAction → ℝ)
    (h_inv : ∀ t, IsSymmetryOf (timeTranslationFlow.flow t) S) :
    IsConservedAlong S timeTranslationFlow.flow :=
  noether_core h_inv

/-- **The standard total energy of mechanical motion is conserved when
    the potential is time-independent.**

    This is the concrete Noether theorem for the standard mechanics
    Lagrangian `L = ½ m q̇² - V(q)`: time-translation invariance is
    automatic when `V` does not depend on `t` explicitly, and energy
    conservation `E = T + V` follows.

    Proven directly by `Action.Hamiltonian.energy_conservation`, this
    lemma packages the result in the `Noether` namespace for clarity. -/
theorem energy_conservation_of_J_action (m : ℝ) (hm : 0 < m) (V : ℝ → ℝ)
    (γ : ℝ → ℝ)
    (hV_diff : ∀ t, DifferentiableAt ℝ V (γ t))
    (hγ_diff : ∀ t, DifferentiableAt ℝ γ t)
    (hγ_diff2 : ∀ t, DifferentiableAt ℝ (deriv γ) t)
    (h_dE_eq_factored : ∀ t : ℝ,
      deriv (HamiltonianMech.totalEnergy m V γ) t =
        deriv γ t * (m * deriv (deriv γ) t + deriv V (γ t)))
    (hEL : ∀ t : ℝ, QuadraticLimit.standardEL m V γ t = 0) :
    ∀ t₁ t₂ : ℝ,
      HamiltonianMech.totalEnergy m V γ t₁ = HamiltonianMech.totalEnergy m V γ t₂ :=
  HamiltonianMech.energy_conservation m hm V γ hV_diff hγ_diff hγ_diff2 h_dE_eq_factored hEL

What this page does not claim

No physical system is asserted to be time-translation invariant. No claim that the J-action is the only valid action for mechanics. No claim that energy conservation holds without the stated differentiability and Euler-Lagrange conditions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Action/Noether.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: