#86: a 1,531-edge C4-free subgraph of Q9

Update, 19 October 2026 — superseded, and a correction. A reader's submission (c3u7pu) gives two explicit 1,532-edge C₄-free subgraphs of Q₉; we verified both with our own code (no full face, no vertex pair with two common neighbours, an added edge rejected; a second instrument via A²). So f(9) ≥ 1,532 — the first public explicit certificate at that size we know of. The submission declares that the whole workflow was run by AI agents (DeepSeek), with the account holder directing it. The correction: the number 1,532 was not new on 11 August. Marinari, Parisi and Ritort (cond-mat/9410089, October 1994) report, for the fully frustrated Ising model on the nine-dimensional cube, an annealed state of energy −.494792 ("−380" on their integer scale). With their normalisation that is exactly 1,532 satisfied bonds out of 2,304, and in a fully frustrated model the satisfied bonds meet every square face in one or three edges — a C₄-free subgraph with 1,532 edges, reported as an energy with no configuration. Our 11 August audit read the then-current version of Minamoto's paper (arXiv:2603.29127 v4), the forum, OEIS and the identified construction repository; none mentioned the 1994 result, which entered Minamoto's paper only in its 28 August revision (v5). What was true below: ours was the largest published edge list on its date. The reader's spin configuration reproduces MPR's energy to every printed digit (−95/192), so it is an explicit state at exactly their reported value. Odd-square sets cannot exceed 1,536 at n = 9 (the field bound); averaging over subcubes from Harborth and Nienborg's f(6) = 132, as posted on the problem's forum on 27 August, gives f(9) ≤ 1,584. Details in the reader-q9-1532 bundle.

The target (erdosproblems.com/86, OPEN). The n-dimensional hypercube Q_n has the binary strings of length n as vertices, with edges between strings differing in one coordinate. If f(n) is the largest number of edges in a C₄-free subgraph of Q_n, Erdős asked whether

f(n)≤(1/2+o(1))n·2ⁿ⁻¹.

We do not resolve that asymptotic question. We improve the explicit finite lower bound:

f(9)≥1,531.

The certificate. The graph lists 1,531 distinct pairs in {0,...,511}. Every pair differs in exactly one bit, so every row is a Q₉ edge. Every hypercube four-cycle is one of the square 2-faces, and Q₉ has exactly

C(9,2)·2⁷=4,608

such faces. Exhaustive verification finds no face with all four boundary edges. A separate common-neighbour check enumerates 7,638 length-two endpoint pairs and finds no pair twice. Either calculation proves C₄-freeness.

Twenty-five more edges. This search started from our independently audited 1,506-edge graph and found valid extensions at every integer size through 1,531. The final graph shares 1,084 edges with that predecessor, adding 447 and removing 422. Against the separately frozen public 1,505-edge graph it shares 1,059 edges, adds 472, and removes 446. Thus the new bound is 25 above our preceding certificate and 26 above the identified external one.

Search versus proof. A min-conflicts swap heuristic found the edge set. Its OpenMP schedule is provenance, not proof and not an optimality certificate. The public reproducer instead parses the fixed graph from scratch, checks every endpoint and face, and independently checks common neighbours. It runs the verifier and controlled duplicate, non-edge, and completed-face mutations under normal Python, -O, and -OO. It also rebuilds the heuristic and repeats its deterministic one-thread 1,505-to-1,506 positive control. Bounded attempts to extend the graph to 1,532 were unsuccessful; that says nothing about existence.

Scope. This proves only f(9)≥1,531. It does not determine f(9), prove the graph optimal, or improve the asymptotic upper bound in Problem 86. The current paper, forum, OEIS, and identified construction repository exposed no larger public Q₉ edge list at the audit date. That is a scoped comparison, not a claim that private or unindexed work cannot exist.