Tensor networks sharpen a mathematical guarantee for the Haldane gap

What is being guaranteed?

The study concerns the spin-1 Heisenberg antiferromagnetic chain: a mathematical model of quantum spins interacting with their nearest neighbors. For the main result, the chain closes into a ring. Its spectral gap is the energy difference between the lowest-energy state and the next level, with energies counted according to their multiplicity.

The important question is whether that gap stays above a fixed positive number as the ring grows. A small ring can have a gap even when the gap approaches zero at larger sizes. Establishing a uniform lower bound therefore requires more than calculating a few examples.

Lu reports that the gap exceeds 0.0729 for every even ring length of at least 36 sites, with the exchange coupling set to one. The result also establishes a unique ground state for those rings. Compared with the earlier guarantee of approximately 0.003821 for even rings of at least 2,304 sites, the lower bound is about nineteen times larger and applies from a much smaller size.

This is not a measurement or an exact calculation of the gap. The paper cites a bulk numerical estimate near 0.4105. The new result raises the rigorously guaranteed floor without claiming to reach that estimate.

Reading a calculation in two directions

The starting point is a computer-assisted proof attributed to OpenAI. Lu reports independently reproducing and verifying its finite numerical inputs in exact arithmetic, then translating the argument into tensor-network diagrams.

These diagrams organize a large calculation into connected local pieces. Here they represent the partition function, which sums energy levels weighted by temperature. The same network can be read along the chain or along imaginary time, a mathematical direction related to inverse temperature rather than a laboratory clock.

The proof tracks two quantities called purities. Thermal purity describes how concentrated the thermal state's probabilities are. When it is sufficiently close to one, a single energy level dominates strongly enough to establish both ground-state uniqueness and a positive gap. A related spatial purity provides control as the chain length increases.

The crucial mechanism is squaring and renormalizing these distributions, which makes small departures from purity shrink quadratically. An identity connecting the two ways of assembling the network couples length doubling to inverse-temperature doubling. Additional inequalities cover the even lengths between successive doublings, so the conclusion is not restricted to a sparse sequence of ring sizes.

Small inputs, large conclusions

For the spin-1 model, the finite evidence includes certified partition-function traces on rings of four to twelve sites and matrix-product trial states on 72 and 120 sites. Those trial states bound the ground-state energy without requiring the entire spectrum of the larger systems.

Tighter bounds on the spatial transfer spectrum, a temperature-lifting argument and separate estimates across length intervals produce the improved 0.0729 guarantee from the same finite inputs.

Lu identifies reflection positivity as the structural condition enabling the spatial inequalities. In the reformulation, it produces a transfer matrix of the form of a matrix multiplied by its transpose, ensuring nonnegative eigenvalues. But reflection positivity alone does not guarantee a gap: a suitable finite numerical starting point is also essential.

The paper reports certified uniform bounds for seven additional models, including dimerized chains, spin ladders and Ising systems. These are results for specified interactions and parameters, not blanket guarantees for every member of those model families.

What the computer has checked

Lean 4 formalizes the general argument and checks the rational inequalities that propagate finite starting bounds to arbitrarily large systems. The scope of that verification matters. For the spin-1 result, some short-ring numerical inputs remain explicit hypotheses supported by calculations outside Lean; the strongest bound also uses externally verified seed calculations. It is not presented as an entirely self-contained kernel check of every numerical ingredient.

The mixed-field Ising example goes further: the paper reports that Lean checks its finite seed arithmetic too, giving an unconditional result within the formalization.

The work is an arXiv preprint submitted on November 8, 2026; the supplied record does not establish peer review. It reports mathematical and computational results, not experiments. Its central contribution is a clearer mechanism for turning finite calculations into guarantees across unbounded system sizes, together with explicit boundaries on what has been formally checked.