Synthesis and interpretive companion to the Constructive Calibration Programme (Papers 2, 4, 6, 7, 8, 9). Contains no new theorems. Assembles machine-verified results from six companion papers into a single calibration table mapping layers of quantum theory to positions in the constructive hierarchy of omniscience and choice principles. The calibration table establishes: finite-volume physics and preparation uncertainty (Heisenberg inequality) are fully constructive (BISH) ; measurement uncertainty and locale spatiality require Dependent Choice (DCₒmega) ; exact spectral membership requires Markov's Principle (MP, orthogonal axis) ; the bidual gap and singular states require WLPO; the thermodynamic limit requires LPO; and the spectral gap is undecidable. The logical geography forms a partial order, not a linear chain, with the omniscience spine (BISH < WLPO < LPO) as the dominant chain and DCₒmega and MP as orthogonal dimensions. Proposes a working hypothesis: empirical predictions of quantum theory are BISH-derivable, and stronger principles enter only through idealizations no finite laboratory can instantiate. Reports a formulation-invariance test (Papers 8 and 9) showing the LPO cost of the thermodynamic limit is identical across transfer-matrix and combinatorial derivations. Includes comparisons with van Wierst, Batterman, Pour-El and Richards, Gisin, and the Doering-Isham topos program. Six open problems are posed. Includes a TikZ diagram of the logical geography. All formal results are verified in Lean 4 (predominantly CRM over Mathlib; Paper 4 uses AxCal). The Lean 4 formalizations and manuscripts were developed with substantial AI assistance. version1. 1: This is the synthesis and conceptual companion to the author's constructive calibration programme (Papers 1–13). It contains no new theorems or Lean formalizations. Its purpose is to assemble the calibration table mapping layers of mathematical physics to positions in the constructive hierarchy (BISH < WLPO < LPO < LEM, with orthogonal axes DC_ω and MP), establish the series-wide certification methodology, formulate a working hypothesis, and pose open problems. What's New in v1. 1: Certification methodology section (§3): New ~2-page section establishing three certification levels — mechanically certified (P2Minimal, P7Minimal), structurally verified (Papers 7-Full, 8A, 9A, 11, 13-BISH), and intentional classical content (Papers 8B, 13-LPO) — with discussion of the Mathlib question, the role of minimal artifacts, and limitations. This is the section referenced by Papers 7, 8, 11, and 13 for the series-wide methodology. Expanded calibration table: Five new rows from Paper 11 (Bell nonlocality, entanglement entropy, partial trace — all BISH) and Paper 13 (Schwarzschild interior finite-time physics — BISH; geodesic incompleteness — LPO). Table now contains 17 entries across four domains of mathematical physics. Strengthened working hypothesis: Evidence now spans functional analysis, statistical mechanics, quantum information, and general relativity. Domain invariance discussion: Papers 8 and 13 use BMC ≡ LPO in unrelated physical domains (thermodynamic limit vs. geodesic incompleteness), providing evidence that LPO costs are intrinsic to the physics. Two new open problems: Infinite-dimensional entanglement entropy (Problem 7) and singularity calibration beyond Schwarzschild/Penrose theorem (Problem 8). Fixed TikZ diagram: MP no longer incorrectly shown as implying WLPO (they are independent over BISH). Paper (23 pages, LaTeX source + compiled PDF). No Lean code — this is a conceptual/synthesis paper. License: CC-BY 4. 0 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.
Building similarity graph...
Analyzing shared references across papers
Loading...
Paul Chun-Kit Lee
New York University
New York University
Building similarity graph...
Analyzing shared references across papers
Loading...
Paul Chun-Kit Lee (Sun,) studied this question.
synapsesocial.com/papers/698acaf07c832249c30ba9dd — DOI: https://doi.org/10.5281/zenodo.18527877