Frustration-freeness is decidable but unprovable

The paper in detail

Write \(a_L=0\) if the \(L\times L\) Hamiltonian is frustration-free and \(a_L=1\) otherwise. With open boundaries the sequence is monotone. If a state of the large lattice is annihilated by every bond, every eigenvector of its reduced density matrix on a smaller square is annihilated by the bonds inside it, since the terms are positive semidefinite. So the sequence is all zeros, or zeros up to a first frustrated size and ones afterwards. Finding a frustrated size proves the answer is no, but no finite search over sizes proves it is yes.

Decidability comes from algebra. Stack all embedded bond terms into one tall matrix \(M_L\). The system is frustration-free exactly when \(M_L\) has a nonzero kernel, that is when every maximal square minor vanishes. Each minor is a polynomial in the \(2d^4\) matrix entries of the two local terms, a number of variables that does not grow with \(L\). Hilbert's basis theorem then says that the infinitely many polynomial conditions, one family per size, have the same common zeros as a finite subfamily, which lives at sizes up to some \(L(d)\). By monotonicity it suffices to test the single size \(L(d)\).

Unprovability comes from tilings. Give each Wang tile a basis state, and penalise forbidden neighbouring pairs with diagonal projectors. The Hamiltonian is then frustration-free at every size exactly when the tiles cover the plane. With a standard construction, that happens exactly when a chosen Turing machine never halts. Take the machine that searches for a contradiction in ZFC. Its Hamiltonian is frustration-free if and only if ZFC is consistent, and ZFC proves this equivalence. A ZFC proof of frustration-freeness would therefore be a ZFC proof of its own consistency, which Gödel's second incompleteness theorem rules out.

The apparent clash is resolved by uniformity. If \(L(d)\) were computable, frustration-freeness would be decidable with \(d\) as part of the input, but the tiling reduction shows that this version is undecidable. Halting machines with \(m\) states that use \(\mathrm{BB}(m)\) tape cells give tile sets that fail only at large sizes, which forces \(L(am+b)\ge\mathrm{BB}(m)\). For the dimension \(d^*\) of the unprovable example, ZFC proves that a cutoff exists but cannot prove any specific integer is one. Open directions include explicit cutoffs for small \(d\), and whether genuinely quantum, non-commuting terms change the picture.

Transferable methods

1. Hilbert's basis theorem turns all system sizes into finitely many

   Each size gives finitely many polynomial conditions on the local terms, but there are infinitely many sizes. Because the number of variables stays at \(2d^4\), all the conditions live in one polynomial ring. In that ring every ideal is finitely generated, so the infinite family collapses to a finite one.

   Let \(N_L=d^{L^2}\) and \(B_L=2L(L-1)\). Stack the embedded bond operators into the \(B_LN_L\times N_L\) matrix \(M_L\). Frustration-freeness is the existence of \(v\ne0\) with \(M_Lv=0\), which is equivalent to \(\operatorname{rank}M_L<N_L\). That holds exactly when \(\det M_L[I]=0\) for every choice \(I\) of \(N_L\) rows. Each entry of \(M_L\) is linear in the entries \(h^{(a)}_{pq,rs}\), so each such determinant is a polynomial of degree \(N_L\) in \(2d^4\) variables. Hermiticity and positivity are imposed separately and do not enter the polynomials.

   Let \(P_L\) be the set of these determinants and \(\mathcal P=\bigcup_{L\ge2}P_L\). Because \(\mathbb C[x_1,\dots,x_{2d^4}]\) is Noetherian, there is a finite \(\widetilde{\mathcal P}\subseteq\mathcal P\) generating the same ideal, and therefore \(Z(\mathcal P)=Z(\widetilde{\mathcal P})\). The finite set lies in \(\bigcup_{L\le L^*}P_L\) for some \(L^*\), so frustration-freeness up to \(L^*\) implies it at every size. Monotonicity reduces this to the single size \(L^*\).

   Editorial remark: equivalently, the ideals \(I_{\le L}\) generated by \(\bigcup_{L'\le L}P_{L'}\) form an ascending chain that must stabilise. The theorem guarantees that the chain stops but gives no bound on where, and that is the non-constructive step that Theorem 4 shows cannot be removed. Editorial check: for 40 random pairs of complex projectors on a \(2\times2\) lattice with \(d=2\), rank deficiency of the stacked matrix agreed with zero ground energy in every case.

   How to reuse it

   Whenever a property for all system sizes is the common zero set of polynomials in a fixed, size-independent set of parameters, Hilbert's basis theorem gives a finite cutoff. An explicit cutoff needs extra structure, such as degree bounds or Gröbner bases, and this paper shows that such structure can be provably absent.

2. Encoding a consistency proof search in tiles

   To make a true statement unprovable, the paper makes frustration-freeness equivalent to a statement ZFC cannot prove: its own consistency. Wang tiles translate non-halting into tiling the plane, and a diagonal penalty Hamiltonian translates tiling into frustration-freeness.

   For tiles \(A^1,\dots,A^n\) take \(d=n\) and \[h^{(a)}=\sum_{(p,q)\in F_a}\lvert A^pA^q\rangle\langle A^pA^q\rvert,\] where \(F_a\) lists the forbidden neighbouring pairs in direction \(a\). The terms are diagonal and commute, and the zero-energy states of \(H_L\) are superpositions of legal \(L\times L\) tilings. So \(H_L\) is frustration-free exactly when a legal tiling of that square exists. Editorial remark: legal tilings of every finite square give a tiling of the plane by a compactness (König's lemma) argument, which is why "all sizes" matches "the plane".

   Let the machine \(T_{\rm ZFC}\) enumerate ZFC proofs and halt if it finds one of \(0=1\). Its tile set yields a Hamiltonian \(H_{\rm ZFC}\) with \[H_{\rm ZFC}\ \text{frustration-free}\iff T_{\rm ZFC}\ \text{never halts}\iff\operatorname{Con}(\mathrm{ZFC}).\] ZFC proves the equivalence, so ZFC proving the left side would mean ZFC proves \(\operatorname{Con}(\mathrm{ZFC})\). Gödel's second theorem forbids this if ZFC is consistent, and in that case the left side is true.

   The same reduction bounds the cutoff from below. A halting \(m\)-state machine that needs \(k\) tape cells gives tiles that cover every square of side below \(k\) but not the plane, so \(L(am+b)\ge\mathrm{BB}(m)\). Editorial toy check: with tiles \(0,\dots,d-1\) and horizontal pairs \((t,t+1)\) as the only legal ones, rows must count upward, so the counts of legal \(L\times L\) tilings are \(2,1,0\) for \(d=2\), \(3,4,1,0\) for \(d=3\) and \(4,9,8,1,0\) for \(d=4\). The first frustrated size is \(d+1\). Turing-machine tiles turn this linear delay into busy-beaver growth.

   How to reuse it

   To show that a property of local Hamiltonians for all sizes is undecidable or unprovable, reduce from tiling. Diagonal penalty Hamiltonians are enough, so the obstruction is combinatorial rather than quantum, and it survives any restriction that still contains classical tile models.

Source: Methods: "Frustration-free problem as common zeros", "Noetherianity and Hilbert's basis theorem", "Wang tiles and Turing machines" and "Scaling of L(d)". Based on the linked paper version. Derivations marked as editorial, and suggested uses in other problems, are editorial guidance rather than results of the paper.

Context & limitations

Why it matters. It gives a natural physics question on which decidability and provability come apart. A correct decision procedure exists for every local dimension, but for some dimension no particular integer can be proved to be a valid cutoff, so the procedure cannot be certified. Many results on gaps and Hall response assume frustration-freeness. The paper shows the property can hold without being provable in standard mathematics, even for a classical tiling-type Hamiltonian.

Limitations. The decidability proof is a pure existence argument from Hilbert's basis theorem and gives no value of \(L(d)\), not even for \(d=2\). Inputs are restricted to algebraic matrix entries, open boundaries and the square lattice (the author notes the argument extends to fixed sequences of graphs). The unprovable example encodes a proof search for ZFC in Wang tiles, so its local dimension is enormous and not stated. The paper is a short letter: the tiling construction and the busy-beaver scaling rest on cited constructions that the entry did not check. The author states that ChatGPT (GPT-5.4, GPT-5.5 Pro, GPT-5.6 Sol and GPT-6 Astra) was used to establish the decidability result and to clarify how it is consistent with the unprovability result.

Description based on the full arXiv HTML of v1, read 2026-11-06: main text, Methods (polynomial formulation, Hilbert's basis theorem, Wang tiles, non-uniform decidability, scaling of the cutoff) and the AI declaration. The cited tiling constructions [28, 39, 40] were not checked.