What question did this study set out to answer?

To formalize the Born rule within the Lean 4 framework, verifying its constructive properties and dependencies on axioms.

February 12, 2026Open Access

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

Key Points

To formalize the Born rule within the Lean 4 framework, verifying its constructive properties and dependencies on axioms.
Formalization using Lean 4 and Mathlib to validate finite-dimensional Born-rule probabilities.
Examination of finite-dimensional linear algebra without reliance on limits or choice principles.
Development of theorems related to probability distributions, expectation reality, and variance.
Confirmed that finite-dimensional Born-rule probabilities are BISH-constructive.
Established that SLLN necessitates Dependent Choice over N, presenting it axiomatically rather than proving from the ground up.
Achieved programme completeness by integrating the DC_omega axis with previous works.

Abstract

Technical note filling the DCₒmega 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ₒmega). 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ₒmega, Level 2): Theorem 6 — SLLN via axiomatised DCₒmega. The DCₒmega layer is axiomatised (dcₒmegaₕolds + sllnₒfdc), not proved from scratch. The full constructive SLLN proof remains an open problem. Contribution is programme completeness — populating the DCₒmega axis alongside Paper 6 (Heisenberg uncertainty) — not mathematical novelty. The BISH content is unsurprising finite-dimensional linear algebra; the DCₒmega 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ₒmegaₕolds + sllnₒfdc. 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-16Paper 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-16Paper 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.

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

Key Points

Abstract

Cite This Study