n
72
Cell: weight-6 x local-2d-bilayer. At n <= 72 and d >= 3 the cell's best k was 22 (codes/64-22-3.json, one layer; 24 in the single-layer [[64,24,3]] submitted from Phase 1 of this campaign), with the two-layer entries at this size sitting lower. For a full-rank model k = n - 2G, so the ladder was run at G = 23, 22, and 21 (k floors 26, 28, 30); the column-count bound G >= 2n/(w+1) = 20.6 makes G=21 the lowest rung that can hold a t >= 2 code, so the ladder ends here.
research/local_sat.py build_local_cnf with the grid site list repeated twice (each of the 36 sites of the 6x6 integer grid carries two qubits at the same coordinate, n = 72; in code, local_sat._grid_sites is replaced by a version that yields every site twice, the one-line layers extension of the single-layer encoder), G=21 checks per side anchored at a grid site and acting within anchor radius 3.5 of it (check diameter at most 7.0, the bilayer cap; on the 6x6 grid the farthest sites are 7.07 apart, so the radius excludes only checks that would span opposite corners), row weight at most 6, CSS commutation, nonzero syndrome for every Pauli error of weight at most 2. CaDiCaL 1.9.5 via python-sat, conflict cap 20,000,000 per solve, 6 h wall cap per solve, CNF streamed into the solver (439,704 variables). First solve SAT after 6,253.6 s and 11,312,692 conflicts; ten distinct models in 7,685 s (14,494,472 conflicts), all k = 30 with d_ub = 3. Model 0 is the code here. The rungs above returned [[72,26,3]] and [[72,28,3]] in 1,430 s and 517 s; both are dominated by this code.
Every weight <= 2 error is detected by the CNF, and an exhaustive enumeration after staging of every X-type and every Z-type error of weight at most 2 (2,628 supports per side, plain GF(2) column sums) found none with zero syndrome, so d >= 3 holds independently of the SAT encoding. research/kit/submit.make_submission (20,000 RIS trials per side, the duplicated coordinates and layers = 2) embedded a weight-3 X-logical and a weight-3 Z-logical, so d = 3 exactly; the file carries confidence upper_bound as the kit labels it. verify/validate_candidate.py: verifier ok (weight class weight-6, locality class local-2d-bilayer, two qubits per site, measured interaction radius 5.83), no lighter logical in 5,380 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-bilayer board". Check weights: X-rows twenty-one of weight 6; Z-rows one of weight 5 and twenty of weight 6. kd^2/n = 3.75. It raises k at (n <= 72, d = 3) in the weight-6 bilayer cell from 24 to 30.
G=20 (k >= 32) lies below the column-count bound and is UNSAT without solving. At weight 8 the same grid and G gives [[72,30,3]] as well (the weight-8 instance solved it in 79 s against 6,254 s here), so the weight-6 code supersedes it in the nested cell; the weight-8 rungs below G=21 remain open and are queued.
research/local_sat.py, research/kit/submit.py, research/kit/surrogate.py, verify/validate_candidate.py. CaDiCaL 1.9.5 via python-sat 1.9.dev15 (Cadical195), CPython 3.12, one core, 1 h 44 min to the first model.
import local_sat
from pysat.solvers import Cadical195
local_sat._grid_sites = lambda side: [(float(x), float(y))
for y in range(side) for x in range(side) for _ in range(2)]
s = Cadical195(bootstrap_with=[])
cnf = local_sat.build_local_cnf(6, 21, 6, 2, 3.5, sink=s, shared_t3=True)
s.conf_budget(20_000_000); assert s.solve_limited()
model = {abs(m) for m in s.get_model() if m > 0}
# HX[g, q] = cnf["xr"][(g, q)] in model; HZ likewise from cnf["zr"];
# coordinates = cnf["sites"] (each grid point twice), layers = 2.
CaDiCaL is deterministic for a fixed clause order; the first model is the code in this file (fingerprint 76a6de8e0eb6e1e8).