Wang Tiling and the Origin of Physical Undecidability: Berger's Theorem Is LPO (Paper 38, Constructive Reverse Mathematics Series)

Paper 38 in the Constructive Reverse Mathematics of Mathematical Physics series. Every undecidability result in quantum many-body physics --- from spectral gaps to phase diagrams --- descends from the undecidability of Wang tiling (Berger 1966). This paper establishes that Wang tiling itself is Turing-Weihrauch equivalent to LPO, proving that the entire genealogy of physical undecidability from Berger through Cubitt lives at a single logical stratum. The tiling decision problem and aperiodicity detection are both shown to be LPO-equivalent. The Genealogy Theorem demonstrates that all known physical undecidabilities factor through Wang tiling, and the Sigma-1-zero ceiling theorem explains why: all physical constructions reduce to halting (which is Sigma-1-zero-complete), so Wang tiling and all its descendants cost exactly LPO. No physical system yet known encodes Sigma-2-zero-complete problems (but see Paper 39). All results formalized in Lean 4 over Mathlib with zero sorry. The formalization comprises 7 Lean source files. Complete Paper List Other papers in the Constructive Reverse Mathematics Series (see Zenodo for current files): Summary Papers: Paper 10: Logical geography of mathematical physics -- DOI: 10.5281/zenodo.18636180 Paper 12: Constructive history of mathematical physics -- DOI: 10.5281/zenodo.18636250 Series: Paper 1: Withdrawn Paper 2: Bidual gap and WLPO -- DOI: 10.5281/zenodo.17107493 Paper 3: Withdrawn Paper 4: Quantum spectra axiom calibration -- DOI: 10.5281/zenodo.17059483 Paper 5: Schwarzschild curvature verification -- DOI: 10.5281/zenodo.18489703 Paper 6: Heisenberg uncertainty (v2, CRM over Mathlib) -- DOI: 10.5281/zenodo.18519836 Paper 7: Physical bidual gap, trace-class operators -- DOI: 10.5281/zenodo.18527559 Paper 8: 1D Ising model and LPO -- DOI: 10.5281/zenodo.18516813 Paper 9: Ising formulation-invariance -- DOI: 10.5281/zenodo.18517570 Paper 10: Logical geography of mathematical physics -- DOI: 10.5281/zenodo.18627193 Paper 11: Entanglement, CHSH, Tsirelson bound -- DOI: 10.5281/zenodo.18527676 Paper 12: Constructive history of mathematical physics -- DOI: 10.5281/zenodo.18627283 [v2.0 Historical Synthesis of Papers 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 Paper 17: Bekenstein-Hawking formula -- DOI: 10.5281/zenodo.18597306 Paper 18: Constructive Stratification of the Standard Model Yukawa RG -- DOI: 10.5281/zenodo.18626839 (version 2) Paper 19: WKB tunneling and LLPO -- DOI: 10.5281/zenodo.18602596 Paper 20: Observable-dependent logical cost, 1D Ising magnetization and WLPO -- DOI: 10.5281/zenodo.18603079 Paper 21: Bell nonlocality and LLPO -- DOI: 10.5281/zenodo.18603251 Paper 22: Markov's Principle and radioactive decay -- DOI: 10.5281/zenodo.18603503 Paper 23: Fan Theorem and optimization -- DOI: 10.5281/zenodo.18604312 Paper 24: Kochen-Specker contextuality and LLPO -- DOI: 10.5281/zenodo.18604317 Paper 25: Ergodic Theorems and Laws of Large Numbers against Countable and Dependent Choice -- DOI: 10.5281/zenodo.18615453 Paper 26: Bidual Gap Detection Is WLPO-Complete: Godel Sequences -- DOI: 10.5281/zenodo.18615457 Paper 27: IVT as the mechanism behind LLPO in Bell physics -- DOI: 10.5281/zenodo.18615459 Paper 28: Classical Mechanics -- DOI: 10.5281/zenodo.18616620 Paper 29: Fekete's Subadditive Lemma -- DOI: 10.5281/zenodo.18643617 Paper 30: Physical Dispensability of the Fan Theorem -- DOI: 10.5281/zenodo.18638394 Paper 31: Physical Dispensability of Dependent Choice -- DOI: 10.5281/zenodo.18645578 Paper 32: QED One-Loop Renormalization: The Landau Pole -- DOI: 10.5281/zenodo.18642598 Paper 33: QCD One-Loop Renormalization and Confinement -- DOI: 10.5281/zenodo.18642610 Paper 34: Scattering Amplitudes Are Constructively Computable -- DOI: 10.5281/zenodo.18642612 Paper 35: The Logical Constitution of Empirical Physics -- DOI: 10.5281/zenodo.18642616 Paper 36: Stratifying Spectral Gap Undecidability (Cubitt's Theorem) -- DOI: 10.5281/zenodo.18642620 Paper 37: The Undecidability Landscape Is LPO -- DOI: 10.5281/zenodo.18642802 Paper 38: Wang Tiling and the Origin of Physical Undecidability -- DOI: 10.5281/zenodo.18642804 Paper 39: Beyond LPO: Thermodynamic Stratification of Physical Undecidability -- DOI: 10.5281/zenodo.18642806