noether_status
plain-language theorem explainer
This definition stores a status string summarizing Noether conservation results for the J-action. Developers auditing formalization progress in Recognition Science would cite it to confirm that time and space translation invariance imply energy and momentum conservation. The implementation is a direct string literal that reports the application of the energy conservation theorem with zero sorries or axioms.
Claim. The status of Noether conservation in the J-action setting is given by the string reporting that time and space translation invariance imply conservation laws, specifically via energy conservation for the standard mechanics Lagrangian when the potential is time-independent.
background
The module specializes the abstract Noether theorem from the QFT library to the cost-functional J-action setting. Continuous symmetries of the J-action, such as time translation, yield conserved quantities along trajectories. The upstream theorem establishes that the standard total energy of mechanical motion is conserved when the potential is time-independent: for the 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. This is proven directly by the Hamiltonian energy conservation lemma. Action is abbreviated as the real numbers in RS-native units.
proof idea
This is a one-line definition that returns a fixed status string. The string explicitly names the upstream energy conservation theorem and reports its proof status (zero sorries, zero axioms). No tactics or reductions are applied beyond the literal assignment.
why it matters
This status definition marks the Noether section's completion within the Recognition framework, where conservation laws arise as direct corollaries of the abstract noether_core theorem applied to the J-action cost functional. It connects to the paper companion in papers/RS_Least_Action.tex, Section Noether Conservation Laws as Corollaries. It touches the open question of completing the full suite of symmetries, including phase rotation for charge conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.