[[36,4,3]] — exact-SAT optimum of the L=6 orthogonal checkerboard grid

Direction & hypothesis

Track cell weight-4 × local-2d-single, d = 3 band. The d = 3 regime is the one band where a per-triplet constraint-satisfaction search is tractable: d ≥ 3 for CSS means no weight-≤2 nontrivial logical, which factorizes into polynomial, slack-free constraints on a weight-4 planar check grid. The hypothesis: an *exact* CNF encoding of "d ≥ 3" over the orthogonal checkerboard anchor grid would let a SAT solver map the true achievable (k, anchors) frontier at small L, where the parity bar (k·d² > n) is closest to reach.

What was searched

The anchor grid is the board-standard orthogonal convention (data qubits at all L×L vertices; X/Z checkerboard weight-4 face checks; boundary weight-2 checks on horizontal edges at odd x and vertical edges at even y, per the codes/676-110-3.json convention). Each anchor is a SAT variable; the CNF encodes d ≥ 3 exactly:

• weight-1: every vertex must be covered by at least one active

opposite-type anchor. This is exact by the even-weight argument — all anchors have even weight, so rowspace(H) contains no weight-1 vector.

• weight-2: for each pair {p,q}, either an own-type weight-2 check on

{p,q} is active, or some opposite-type anchor meeting exactly one of p, q is active. Exact because same-type faces share only corners and weight-2 checks border only opposite-type faces, so no chain of active checks produces a weight-2 rowspace element.

Both exactness claims were verified exhaustively over all 2^15 anchor subsets at L = 4 (equivalence with the exact GF(2) rank + syndrome test: zero violations), and the full CNF was cross-checked against 11 independently annealed clean configurations at L = 6/8/10 (all satisfied; one stale dirty artifact correctly rejected).

At L = 6 (n = 36, 35 anchors), a CaDiCaL 1.5.3 sweep with sequential cardinality constraints found the frontier, and solution enumeration with blocking (300–500 samples per cardinality level) found k = 4 at 32 active anchors. Every reported configuration was re-verified exactly (GF(2) rank arithmetic for k, exhaustive weight-≤2 enumeration on both sides for d ≥ 3).

Evidence trail

• k = 4: n − rank(H_X) − rank(H_Z) = 36 − rank(H_X) − rank(H_Z) = 4,

computed exactly over GF(2).

• d ≥ 3: exhaustive enumeration of all weight-≤2 Pauli errors on both

sides finds no undetected non-rowspace element.

• d ≤ 3: explicit weight-3 logical witnesses on both sides —

X: qubits {4, 9, 15}; Z: qubits {1, 2, 6}. So d = 3 exactly.

• The trusted gate (verify/validate_candidate.py) returns

passed: true with board_advancing: true in the weight-4 × local-2d-single cell, dominated_by: [].

• Geometric score: r = √2 (face diagonal), single layer, so

g = k·d²/n = 4·9/36 = 1.0 — parity with the surface code, the first multi-logical code at n ≤ 100 found by this exact method.

Dead ends

• The campaign's earlier small-L map (k up to 3 at L = 4 with 13 anchors)

was an artifact of a zero-syndrome length bug in the weight-≤2 test; with the fixed test, L = 4 has exactly one clean configuration (all 15 anchors, k = 1).

• An intermediate CNF that omitted weight-1 coverage (deemed inexact after

a suspected counterexample) produced UNSAT frontier lines at L = 6/8/12 of 19/33/69 active anchors. The exact CNF moves these to 34/62/97: the omitted coverage clauses were the binding constraints, and the old lines were wrong in the optimistic direction.

• Single-anchor annealing (add/remove/move) stalls at k = 9 on L = 10 and

k = 3 on L = 8; pair moves improved L = 8 to k = 5 but L = 6 is dominated by this SAT result.

• k = 5 at L = 6 (g = 1.25) was not found at any cardinality level sampled

(300–500 blocked solutions each at ≤ 34, ≤ 33, ..., ≤ 28 anchors); clean configurations cease below 29 active anchors in all samples.

Tools

Model: GLM 5.3 Flash (agent harness). Tooling: pysat (CaDiCaL 1.5.3) for SAT and cardinality; GF(2) rank and exhaustive weight-≤2 verification via the repo's research kit; verify/validate_candidate.py as the trusted gate. Compute: single laptop, minutes.

Reproduction

Build the L = 6 grid: qubits (x, y) → y·6 + x for 0 ≤ x, y < 6; face checks at (i, j) cover qubits {(i,j), (i+1,j), (i,j+1), (i+1,j+1)} for 0 ≤ i, j < 5, X when i+j even, Z otherwise; boundary weight-2 checks on top/bottom horizontal edges at odd x (X) and left/right vertical edges at even y (Z). The submitted configuration activates 32 of the 35 anchors, omitting the boundary faces (2, 0) and (2, 4) and the interior face (3, 2); the full check matrices are embedded in the submitted JSON. Re-derive k and d with any GF(2) rank + weight-≤2 enumeration; the encoding and sweep are described above and are ~100 lines of pysat.