Certified structure and a certified algorithm for the hard-square lattice gas

Abstract

We report three results on the Z² hard-core (hard-square) lattice gas, each carried to completion by an exact-rational and certified-interval arithmetic discipline — never an unverified floating-point approximation. First, for the finite-strip transfer matrix of this model at widths L=2,3,4,5, we certify a branch point at every width, and for L=3 and L=4 we prove the Beraha–Kahane–Weiss dominance hypothesis continuously across the entire path from z=0 to the branch point, with no remaining gap at either width — combining a certified eigenvector-overlap bridge argument, a certified continuous root-exclusion bound, and a desingularizing coordinate blow-up with an explicit seam certificate. For L=5, the same bridge argument covers 84.00% of the path continuously, and all 12 remaining sampled points are now certified dominant via an exact-deflation Cauchy-coefficient bound, with one point additionally requiring a Dandelin–Lobachevsky–Graeffe root-squaring step. Second, we certify a depth-indexed sequence of upper bounds on the exact spectral radius of a bounded-memory relaxation of the Weitz self-avoiding-walk tree on Z² (under the Sinclair–Srivastava–Štefankovič–Yin walk-relative edge ordering), reaching ≤2.435510 at depth L=25, bracketed to within 4×10⁻⁶ of the true spectral radius. We prove a theorem identifying this sequence's limit, as the retention depth grows, with the exact (unrelaxed) tree's own growth rate. Third, we prove a zero-free-disk theorem (radius 0.112591, exceeding the generic degree-4 Scott–Sokal bound 27/256≈0.10547) and build from it a deterministic approximation algorithm for the independence polynomial inside the disk, with a rigorous relative-error guarantee valid for complex activities, achieving measured empirical speedups of up to 1258.7× at n=25 against brute force on consumer laptop hardware (Apple M3 Pro, 18GB RAM — not a cluster, server, or HPC allocation). Two of the three results — the Weitz-tree bound and the zero-free-disk theorem underlying the approximation algorithm — reuse one finite-type-automaton/bisimulation-compression construction, unmodified, across two structurally distinct recursions; the strip transfer matrix's own row-state space is small enough at every tested width that no compression step is needed there. Full certification methodology, every certificate's exact scope (what it does and does not establish), and hardware disclosure are given in the paper. A machine-checked reproduction package (pinned source, per-file hashes, and a documented clean-environment rebuild/re-run) accompanies this deposit, covering the paper's §2 and §4 results in full and §3's L=3, L=4, and L=5 dominance results; §3's L=2 claim and its representation-audit check are not yet packaged and are disclosed as such in the package's own MANIFEST.Version 1.1 (5 October 2026). Adds Section 2.6: the certified growth bounds are exported as third-party-checkable CW1 certificates (L = 5, 7, 9, 11) and the Collatz-Wielandt check is reproved in Lean 4 + Mathlib, with the L = 9 certificate verified in the Lean kernel (axioms propext, Classical.choice, Quot.sound). Corrects the strip transverse boundary in Section 3 from periodic/torus to free/cylinder - the boundary the released source has always computed; no previously reported value changes, and the brute-force validation is shown to have used the same matrix. Also names the twist convention and other small textual points raised by an external reproduction (38 of 38 checks passing) by G. Ward's One Beam lab, whose script and output are included. See CHANGELOG_v1.1.md.