n
32
Cell: weight-8 x local-2d-bilayer. At n <= 32 and d >= 4 the weight-8 bilayer cell was led by the two-layer tile code codes/24-10-4.json (k = 10) beside codes/32-8-4.json, codes/30-8-4.json, codes/25-7-4.json, and codes/16-6-4.json. For a full-rank model k = n - 2G, so G=9 forces k >= 14; the column-count bound G >= 2n/(w+1) = 7.1 leaves G=8 (k >= 16) as the last rung that can hold a t >= 2 code.
research/local_sat.py build_local_cnf with the grid site list repeated twice (each of the 16 sites of the 4x4 integer grid carries two qubits at the same coordinate, n = 32; 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=9 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 4x4 grid the farthest sites are 4.24 apart, so the radius constrains nothing and the instance is the weight-bounded CSS search at n = 32 with a bilayer-honest layout by construction), 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 (325,184 variables). First solve SAT after 26.9 s and 32,716 conflicts; ten distinct models in 403.1 s (589,107 conflicts), all k = 14 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 (5,488 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: verifier ok (weight class weight-8, locality class local-2d-bilayer, two qubits per site, measured interaction radius 4.24), no lighter logical in 3,780 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-8 x local-2d-bilayer board". Check weights: X-rows nine of weight 8; Z-rows nine of weight 8. kd^2/n = 7.0. It raises k at (n <= 32, d = 4) in the weight-8 bilayer cell from 10 to 14; every check has weight exactly 8.
G=10 at the same grid and weight yields only k = 12 ([[32,12,4]], dominated). The rung below, G=8 (k >= 16), is the column-count minimum for weight 8 at n = 32 and exhausted the 20,000,000-conflict cap in 9,450 s with neither a model nor an UNSAT proof, so the ladder ends undecided at k = 16 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(4, 9, 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 3c24d908e8234dc4).