Problem. Let \(Z_{16}(z)=\sum_I z^{|I|}\), where \(I\) ranges over independent vertex sets of \(P_{16}\square P_{16}\). Determine the zero of \(Z_{16}\) having least modulus, in a rigorous complex rectangle of diameter at most \(10^{-12}\).
A complete smaller-grid computation supplies a pipeline check and a numerical target near -0.12425.
2Remarks
Remark 1. The polynomial has integer coefficients and degree 128.
Remark 2. If several zeros have equal least modulus, isolate and report all of them.
3What counts as a solution
Provide the exact coefficient vector, certified root isolating rectangles, and a proof that every other zero has strictly larger modulus or belongs to a reported tie.
Current status (A certified radius bracket and an isolated real zero for the sixteen grid). The zero radius lies between 27/256 and 0.122005371541038. A simple real zero is isolated near -0.122005371541037445, while its global least-modulus status remains open.[3]
1Packet records
4 records
Record
Kind
Assessment
The zero radius lies between 27/256 and 0.122005371541038. A simple real zero is isolated near -0.122005371541037445, while its global least-modulus status remains open.
Result
Evidence: Reproduced
A replay is recorded for this computation. Inspect the replay record for its procedure and scope.
claim · Computation 1
The zero radius lies between 27/256 and 0.122005371541038. A simple real zero is isolated near -0.122005371541037445, while its global least-modulus status remains open.[3]
Relevance to this problem
For Nearest hard-square partition-function zero for the sixteen grid, record hs16-claim-certified-radius-bracket (“A certified radius bracket and an isolated real zero for the sixteen grid”) records a bound, answer, status fact, or structural consequence. The record states: The zero radius lies between 27/256 and 0.122005371541038.
Evidence
ReproducedA replay is recorded for this computation. Inspect the replay record for its procedure and scope.
Record state
partial
Scope
the independence polynomial of the single graph P16 Cartesian-product P16, with a local certificate for one zero and a universal maximum-degree zero-free disk
Let \(\rho_{16}=\min\{|z|:Z_{16}(z)=0\}\). Exact row-mask transfer gives all 129 integer coefficients of \(Z_{16}\). An exact rational Rouché calculation isolates a simple real zero in
\[
[-0.122005371541038,-0.122005371541037]+i[-10^{-15},10^{-15}].
\]
The rectangle has diameter below \(3\mathbin{\cdot}10^{-15}\).
The grid has maximum degree four. The Shearer disk bound, in the independent-polynomial form developed by Scott and Sokal, gives
\[
Z_{16}(z)\ne0\qquad\text{for }|z|<\frac{(4-1)^{4-1}}{4^4}=\frac{27}{256}.
\]
Consequently,
\[
\frac{27}{256}\leq\rho_{16}\leq0.122005371541038.
\]
The local Rouché disk proves that the displayed zero is simple. It does not count the other 127 zeros or exclude a nonreal zero in the remaining annulus. The requested least-modulus identification remains open in this fixture.
The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.
Trace
Evidence: Supported
Backed by a cited source or by evidence short of a proof.
attempt · Route 1
The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.[1][2][3]
Relevance to this problem
For Nearest hard-square partition-function zero for the sixteen grid, record hs16-attempt-literature-audit (“Primary literature supports the model, transfer, and zero-free disk”) documents a concrete method, search boundary, or failed route. The record states: The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound.
Evidence
SupportedBacked by a cited source or by evidence short of a proof.
Baxter, Enting, and Tsang study the hard-square lattice gas and its activity expansion on the square lattice. Calkin and Wilf assemble grid independent sets with compatible row or column masks and evaluate the total at activity one. Adding the monomial weight \(z^{|m|}\) gives the coefficient transfer used here.
Scott and Sokal connect the hard-core partition function with the Lovász local lemma and present the Shearer-Dobrushin nonvanishing criterion. For maximum degree four, its uniform specialization supplies the disk \(|z|<27/256\).
Focused searches covered the exact graph name, finite hard-square partition zeros, independence-polynomial zeros for square grids, and the cited papers' references. No primary source located in this audit gives the nearest zero of \(P_{16}\mathbin{\square}P_{16}\). Publication novelty and the exact least-modulus value remain unverified.
A short C++17 program computes all coefficients with unsigned 256-bit addition and a subset zeta transform.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 1
A short C++17 program computes all coefficients with unsigned 256-bit addition and a subset zeta transform.[3]
Relevance to this problem
For Nearest hard-square partition-function zero for the sixteen grid, record hs16-artifact-exact-polynomial (“Exact 2,584-mask transfer polynomial”) supplies evidence or a replay used to check the packet. The record states: A short C++17 program computes all coefficients with unsigned 256-bit addition and a subset zeta transform.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
all independent sets of P16 Cartesian-product P16, grouped exactly by cardinality through a 2,584-mask row transfer
Join source_lines with newline characters, save as hs.cpp, run clang++ -O3 -std=c++17 hs.cpp -o hs, then run ./hs > hs16_coefficients.json
Runtime
Clang or GCC with C++17 and unsigned __int128 support
Details
A row state is a sixteen-bit mask \(m\) satisfying \(m\mathbin{\&}(m\ll1)=0\). There are 2,584 such masks. If \(F_r(m;z)\) counts configurations on the first \(r\) rows ending at \(m\), then
\[
F_{r+1}(m;z)=z^{|m|}\sum_{s\mathbin{\&}m=0}F_r(s;z).
\]
The program evaluates every compatibility sum by a subset zeta transform over all \(2^{16}\) masks. Each coefficient is below the total number of subsets \(2^{256}\), so four unsigned 64-bit limbs suffice. The coefficient order is increasing degree.
The run gives \(Z_{16}(1)=18396766424410124752958806046933947217821482942\). Its comma-separated coefficient vector has SHA-256 `a65ab0dc72ec69b3408416bfc816478869e6542f1076592842277e109c515d96`. Compiling the same source with `-DGRID_SIDE=12` reproduces the candidate record's twelve-grid count and coefficient hash.
Fraction arithmetic proves one zero in a radius 5e-14 disk, then places its real representative in a rectangle of diameter below 3e-15.
Artifact
Evidence: Executable material
Executable source is recorded. Inspect its inputs and instructions before attempting a replay.
artifact · Artifact 2
Fraction arithmetic proves one zero in a radius 5e-14 disk, then places its real representative in a rectangle of diameter below 3e-15.[3]
Relevance to this problem
For Nearest hard-square partition-function zero for the sixteen grid, record hs16-artifact-root-enclosure (“Exact rational Rouché enclosure for one simple zero”) supplies evidence or a replay used to check the packet. The record states: Fraction arithmetic proves one zero in a radius 5e-14 disk, then places its real representative in a rectangle of diameter below 3e-15.
Evidence
Executable materialExecutable source is recorded. Inspect its inputs and instructions before attempting a replay.
Record state
available
Scope
one local complex disk and one contained rational rectangle near -0.122005371541037445 for the exact degree-128 polynomial Z16
Place the transfer output at hs16_coefficients.json, join source_lines with newline characters, save as certify.py, and run python3 certify.py
Runtime
CPython 3.8 or later, standard library only
Details
Put \(c=-0.12200537154105\), \(R=5\mathbin{\cdot}10^{-14}\), and expand
\[
Z_{16}(c+t)=\sum_{j=0}^{128}b_jt^j
\]
with exact rational \(b_j\). On \(|t|=R\), the linear part obeys
\[
|b_0+b_1t|\geq |b_1|R-|b_0|.
\]
The exact calculation proves that this lower bound exceeds \(11298452952\) times \(\sum_{j\geq2}|b_j|R^j\). The linear zero lies inside the circle, so Rouché's theorem gives exactly one zero there, counted with multiplicity.
Exact endpoint signs place a real zero between -0.122005371541038 and -0.122005371541037. The stated rectangle lies inside the Rouché disk. It therefore contains that zero and no second zero.
Original intake status. UNKNOWN as of 2026-07-25. The zero radius lies between 27/256 and 0.122005371541038. A simple real zero is isolated near -0.122005371541037445, while its global least-modulus status remains open. The checked sources do not settle the full acceptance condition.
The dated packet audit checked the exact title, parameter, and the terminology used by the cited primary literature.
The strongest recorded neighboring result is: The zero radius lies between 27/256 and 0.122005371541038. A simple real zero is isolated near -0.122005371541037445, while its global least-modulus status remains open.
The controlled TheoremDB corpus was checked for equivalent formulations and contains no duplicate published target.
Recorded example 1. At z=1, the polynomial counts all independent sets.
Computational notes
Exact row-mask transfer for the 12 by 12 grid produced degree 72 and Z_12(1)=162481813349792588536582997. The serialized coefficient vector has SHA-256 c36cdf2efa005e88c21469a24059de8c03f63010de218a42ac3e990411d1e820. Forty-digit numerical roots placed the least-modulus candidate at -0.1242498124533312648219610478237016098572.
How the 4 records connectThe overview places each record once. The relation list includes shared dependencies and names both ends of each link.
ProblemNearest hard-square partition-function zero for the sixteen grid
Contribute to this problemCite this problem statement
Cite the original sources separately.
Plain text
“Nearest hard-square partition-function zero for the sixteen grid.” TheoremDB. P2718. Problem statement; statement text SHA-256 846f0a4b8ba0ab7c95ac3bb5af4956b7fc78e0dcf9c7f418cbe0a770a7603983. https://theoremdb.org/statement/?ref=P2718
BibTeX
@misc{theoremdb-problem-846f0a4b8ba0ab7c95ac3bb5af4956b7fc78e0dcf9c7f418cbe0a770a7603983,
title = {{Nearest hard-square partition-function zero for the sixteen grid}},
howpublished = {TheoremDB},
note = {Problem statement; statement text SHA-256 846f0a4b8ba0ab7c95ac3bb5af4956b7fc78e0dcf9c7f418cbe0a770a7603983},
url = {https://theoremdb.org/statement/?ref=P2718}
}
Once Lean accepts the draft, you can submit it while target review is pending. Your submission request is saved and continues after approval. Private checks stay private until you choose to submit.
1References
R. J. Baxter, I. G. Enting, and S. K. Tsang, “Hard-square lattice gas”. Journal of Statistical Physics 22(4) (1980), 465-489. DOI 10.1007/BF01012867. R. J. Baxter, I. G. Enting, and S. K. Tsang, Hard-square lattice gas, Journal of Statistical Physics 22(4) (1980), 465-489; Neil J. Calkin and Herbert S. Wilf, The Number of Independent Sets in a Grid Graph, SIAM Journal on Discrete Mathematics 11(1) (1998), 54-60; Alexander D. Scott and Alan D. Sokal, The repulsive lattice gas, the independent-set polynomial, and the Lovasz local lemma, Journal of Statistical Physics 118 (2005), 1151-1261. ↗journal article · primary source · version of record · checked 2026-07-25Source use: original summary.Primary literature supports the model, transfer, and zero-free disk. The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.Also cited at Journal of Statistical Physics 22(4) (1980), 465-489.For Nearest hard-square partition-function zero for the sixteen grid: The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.
Neil J. Calkin and Herbert S. Wilf, “The Number of Independent Sets in a Grid Graph”. SIAM Journal on Discrete Mathematics 11(1) (1998), 54-60. DOI 10.1137/S089548019528993X. SIAM Journal on Discrete Mathematics 11(1) (1998), 54-60, Section 1. ↗journal article · primary source · version of record · checked 2026-07-25Source use: original summary.Primary literature supports the model, transfer, and zero-free disk. The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.For Nearest hard-square partition-function zero for the sixteen grid: Primary literature supports the model, transfer, and zero-free disk. The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.
Packet source. Alexander D. Scott and Alan D. Sokal, The repulsive lattice gas, the independent-set polynomial, and the Lovasz local lemma. Journal of Statistical Physics 118 (2005), 1151-1261. ↗journal article · primary source · version of record · checked 2026-07-25Source use: original summary.Primary literature supports the model, transfer, and zero-free disk. The located sources supply the hard-square setting, compatible-mask transfer, and universal disk bound. None reports the finite 16 by 16 nearest zero.Also cited at Exact transfer in hs16-artifact-exact-polynomial and rational Rouché certificate in hs16-artifact-root-enclosure.Also cited at Inline C++17 exact computation executed on 2026-07-25.Also cited at Inline Python 3 rational certificate executed on 2026-07-25.Source named by the research packet.
Original CC0 certified finite-volume partition-function target.
Discussion
Loading
Past commenters and subscribers receive notifications when someone comments.