Papers With

← All papers
First page of The Arc Threshold of the Two-Row Ising Torus: Exact Factorization, an Algebraic Critical Coupling, Uniformity in the Circumference, and the Rate of Convergence

The Arc Threshold of the Two-Row Ising Torus: Exact Factorization, an Algebraic Critical Coupling, Uniformity in the Circumference, and the Rate of Convergence

Marco Mandap

math.PR Nov 3, 2026 · v1
formalization mathlib probability physics
Read PDF arXiv abstract
TL;DR
Formalizes in Lean 4/Mathlib the transfer-matrix factorization, characteristic cubic, Cayley–Hamilton recurrence, and 2×2 arc-condition threshold for the two-row Ising torus.
Abstract
The Lee-Yang circle theorem places every zero of a ferromagnetic Ising partition polynomial on the unit circle. The arc condition, that every zero lie in the closed left half-plane, turns the circle theorem into a product formula for the characteristic function of the occupation count and makes it usable for local limit theorems. For the two-row periodic Ising torus we give the exact reflection factorization of the row transfer matrix, reduce the crossing at zeta = i to a real cubic, and identify the critical coupling a_c* = 0.8637850566870... as the unique root in (0,1) of an explicit octic. We prove that every a > a_c* satisfies the arc condition simultaneously for all circumferences, that no smaller coupling does, and that the finite thresholds approach a_c* at the rate C/n^2 with an explicit algebraic constant C. The factorization and the 2x2 threshold are formalized in Lean 4 against Mathlib; the zeta = i reduction, uniformity and rate are analysis-level.
Problem

The arc condition requires every Lee–Yang zero of a ferromagnetic Ising partition polynomial to lie in the closed left half-plane, which makes local limit theorems usable. The question is which couplings satisfy it for the two-row periodic Ising torus, uniformly in the circumference.

Approach

A reflection decomposition splits the 4×4 row transfer matrix into a symmetric 3×3 block plus a scalar, giving a trace formula for the partition polynomial. The crossing at ζ = i reduces to a real cubic whose discriminant factors through an explicit octic. The factorization, characteristic polynomial, Cayley–Hamilton recurrence, and 2×2 threshold are kernel-checked in Lean 4 against Mathlib, with no sorry and only standard axioms. The ζ = i reduction, uniformity, and rate are proved on paper, not in Lean.

Results

The critical coupling a_c* ≈ 0.86378505668702 is the unique root in (0,1) of the octic. Every a > a_c* satisfies the arc condition for all circumferences and no smaller coupling does. The finite thresholds converge to a_c* as C/n^2 with C ≈ 0.1914850, and the 2×2 threshold (√2−1)^{1/4} is formally verified.

na_c(n)# roots in (0,1)n^2(a_c* − a_c(n))
10.80224326292310.06154
20.84035784966510.09371
100.86219356571750.15915
300.863585658848150.17946
Finite-circumference thresholds a_c(n) (selected rows)