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

Version 1.1 (02/09/2026) This essay tells the story of years of mathematical physics from an unfamiliar angle. A machine-verified research programme — approximately 11,000 lines of formally checked proofs in the Lean 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. The calibration covers quantum states, static structures, and exactly solvable models; time evolution, scattering amplitudes, and real-time path integrals remain uncalibrated. Paper 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 TikZ figures illustrating key conceptual relationships, highlighted key-message boxes, and a detailed bibliography connecting to the formally verified papers in the series. --- ## Contents "`paper 12/v1.1/|-- essay_constructive_history.tex LaTeX source (33 pages, TikZ figures)|-- essay_constructive_history.pdf compiled PDF|-- ZENODO_DESCRIPTION.md this file"` This paper contains no Lean code. The formal proofs it discusses are archived separately as Papers 2, 6-11, and in the Constructive Calibration Programme. --- ## Relationship to Other Papers | Paper | Title | Role ||-------|-------|------|| | WLPO Equivalence of the Bidual Gap | Singular states calibration || | Heisenberg Uncertainty in CRM | Preparation vs. measurement HUP || | Non-Reflexivity of S_1(H) | WLPO dispensability || | LPO-Equivalence of 1D Ising (Transfer Matrix) | Thermodynamic limit calibration || | Formulation-Invariance (Combinatorial Ising) | Domain invariance evidence || | Formal Synthesis | Machine-verified summary of all calibrations || | Tsirelson Bound and Bell Entropy | Quantum entanglement at BISH || **12** | **The Map and the Territory (this paper)** | **Narrative essay for broad audience** || | Schwarzschild Geodesic Incompleteness | GR singularity calibration | --- 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. --- ## Citation "`bibtex@unpublished{Lee2026Paper12, author = {Lee, Paul Chun-Kit}, title = {The Map and the Territory: A Constructive History of Mathematical Physics}, year = {2026}, note = {Paper in the Constructive Calibration Programme, Version 1.1},}"`