← All papers
First page of Spectral Gap of the Hexagonal AKLT Model via Boundary-State Factorization

Spectral Gap of the Hexagonal AKLT Model via Boundary-State Factorization

Michael J. Kastoryano

quant-ph Sep 23, 2026 · v1 math-ph
A Lean 4 proof certificate verifies the scalar Kotecký–Preiss summability and root-counting estimates, including geometric and counting inputs, used for the AKLT gap.
We establish a sufficient condition under which overlapping PEPS boundary states satisfy the approximate factorization criterion for a spectral gap. The condition is formulated in terms of the boundary response induced by cutting bonds through the center of a rectangular region. We decompose this response into a contribution common to all four associated regions and a remainder measured in the instantaneous boundary metric. A single linear transport absorbs the common contribution and yields compatible factorization operators, with an error controlled solely by the remainder. We apply this framework to Ising PEPS and to the spin-3/2 AKLT model on the hexagonal lattice. For Ising PEPS, the required boundary-response estimate reduces to a Dobrushin-Shlosman-type condition. For the hexagonal AKLT model, a rooted expansion in paths and loops isolates the common response, while a local comparison of boundary states together with a scalar Kotecký-Preiss estimate controls the remaining terms. In both cases, the factorization error decays exponentially with the overlap width, up to a prefactor proportional to the cut length. For AKLT, we establish the corresponding physical projector estimate and obtain a uniform spectral gap. For Ising PEPS, the gap implication additionally requires compatible injective regional contractions, as specified in the paper. More generally, the method provides a systematic route from locality of PEPS boundary response to spectral gaps of two-dimensional parent Hamiltonians.

Proving a uniform spectral gap for the spin-3/2 AKLT model on the hexagonal lattice requires boundary estimates beyond decay of correlations. Earlier proofs relied on numerical certification or on decorated lattices.

A sufficient condition for approximate factorization of overlapping PEPS boundary states is formulated via the boundary response to cutting bonds through a region's center. The response is split into a common part absorbed by a linear transport and a remainder. For AKLT, a rooted path-and-loop expansion with a scalar Kotecký–Preiss estimate controls the remainder. The scalar summability theorem, with its geometric and counting inputs, is machine-checked in Lean, while the operator-level arguments remain on paper.

Factorization error decays exponentially in overlap width, giving a uniform spectral gap for the hexagonal AKLT model and a Dobrushin–Shlosman-type criterion for Ising PEPS. Lean certifies the KP inequality, per-edge root bound, and rooted summability constant uniformly over rectangles and cuts.