The Measurement Problem as a Logical Artefact: Constructive Calibration of Quantum Decoherence (Paper 14 — Lean 4 Formalization)

Paper 14 in the Constructive Reverse Mathematics of Physics series. This deposit contains the complete Lean 4 + Mathlib formalization of quantum decoherence calibrated against constructive omniscience principles, together with the accompanying paper (LaTeX source and compiled PDF). MAIN RESULTS Part A — BISH content (constructive, no omniscience): decoherence_epsilon_bound: For any epsilon > 0 and interaction angle 0 < theta < pi, there exists an explicitly computable N_0 such that the quantum coherence c(N) < epsilon for all N >= N_0. coherence_eq_geometric: The coherence decays geometrically: c(N) = ||rho_01|| * |cos(theta/2)|^N. decoherenceMap_eq_physical: The explicit decoherence formula equals the physical definition Phi(rho) = Tr_E[U(theta) (rho (x) |0><0|) U^dag(theta)], verified by brute-force 4x4 matrix computation. Part B — LPO equivalence: exact_decoherence_iff_LPO: The assertion "every bounded antitone sequence converges exactly" is equivalent to the Limited Principle of Omniscience (LPO). abc_iff_bmc: Antitone Bounded Convergence <-> (monotone) Bounded Monotone Convergence, via sign-flip (fully proved, no axioms). AXIOM CERTIFICATE BISH theorems: [propext, Classical.choice, Quot.sound] — standard Mathlib infrastructure only. No omniscience principles. LPO theorems: Above plus bmc_of_lpo, lpo_of_bmc (axiomatized, citing Bridges-Vita 2006 and Paper 8). Sign-flip lemma (abc_iff_bmc): Fully proved, no custom axioms. TECHNICAL DETAILS Lean 4: leanprover/lean4:v4.28.0-rc1 Mathlib4: commit 7091f0f601d5aaea565d2304c1a290cc8af03e18 Build: cd P14_Decoherence && lake exe cache get && lake build Status: 0 errors, 0 sorry PACKAGE CONTENTS P14_Decoherence/ — Self-contained Lean 4 package (9 source files, 805 lines) paper14_writeup.tex — LaTeX source paper14_writeup.pdf — Compiled paper (13 pages) README.md — Build instructions and file manifest 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 — DOI: 10.5281/zenodo.18527877Paper 11: Entanglement, CHSH, Tsirelson bound — DOI: 10.5281/zenodo.18527676Paper 12: Constructive history of mathematical physics — DOI: 10.5281/zenodo.18528793Paper 13: Event horizon as logical boundary — DOI: 10.5281/zenodo.18529007 Paper 14: Quantum Decoherence - DOI: 10.5281/zenodo.18569068 Note: GitHub repository is not maintained; please see Zenodo for current files.