The area law for gapped ground states in two dimensions

The area law for gapped ground states asks whether the entanglement entropy of a region in the unique ground state of a gapped local Hamiltonian is bounded by the size of the region's boundary rather than its volume. Hastings proved this in one dimension in 2007. In higher dimensions it has been known only for restricted model classes or under additional assumptions. Two manuscripts in OpenAI's public mathematics collection (github.com/openai/math), dated 24 September 2026, make claims in two dimensions. The first claims an area law on every finite square-lattice domain, assuming only a gap of the full Hamiltonian. The second claims that the corresponding ground states on square grids have tensor-network (PEPS) approximations of polynomial bond dimension. This page summarizes the published claims and lists publicly available follow-up work.

Background

• As recounted in the introduction of A two-dimensional area law from a global spectral gap:
  • The question. For finite-dimensional lattice spins, the gap-to-area conjecture asks for an entropy bound proportional to the boundary area of a unique ground state. The local dimension, interaction range and interaction strength are bounded, and the spectral gap has a positive lower bound independent of the system size. The question grew out of quantum-field calculations of entanglement entropy motivated by black-hole entropy (Bombelli, Koul, Lee and Sorkin; Srednicki).
  • One dimension. Hastings proved a length-independent entropy bound for gapped finite-range chains (2007). Arad, Landau and Vazirani improved the dependence on the inverse gap for frustration-free chains using approximate ground-state projectors, and Arad, Kitaev, Landau and Vazirani extended the approach to general chains. Brandão and Horodecki derived a one-dimensional area law from exponential decay of correlations between separated regions.
  • Higher dimensions. Earlier strict bounds concern restricted classes. Cramer, Eisert, Plenio and Dreißig treated harmonic lattices. Other results add assumptions: Masanes used correlation decay and counts of low-energy states, Brandão and Cramer a heat-capacity hypothesis, and Cho a compatibility condition along growing families.
  • Two dimensions. Anshu, Arad and Gosset proved a subvolume bound for rectangular regions, and then a near-linear bound across vertical cuts. Both concern frustration-free plaquette projector models with a unique ground state and a uniform local gap. The manuscript notes that a local gap is a stronger assumption than a gap of the full system.

The original results

• Area law (24 September 2026). A two-dimensional area law from a global spectral gap, Theorem 1.1. The setting is a finite set Λ of the square lattice with its induced graph, a q-dimensional space at each site, and a Hamiltonian that is a sum of Hermitian terms of norm at most J supported on sets of graph diameter at most R. Suppose the Hamiltonian has a unique ground vector Ω with ground energy E₀ and satisfies H − E₀ ≥ Δ(1 − |Ω⟩⟨Ω|). Then every subset A of Λ satisfies S_Ω(A) ≤ C |∂_ΛA|, where ∂_ΛA is the set of lattice edges crossing from A to its complement in Λ. The constant C depends only on q, R, J and Δ, and is the same for all domains, sets and Hamiltonians.
  • The manuscript stresses that the gap is assumed only for the full Hamiltonian, not for restrictions to smaller regions. The domain may have holes or several components; distances are measured in the induced graph.
  • Corollary 1.2 states the case of on-site and nearest-neighbour interactions on subsets of a finite rectangle. It also gives the vertex-boundary forms S_Ω(A) ≤ 4C |∂_inA| and S_Ω(A) ≤ 2C |Z_A|.
  • Method, as described: the proof bounds the mutual information between a region inside A and everything beyond a suitable collar, including the complement of A. After a set of O(|∂_ΛA|) sites is removed, A is split into two ordered families of regions. Two applications of the entropy chain rule then cancel the individual region entropies. The ingredients are positive quasilocal operators that annihilate the ground vector (Proposition 4.3), information bounds across collars (Propositions 9.6 and 10.2), and the geometric two-family decomposition (Proposition 11.2).
• PEPS approximation (24 September 2026). Polynomial PEPS approximation of gapped square-grid ground states, Theorem 1.1, as summarized in the area-law manuscript. The setting is the open L × L square grid (L ≥ 2) with on-site and nearest-neighbour interactions, local dimension q ≥ 2, term-norm bound J and global gap Δ. Every unique ground vector in this class then has a projected entangled-pair state approximation with maximum bond dimension at most CL^c and global vector error at most L⁻¹, with constants depending only on q, J and Δ. The manuscripts describe it as an existence result that does not assert an efficient construction or contraction algorithm. The proof combines the area-law manuscript's estimates with further compression and routing arguments.
• Sources. Commit 1581d4c of the openai/math repository:
  • A two-dimensional area law from a global spectral gap;
  • Polynomial PEPS approximation of gapped square-grid ground states.
• Formalization in the collection. At commit 1581d4c the collection has no Lean scope note (lean/docs/) and no Comparator challenge for either manuscript.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 17 October 2026)
2026-10-16	AxiomMath/AreaLaw2D (GitHub, commit 1e91b65)	Formalization (third-party Lean)	The README claims Lean 4 proofs of Theorem 1.1 (OpenAI.area_law) and Corollary 1.2 of the area-law manuscript, together with Propositions 4.3, 9.6, 10.2 and 11.2 and the lemmas of Sections 2, 3 and 11. It states that the build contains no sorry and that every result depends only on the axioms propext, Classical.choice and Quot.sound. It names the statement file OpenAI/Statements.lean as the trust boundary. It records the deviations from the paper's conventions in docs/oai265/Memory.md and includes a Comparator pair for Theorem 1.1. Parts of the supporting theory are ported from TNLean and QICLean. The README states that the proofs were produced by Axiom's agent tooling and OpenAI Codex, directed by Ruiz Chen. Lean v4.33.0 with Mathlib and Physlib.	Repository; the build and axiom statements are the repository's own.
Ongoing (commit of 2026-10-16)	TNLean (GitHub, commit 3a71b46), a Lean 4 tensor-network library	Formalization (in progress)	Its blueprint chapter Polynomial PEPS approximation of gapped square-grid ground states follows the PEPS manuscript, with Lean files under TNLean/PEPS/Approximation/. The README calls the library a research formalization in progress, in which some files contain unfinished proofs or results assumed as axioms. AreaLaw2D's README says that TNLean's independent formalization of the area-law manuscript covers Sections 2 to 4 and much of the geometry of Section 11.	Repository (in progress).
2026-10-10	T. Kuwahara, The Rényi area law conjecture is false below α=1 in high dimensions, arXiv:2610.15199v1	Related (Rényi entropies)	In every dimension two and higher, constructs finite-range Hamiltonians with fixed local dimension, bounded interactions, unique ground states and a uniform spectral gap. Their ground states have volume-law Rényi entanglement for 0 < α < 1, while obeying a von Neumann area law. Concludes that α = 1 is the sharp threshold for a universal Rényi area law within this class. Also determines the worst-case rank–error trade-off for approximate ground-state projectors.	arXiv preprint (v1).

Notes

• Theorem 1.1 concerns the von Neumann entropy. According to the preprint's abstract, Kuwahara's Rényi counterexamples obey a von Neumann area law.
• The AreaLaw2D statements are that repository's own encoding of the manuscript; the collection itself contains no formal statement for this family.
• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.