Technical Note 16: The Born Rule as a Logical Artefact — Lean 4 Formalization

Technical note filling the DC_omega row of the constructive calibration table. Lean 4 + Mathlib formalization verifying that finite-dimensional Born-rule probability (non-negativity, sum-to-one, expectation reality, variance non-negativity, Chebyshev bound) is BISH-constructive, while the frequentist strong law of large numbers (SLLN) requires Dependent Choice over N (DC_omega). Part A (BISH, Level 0): Theorems 1-5 — Born probability distribution, expectation reality, variance non-negativity, relative frequency bounds, Chebyshev/weak law bound. Finite-dimensional linear algebra, no limits, no choice. Part B (DC_omega, Level 2): Theorem 6 — SLLN via axiomatised DC_omega. The DC_omega layer is axiomatised (dc_omega_holds + slln_of_dc), not proved from scratch. The full constructive SLLN proof remains an open problem. Contribution is programme completeness — populating the DC_omega axis alongside Paper 6 (Heisenberg uncertainty) — not mathematical novelty. The BISH content is unsurprising finite-dimensional linear algebra; the DC_omega requirement for SLLN is known in constructive probability. Lean 4 formalization: 564 lines, 9 files, 0 sorry, 0 errors. CRM axiom audit (Paper 10 methodology): BISH theorems have axiom closure {propext, Classical.choice, Quot.sound} with no custom axioms; DC theorems add dc_omega_holds + slln_of_dc. Built with Lean 4 v4.28.0-rc1 and Mathlib4 (commit 7091f0f6). 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.