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ₑpsilonbound: For any epsilon > 0 and interaction angle 0 = N₀. coherenceₑqgeometric: The coherence decays geometrically: c (N) = ||rho₀1|| * |cos (theta/2) |N. decoherenceMapₑqₚhysical: The explicit decoherence formula equals the physical definition Phi (rho) = TrEU (theta) (rho (x) |0> (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ₒfₗpo, lpoₒfbmc (axiomatized, citing Bridges-Vita 2006 and Paper 8). Sign-flip lemma (abcᵢffbmc): Fully proved, no custom axioms. TECHNICAL DETAILS Lean 4: leanprover/lean4: v4. 28. 0-rc1 Mathlib4: commit 7091f0f601d5aaea565d2304c1a290cc8af03e18 Build: cd P14Decoherence please see Zenodo for current files.