The Map and the Territory: A Constructive History of Mathematical Physics

This essay tells the story of 150 years of mathematical physics from an unfamiliar angle. A machine-verified research programme—approximately 11,000 lines of formally checked proofs in the Lean 4 proof assistant—has established that every empirical prediction of quantum and statistical mechanics examined so far can be derived using only the most elementary constructive logic, without the law of excluded middle or any principle of omniscience. The elaborate classical superstructure of modern physics—infinite-dimensional Hilbert spaces, thermodynamic limits, path integrals, singularity theorems—enters only through idealizations that no finite laboratory can instantiate. This essay traces how classical logic was progressively imported into mathematical physics from the 1870s onward, what it cost at each stage, what constructive alternatives existed or could have been used instead, and what the pattern implies for the current state of theoretical physics. Paper 12 in the Constructive Calibration Programme, a companion to the formal synthesis (Paper 10), written for a broader audience. The essay covers five acts: (I) the Weierstrass–Boltzmann era and the import of LPO into analysis and statistical mechanics; (II) quantum mechanics, where density matrices, spectral bounds, and uncertainty relations live at BISH; (III) general relativity, where singularity theorems require LEM but all observational content is constructive; (IV) quantum field theory, where every confirmed prediction is a finite BISH computation despite the infinite-dimensional formalism; and (V) post-Standard-Model physics and the structural correlate between logical altitude and empirical disconnection. Features 11 TikZ figures illustrating key conceptual relationships, 9 highlighted key-message boxes, and a detailed bibliography connecting to the formally verified papers in the series. 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 Note: GitHub repository is not maintained; please see Zenodo for current files.