Formulation-Invariance of the Logical Cost of the Thermodynamic Limit: A Combinatorial Proof for the 1D Ising Model (Lean 4 Formalization)

Lean 4 formalization proving that the logical cost of the thermodynamic limit for the one-dimensional Ising model is formulation-invariant. The same two results established in Paper 8 via transfer matrices — (A) BISH dispensability of finite-size error bounds, and (B) LPO equivalence of the thermodynamic limit — are re-derived using purely combinatorial methods: finite sums over ±1N, bond variables, and the binomial parity sieve identity. No transfer matrices, eigenvalues, linear algebra, or functional analysis are used. The partition function identity ZN (β) = (2 cosh β) N + (2 sinh β) N is derived from the bond-configuration correspondence and the parity sieve, replacing the spectral decomposition Tr (TN) = λ₊N + λ₋N. The resulting axiom profiles are identical to Paper 8: Part A uses no omniscience principles; Part B establishes LPO ↔ BMC with the same axiom set. The formalization enforces strict formulation independence: no Mathlib modules from LinearAlgebra. * or Analysis. NormedSpace. * are imported. The two formalizations share only the unavoidable common substrate (real arithmetic, LPO/BMC definitions). Contents: 18 Lean 4 source files (1319 lines, 0 sorries), LaTeX source, compiled PDF (16 pages), build infrastructure. Toolchain: Lean 4 v4. 28. 0-rc1, Mathlib4 commit 7091f0f601d5aaea565d2304c1a290cc8af03e18. Part of the constructive reverse mathematics for mathematical physics programme (Papers 2, 7, 8, 9).