Action Noether Noether Status

The status string

Noether's theorem is a classical result in physics: it says that every continuous symmetry of a physical system's action corresponds to a conserved quantity. The most familiar pair is time symmetry giving energy conservation and space symmetry giving momentum conservation. The declaration noether_status is a short text string inside the Recognition Science framework's machine-checked library of formal theorems. It reports, in one line, that the framework has proved these two classical consequences for its own action functional, and that the proofs contain no unfinished steps and no extra axioms.

The string itself reads: "Action.Noether: time/space translation invariance ⇒ Noether conservation, energy_conservation_of_J_action (0 sorry, 0 axiom)". The first part names the module and the two symmetries. The second part points to the formal theorem energy_conservation_of_J_action, which states that for a standard mechanical Lagrangian, the total energy E = T + V is constant along a trajectory when the potential does not depend on time. The parenthetical "0 sorry, 0 axiom" is the library's audit trail: it means the proof was checked end to end and relies only on the ambient logic's standard postulates, not on any framework-specific assumptions.

What the string does not claim is just as important. It does not assert that Noether's theorem is new, nor that the framework discovered energy or momentum conservation. These are classical results, proved here as corollaries of a more abstract theorem applied to a particular action. The string also does not claim that the framework's own cost functional, the J-action, has been shown to produce these conservations directly; the named theorem is about the standard mechanics Lagrangian, not about the J-action itself. The status line is a bookkeeping entry, a compact certificate that a specific piece of formal work exists and is clean.

In practice, this means a reader can treat the status string as a pointer. It tells you where to look for the formal proofs, what those proofs cover, and that they passed a machine check. It does not extend the physics beyond what Noether proved in 1918. The value is in the audit, not in the content of the theorem itself.

def noether_status : String :=
  "Action.Noether: time/space translation invariance ⇒ Noether conservation, energy_conservation_of_J_action (0 sorry, 0 axiom)"

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

The status string does not claim that Noether's theorem is a new result or that the framework discovered energy conservation. The named theorem applies to the standard mechanics Lagrangian, not to the framework's own cost functional J. The zero-axiom audit refers to the proof's postulates within the ambient type theory, not to an absence of any foundational assumptions.

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: