Action Noether Space Translation Flow

The flow of space translation

In classical mechanics, the action is a single number that summarizes an entire trajectory of a system, from its starting point to its ending point. The principle of stationary action says that the trajectory a system actually follows is the one for which this number is, in a precise sense, unchanging against small variations. A symmetry of the action, a transformation that leaves this number unchanged, leads to a conserved quantity, a fact known as Noether's theorem, named after Emmy Noether who published it in 1918. The theorem is a central result in modern physics because it connects the abstract symmetries of nature to concrete conservation laws, such as the conservation of energy and momentum.

The declaration spaceTranslationFlow in the Recognition Science framework's machine-checked library of formal theorems is a precise definition of a one-parameter group of transformations. Each transformation in this group takes a trajectory and shifts it by a constant amount in space, meaning it adds a fixed value to the trajectory's position at every moment in time. The declaration formally verifies that these shifts form a group, which means that shifting by zero changes nothing and that shifting by one amount followed by another is the same as shifting by their sum. This is a purely mathematical statement about the structure of these transformations, not yet a statement about any particular physical system.

The framework then uses this definition to prove a theorem: if a J-action functional is invariant under this flow, meaning its value does not change when the trajectory is shifted in space, then the action itself is conserved along the flow. The conserved quantity is interpreted as the total momentum of the system. This result is a direct corollary of the abstract Noether theorem applied to the cost functional. In plain language, it establishes that a system whose behavior does not depend on where it is located in space will have a constant momentum, a familiar principle from classical physics.

This theorem does not claim that any particular physical system is space-translation invariant. It only states the logical consequence that follows if such an invariance holds. It also does not derive the value of momentum from first principles, nor does it claim that the framework's J-action is the only possible action functional. The declaration is a formal, machine-checked statement about the relationship between a symmetry and a conservation law, not an empirical claim about the universe.

/-- The space-translation flow on `RealAction`. -/
def spaceTranslationFlow : OneParamGroup RealAction where
  flow dx γ := spaceShift dx γ
  flow_zero γ := by funext s; simp [spaceShift]
  flow_add s t γ := by funext u; simp [spaceShift]; ring

/-- **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

This theorem does not claim that any particular physical system is space-translation invariant. This theorem does not derive the numerical value of momentum from first principles. This 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: