n
72
Cell: weight-8 x local-2d-bilayer. At n <= 72 and d >= 4 the weight-8 bilayer cell was led by codes/54-20-4.json (k = 20) beside codes/50-18-4.json and codes/48-16-5.json. For a full-rank model k = n - 2G, so G=24 forces k >= 24; the column-count bound G >= 2n/(w+1) = 16.0 leaves G = 23 down to 16 as rungs that could still hold a code.
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=24 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), row weight at most 8, CSS commutation, nonzero syndrome for every Pauli error of weight at most 3. 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 (9,226,488 variables). First solve SAT after 9,395 s and 785,238 conflicts; ten distinct models in 31,942 s (2,608,453 conflicts), all k = 24 with d_ub = 4. Model 0 is the code here.
Detection of every weight <= 3 error with no weight <= 3 stabilizer gives d >= 4; an exhaustive enumeration after staging of every X-type and every Z-type error of weight at most 3 (62,268 supports per side, plain GF(2) column sums) found none with zero syndrome, so d >= 4 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-4 X-logical and a weight-4 Z-logical, so d = 4 exactly; the file carries confidence upper_bound as the kit labels it. verify/validate_candidate.py against the current board: verifier ok (weight class weight-8, 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-8 x local-2d-bilayer board". Check weights: X-rows twenty-four of weight 8; Z-rows twenty-four of weight 8. kd^2/n = 4.0. It raises k at (n <= 72, d = 4) in the weight-8 bilayer cell from 20 to 24; every check has weight exactly 8.
G=25 at the same grid and weight was still enumerating k = 22 models (dominated) when the machine hosting the run was lost. At weight 6 the same grid walled at both G=25 and G=24: each ran its full 6 h wall cap without a solve returning, so the weight-6 bilayer cell at n = 72 has no d = 4 point from this campaign.
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.
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, 24, 8, 3, 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 2e6f0d603d663297).