Action Noether Is Space Translation Invariant

Momentum from symmetry

In classical mechanics, a symmetry of a system's action often leads to a conserved quantity. The action is a number assigned to a possible path of motion, and a symmetry is a transformation that leaves that number unchanged. The theorem of Emmy Noether, published in 1918, makes this precise: for every continuous symmetry of the action, there is a corresponding conserved quantity. The most familiar example is that if the action does not change when you shift all positions by a constant amount, then the total momentum of the system is conserved.

The Recognition Science framework builds a machine-checked library of formal theorems that specializes Noether's result to its own cost functional, called the J-action. Within this framework, recognition (a discrete record of events) assigns a cost to every possible trajectory, and the framework's library proves that the abstract Noether theorem applies to this cost. The declaration isSpaceTranslationInvariant defines what it means for such a cost functional to be symmetric under space translation: shifting the trajectory by any constant amount leaves the cost unchanged. This is a definition, not a theorem, and it is the hypothesis for the conservation result that follows.

The framework's library then proves the theorem space_translation_invariance_implies_momentum_conservation. It states that if a J-action functional is space-translation invariant, then the functional itself is conserved along the space-translation flow. In plain terms, if the cost of a path does not depend on where the path is located in space, then the total momentum of the system is constant over time. This is the direct analogue of the standard Noether result, and it is a corollary of the abstract noether_core theorem applied to the cost functional.

The declaration does not claim that any particular physical system is space-translation invariant. It only establishes the conditional statement: if a system's action has this symmetry, then momentum is conserved. It also does not claim that the conserved quantity is the ordinary mechanical momentum m v; the framework interprets it as total momentum, but the theorem itself only establishes that something is conserved. The framework's library also proves analogous results for time-translation invariance and energy conservation, and for phase-rotation invariance and charge conservation, all as corollaries of the same abstract theorem.

/-- A J-action functional on real-valued trajectories is
    space-translation invariant if shifting the trajectory by a constant
    leaves the action unchanged. -/
def isSpaceTranslationInvariant (S : RealAction → ℝ) : Prop :=
  ∀ dx : ℝ, IsSymmetryOf (spaceShift dx) S

/-- **Momentum conservation from space-translation invariance.**

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

/-- **Momentum conservation from space-translation invariance.**

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

What this page does not claim

The declaration does not claim that any particular physical system is space-translation invariant. The theorem does not identify the conserved quantity as the ordinary mechanical momentum m v. The framework does not claim to derive the value of the momentum or any other physical constant from this symmetry alone.

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: