Beyond LPO: The Thermodynamic Stratification of Physical Undecidability (Paper 39, Constructive Reverse Mathematics Series)

Paper 39 in the Constructive Reverse Mathematics of Mathematical Physics series. While Papers 36-38 showed all known physical undecidabilities are LPO (Sigma-1-zero), this paper proves the ceiling is not Sigma-1-zero. A modified Cubitt encoding --- running a Turing machine on all inputs simultaneously via Robinson tiling with perimeter counters --- encodes the Sigma-2-zero-complete Finiteness Problem. The generic spectral gap (without promise gap) is Sigma-2-zero/Pi-2-zero-complete, requiring LPO-prime (the Turing jump of LPO). The central result is the Thermodynamic Stratification Theorem: computational complexity bifurcates on thermodynamic scaling. Extensive observables (energy density, magnetization) cap at LPO via Fekete's subadditive lemma, while intensive observables (spectral gap) reach LPO-prime. Crucially, empirical physics --- which operates at finite precision and therefore measures extensive quantities --- remains capped at LPO. Promise-gapped physics (all of Papers 36-38) also caps at LPO. All results formalized in Lean 4 over Mathlib with zero sorry. The formalization comprises 8 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