Noether's Theorem and the Logical Cost of Global Conservation Laws (Paper 15 — Lean 4 Formalization)

Paper 15 in the Constructive Reverse Mathematics of Physics series. This deposit contains the complete Lean 4 + Mathlib formalization of Noether's theorem (energy conservation on a lattice) calibrated against constructive omniscience principles, together with the accompanying paper (LaTeX source and compiled PDF). MAIN RESULTS Part A — BISH content (constructive, no omniscience): noetherconservation: The total rate of energy change vanishes identically for any field configuration on a finite periodic lattice. This is the algebraic content of Noether's theorem — pure BISH. energyDensityₙonneg: Each energy density term is non-negative when V >= 0. This is the weak energy condition that enables the BMC pattern. partialEnergyₘono: The partial energy EN = Σ_{i= 0. sumₛhift / sumₛhiftₚrev: Shift invariance of periodic sums (Σ f (next (i) ) = Σ f (i) ), the key lemma for the telescoping argument. Part B — LPO equivalence: npscᵢffbmc: Nonnegative Partial Sum Convergence Bounded Monotone Convergence (fully proved, no custom axioms — pure BISH!). globalₑnergyᵢffLPO: The assertion "for every bounded field configuration with V >= 0, the total energy E = lim EN exists" is equivalent to the Limited Principle of Omniscience (LPO). npscᵢffₗpo: NPSC LPO (composition of npscᵢffbmc with bmcᵢffₗpo). FOUR DOMAINS, ONE LOGICAL STRUCTURE This is the fourth physical domain producing the BMC LPO pattern: Domain Paper Bounded Monotone Sequence LPO Content Statistical Mechanics P8 Free energy fN f_∞ exists exactlyGeneral Relativity P13 Radial coordinate r (τ) r → 0 exactlyQuantum Measurement P14 Coherence c (N) c → 0 (collapse) Conservation Laws P15 Partial energy EN E = lim EN exists AXIOM CERTIFICATE BISH theorems: propext, Classical. choice, Quot. sound — standard Mathlib infrastructure only. Classical. choice traces to Fin. fintype and Real. instField. No omniscience principles. Abstract framework (npscᵢffbmc): Fully proved, no custom axioms — NPSC ↔ BMC is pure BISH. LPO theorems: Above plus bmcₒfₗpo, lpoₒfbmc (axiomatized, citing Bridges-Vîță 2006 and Paper 8). CRM audit: bycases uses instDecidableEqNat (zero axioms). No Classical. em or Classical. byContradiction anywhere. TECHNICAL DETAILS Lean 4: leanprover/lean4: v4. 28. 0-rc1 Mathlib4: commit 7091f0f601d5aaea565d2304c1a290cc8af03e18 Build: cd P15Noether please see Zenodo for current files.