IndisputableMonolith.Action.Noether
This module defines the J-action functional on real-valued trajectories together with its time and space translation invariances. Researchers deriving conservation laws from Recognition Science cost functionals would cite it to connect the action principle to Noether's theorem. The module imports the Hamiltonian formulation from the J-action and the general Noether result from cost stationarity, supplying the concrete action-level objects used downstream.
claimLet $S_J[ q ] = 0$ denote the J-action on trajectories $q: I → ℝ$. Time-translation invariance of $S_J$ implies conservation of the conjugate energy $E = p^2/(2m) + V(q)$, while space-translation invariance implies conservation of momentum $p = m q̇$.
background
The module sits inside the Action domain and imports the Hamiltonian formulation obtained from the J-action via Legendre transform of the small-strain Lagrangian $L(q, q̇) = ½ m q̇² - V(q)$. It also imports the QFT Noether theorem that extracts conserved quantities directly from cost-stationarity of the underlying functional. The central object is the real-valued J-action whose translation symmetries are expressed through the sibling declarations RealAction, timeShift, isTimeTranslationInvariant, spaceShift and their associated flow maps.
proof idea
This is a definition module, no proofs. It declares the action functional, the shift operators, the invariance predicates, and the two conservation statements energy_conservation_of_J_action and space_translation_invariance_implies_momentum_conservation as direct applications of the imported Noether theorem.
why it matters in Recognition Science
The module supplies the action-level foundation required by EnergyConservationDomainCert, which certifies energy conservation along Newtonian trajectories. It completes the concrete step from the general cost-stationarity Noether theorem (QFT-006) to the specific conservation laws of the J-action, closing the link between the Hamiltonian derivation and domain-certified conservation statements.
scope and limits
- Does not treat field theories or higher-dimensional targets.
- Does not address gauge symmetries or internal symmetries.
- Does not derive the J-action form from the forcing chain.
- Does not include relativistic or quantum corrections.
used by (1)
depends on (2)
declarations in this module (11)
-
abbrev
RealAction -
def
timeShift -
def
isTimeTranslationInvariant -
def
timeTranslationFlow -
theorem
time_translation_invariance_implies_energy_conservation -
def
spaceShift -
def
isSpaceTranslationInvariant -
def
spaceTranslationFlow -
theorem
space_translation_invariance_implies_momentum_conservation -
theorem
energy_conservation_of_J_action -
def
noether_status