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

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.