Action Noether Space Translation Invariance Implies Momentum Conservation

The conservation law

In classical mechanics, Noether's theorem links continuous symmetries of a physical system to conserved quantities. The Recognition Science framework's machine-checked library of formal theorems contains a specialization of this abstract result to its own cost-functional setting. The declaration space_translation_invariance_implies_momentum_conservation establishes the following: if a J-action functional on real-valued trajectories is invariant under a constant shift in space, then the functional is conserved along the space-translation flow. The conserved quantity is interpreted as the total momentum.

The theorem is a direct corollary of the abstract noether_core theorem applied to the cost functional. The proof in the library is axiom-clean, meaning it relies only on the standard axioms of the ambient type theory and contains no unproven assumptions. This is a formal, machine-checked result, not a heuristic argument.

In Recognition Science, the framework models physical laws as consequences of a forced cost function, and this theorem is one of its derived results. The framework's library also contains analogous theorems for time-translation invariance implying energy conservation and phase-rotation invariance implying charge conservation. These are all corollaries of the same abstract Noether theorem.

What the theorem does not claim is equally important. It does not prove that any particular physical system is space-translation invariant; that is a separate hypothesis. It does not derive the specific form of the conserved quantity beyond identifying it as momentum. And it does not claim that the J-action is the only possible action functional, only that if it is space-translation invariant, then momentum is conserved.

/-- **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 theorem does not prove that any particular physical system is space-translation invariant. The theorem does not derive the specific form of the conserved quantity beyond identifying it as momentum. The theorem does not claim that the J-action is the only possible action functional.

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: