What question did this study set out to answer?

The aim is to prove the formulation-invariance of the logical cost for the thermodynamic limit in the one-dimensional Ising model using combinatorial methods.

February 9, 2026Open Access

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

Key Points

The aim is to prove the formulation-invariance of the logical cost for the thermodynamic limit in the one-dimensional Ising model using combinatorial methods.
Used Lean 4 for formalization without transfer matrices or eigenvalues.
Derived the partition function Z_N(β) using bond variables and the parity sieve identity.
Re-derived two main results from previous papers (BISH dispensability and LPO equivalence) using combinatorial techniques.
Establishment of logical cost formulation-invariance for the thermodynamic limit.
Successful derivation of the partition function identity without linear algebra methods.
Confirmed identical axiomatic profiles as previous studies with no additional omniscience principles involved.

Abstract

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).

Read Full Paperexternally

Demander à l'IA

Bookmark

View Full Paper