The Logical Cost of the Thermodynamic Limit: LPO-Equivalence and BISH-Dispensability for the 1D Ising Free Energy — A Lean 4 Formalization

We prove two complementary results about the thermodynamic limit of the one-dimensional Ising model, formalized in Lean 4 with Mathlib. (A) Dispensability. The finite-size error bound |f_N(β) − f_∞(β)| ≤ (1/N)tanh(β)^N is provable in Bishop-style constructive mathematics (BISH) without any omniscience principle. A constructive witness N₀ for any prescribed accuracy ε > 0 is explicitly computed. (B) Calibration. The existence of the thermodynamic limit as a completed real number is equivalent over BISH to the Limited Principle of Omniscience (LPO), via the known equivalence between LPO and bounded monotone convergence (Bridges–Vîță 2006) instantiated through the Ising free energy function g(J) = −log(2 cosh(βJ)). Together, these results establish that the LPO cost of the thermodynamic limit is genuine (it is equivalent to, not merely sufficient for, a known omniscience principle) and dispensable (the empirical content requires no omniscience). The archive contains: 18 Lean 4 source files (1374 lines total, 0 errors, 0 warnings, 0 sorries) LaTeX source and compiled PDF (17 pages) Build instructions (ZENODO_README.md) Axiom profile: Part A and the backward direction of Part B use only Lean's foundational axioms [propext, Classical.choice, Quot.sound]. The forward direction (LPO → BMC) is axiomatized citing Bridges–Vîță 2006. This is Paper 8 in a constructive reverse mathematics series. Companion papers: Paper 2 (WLPO ↔ bidual gap in ℓ¹), Paper 7 (WLPO via trace-class non-reflexivity).