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): noether_conservation: 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_nonneg: Each energy density term is non-negative when V >= 0. This is the weak energy condition that enables the BMC pattern. partialEnergy_mono: The partial energy E_N = Σi<N ε_i is monotone increasing when V >= 0. sum_shift / sum_shift_prev: Shift invariance of periodic sums (Σ f(next(i)) = Σ f(i)), the key lemma for the telescoping argument. Part B — LPO equivalence: npsc_iff_bmc: Nonnegative Partial Sum Convergence <-> Bounded Monotone Convergence (fully proved, no custom axioms — pure BISH!). global_energy_iff_LPO: The assertion "for every bounded field configuration with V >= 0, the total energy E = lim E_N exists" is equivalent to the Limited Principle of Omniscience (LPO). npsc_iff_lpo: NPSC <-> LPO (composition of npsc_iff_bmc with bmc_iff_lpo). 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 f_N f_∞ exists exactlyGeneral Relativity P13 Radial coordinate r(τ) r → 0 exactlyQuantum Measurement P14 Coherence c(N) c → 0 (collapse)Conservation Laws P15 Partial energy E_N E = lim E_N 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_iff_bmc): Fully proved, no custom axioms — NPSC ↔ BMC is pure BISH. LPO theorems: Above plus bmc_of_lpo, lpo_of_bmc (axiomatized, citing Bridges-Vîță 2006 and Paper 8). CRM audit: by_cases 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 P15_Noether && lake exe cache get && lake build Status: 1955 jobs, 0 errors, 0 sorry PACKAGE CONTENTS P15_Noether/ Self-contained Lean 4 package (6 source files, ~520 lines)paper15_writeup.tex LaTeX sourcepaper15_writeup.pdf Compiled paper (15 pages)README.md Build instructions, file manifest, axiom certificate KEYWORDS constructive mathematics, reverse mathematics, Noether's theorem, conservation laws, energy conservation, lattice field theory, Lean 4, Mathlib, formal verification, LPO, bounded monotone convergence, NPSC, weak energy condition Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files):Paper 1: WithdrawnPaper 2: Bidual gap and WLPO — DOI: 10.5281/zenodo.17107493Paper 3: WithdrawnPaper 4: Quantum spectra axiom calibration — DOI: 10.5281/zenodo.17059483Paper 5: Schwarzschild curvature verification — DOI: 10.5281/zenodo.18489703Paper 6: Heisenberg uncertainty (v2, CRM over Mathlib) — DOI: 10.5281/zenodo.18519836Paper 7: Physical bidual gap, trace-class operators — DOI: 10.5281/zenodo.18527559Paper 8: 1D Ising model and LPO — DOI: 10.5281/zenodo.18516813Paper 9: Ising formulation-invariance — DOI: 10.5281/zenodo.18517570Paper 10: Logical geography of mathematical physics — 10.5281/zenodo.18580342 [v 2.0 Technical Synthesis of paper 1-16]Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18581707 [v 2.0 historical synthesis of paper 1-16]Paper 13: Event horizon as logical boundary — DOI: 10.5281/zenodo.18529007 Paper 14: Quantum Decoherence - DOI: 10.5281/zenodo.18569068 Paper 15: Noether Theorem - DOI: 10.5281/zenodo.18572494 Paper 16: Technical Note Born Rule - DOI: 10.5281/zenodo.18575377 Note: GitHub repository is not maintained; please see Zenodo for current files.