NoetherFalsifier
plain-language theorem explainer
NoetherFalsifier records a string description of an apparent violation of Noether's theorem together with a string resolution. Researchers deriving conservation laws from cost stationarity in Recognition Science cite this structure when enumerating consistency checks for ledger balance. The declaration is a plain record type with two fields and no computational content or axioms.
Claim. A Noether falsifier is a pair $(v, r)$ where $v$ is a string describing an apparent violation (conserved quantity without symmetry, symmetry without conservation in an isolated system, or energy-momentum violation) and $r$ is a string giving its resolution under cost stationarity.
background
The module derives Noether's theorem from Recognition Science cost stationarity: a symmetry is a transformation leaving the J-cost unchanged, while conservation follows from ledger balance along solutions. J-cost is defined as $J(x) = (x + x^{-1})/2 - 1$, which is strictly convex with unique minimum at $x=1$. Upstream structures supply the ledger factorization, phi-forcing of J, spectral emergence of gauge groups, and convex minimization properties that underwrite the stationarity argument.
proof idea
The declaration is a structure definition that introduces the record type directly; no lemmas or tactics are applied.
why it matters
It supplies the data type consumed by apparentViolations, which enumerates concrete cases such as energy non-conservation resolved by broken time-translation symmetry and baryon-number violation resolved by approximate U(1)_B. The structure therefore closes the loop from the mathematical proof of Noether's theorem (via cost stationarity) to the physical statement that apparent violations are explained by symmetry breaking rather than by failure of the ledger mechanism. It touches the open question of which symmetries remain exact once cosmological expansion is included.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.