Area Law and PEPS

The two theorems

Qudits of dimension q sit on the sites of a finite piece Λ of the square lattice. The Hamiltonian H is a sum of bounded local terms. Its ground vector Ω is unique and separated from the rest of the spectrum by a gap Δ, so that $H - E_{0} \geq Δ (1 - | Ω ⟩⟨ Ω |)$ . Neither theorem assumes a gap on subregions, frustration freeness or translation invariance.

Area-law manuscript · Theorem 1.1

Entanglement obeys an area law

For every region A, the entanglement entropy of the ground state Ω is at most a constant times the number of lattice edges leaving A.

S_{Ω} (A) \leq C (q, R, J, Δ) | \partial_{Λ} A |

Here S_Ω(A) is the entropy of A, and |∂_ΛA| counts the edges leaving A. The constant C depends only on four numbers. They are the qudit dimension q, the range R (each term acts on a set of graph diameter at most R), the bound J on each term's strength, and the gap Δ.

Without such a bound, S could grow like the number of sites in A. The statement is the gap-to-area-law conjecture in two dimensions. Hastings proved the one-dimensional case in 2007. Earlier two-dimensional results assumed frustration-free models with local gaps and gave weaker bounds.

PEPS manuscript · Theorem 1.1

Ground states are polynomial PEPS

A projected entangled pair state on an open square grid: one tensor A_v per site, bonds along grid edges, one physical leg per site.

Take an open L×L grid with on-site and nearest-neighbour terms. Some PEPS Φ, with one tensor per site and bond dimension polynomial in L, matches the whole ground state Ω to error 1/L.

min_{θ} ‖ \frac{Φ}{‖ Φ ‖} - e^{i θ} Ω ‖ \leq L^{- 1}, D_{\max} \leq C L^{c}

Here θ is a global phase, and D_max is the largest bond dimension. The constants C and c depend only on the qudit dimension q, the bound J on each term's strength, and the gap Δ.

An area law bounds each cut separately, while a PEPS has to make all cuts compatible on the given lattice. The result addresses Questions 7–8 of the Cirac–Garre-Rubio–Pérez-García survey tracked in #8273. It asserts existence only, and the tensors need not be efficiently computable.

Checking the papers

Gaps found so far

A machine-checked proof has to state every step. Where the Lean development cannot yet follow a paper exactly, the difference is written up in a paper-gap note. Each entry below says where in the proof it sits, what that step does, and whether it puts the theorem at risk. Most are unfinished Lean work, not problems in the papers.

Sources

References

Earlier work behind the ideas in the proof stages and gap entries above, numbered in order of first citation. A work marked as not cited in the manuscripts is an earlier source for an idea they use without a citation.

The libraries

The formalization is built on these open-source Lean 4 libraries. The tools written for it stay in the libraries, available for the next problem.

Terms used here

For maintainers

Work queue, blocking map, activity and file list

What to do next

Derived from CI, merge state and the blocking graph at the time of the snapshot.

Blocking map

Each issue sits one column to the right of its deepest blocker, in the band of its stream. Select an issue to see what it needs and what it unlocks. The orange chain is the longest run of open prerequisites behind it.

Activity and formalization status

How much has been written, how much has merged, and how much of it the blueprint marks as checked by Lean (\leanok).

Pull requests, cumulative

Lean lines merged, cumulative

Net lines (added minus deleted) in .lean files of merged campaign pull requests. The dashed line counts every file, including blueprint chapters, paper-gap notes and CI configuration.

Blueprint chapters on main

Library	Chapter	Proved	Stated, proof pending	Not formalized	Not ready

Issue	Title	Status	Blocked by	Pull requests