n
50
Cell: weight-6 x local-2d-bilayer. At n <= 50 and d >= 4 the weight-6 bilayer cell was led by codes/48-12-4.json (k = 12) beside codes/25-7-4.json, codes/36-10-4-b.json, and codes/30-8-4.json. For a full-rank model k = n - 2G, so G=17 forces k >= 16; the column-count bound G >= 2n/(w+1) = 14.3 leaves G = 16 and below 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 25 sites of the 5x5 integer grid carries two qubits at the same coordinate, n = 50; 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=17 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 5x5 grid the farthest sites are 5.66 apart), row weight at most 6, 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 (2,231,690 variables). First solve SAT after 10,493 s and 2,923,043 conflicts; ten distinct models in 47,101 s (13,057,176 conflicts), all k = 16 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 (20,875 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-6, locality class local-2d-bilayer, two qubits per site, measured interaction radius 5.66), no lighter logical in 4,500 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-bilayer board". Check weights: X-rows one of weight 5 and sixteen of weight 6; Z-rows one of weight 4 and sixteen of weight 6. kd^2/n = 5.12. It raises k at (n <= 50, d = 4) in the weight-6 bilayer cell from 12 to 16.
G=18 at the same grid and weight yields only k = 14 (dominated). The rung below, G=16 (k >= 18), ran for its full 6 h wall cap without a solve returning, so k = 18 at d = 4 on this grid is open rather than excluded.
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(5, 17, 6, 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 cc0383f53d337e0d).