n
49
Cell: weight-8 x local-2d-single. The d=4 points in this cell were codes/16-6-4.json (weight 8) and codes/36-12-4.json (weight 8) beside the weight-6 entries that nest into it; nothing sat at n=49. For a full-rank model k = n - 2G, so k >= 13 (one above [[36,12,4]]) needs G <= 18, and the column-count bound for weight 8 at n=49 (G >= 2n/9 = 10.9) leaves that open. The weight-6 instance at the same G had been running for hours without an answer when this one was queued as the last rung of the Phase 1 list.
research/local_sat.py build_local_cnf(7, 18, 8, 3, 2.0, shared_t3=True): 7x7 grid, 18 checks per side anchored within radius 2.0 (interaction radius at most 4.0 by construction), row weight at most 8, CSS commutation, nonzero syndrome for every Pauli error of weight at most 3 (2,182,954 variables, 8,409,697 clauses, 21 s to build, about 3 GB RSS). CaDiCaL 1.9.5 via python-sat, conflict cap 20,000,000 per solve, 6 h wall cap per solve. First solve SAT after 649.1 s and 233,788 conflicts; ten distinct models in 2,929 s (778,144 conflicts), all k = 13 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 (19,649 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) 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-single, interaction radius 4.0), no lighter logical in 4,460 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-8 x local-2d-single board". Check weights: X-rows 4, 4, 5, seven of weight 6, 7, 7, six of weight 8; Z-rows 4, 4, 5, six of weight 6, 7, 7, 7, six of weight 8. kd^2/n = 4.24. It does not enter the weight-6 cell.
The weight-6 instance at the same grid and G (k >= 13 at weight 6, which would dominate this code) ran for its full 6 h wall cap under CaDiCaL 1.9.5 without a solve returning; it is the live wall in the weight-6 cell at n=49, next to the [[49,11,4]] yield at G=19. At weight 8 the rung below, G=17 (k >= 15), was not run.
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, 11 min to the first model, RSS about 3 GB.
from pysat.solvers import Cadical195
from local_sat import build_local_cnf
cnf = build_local_cnf(7, 18, 8, 3, 2.0, shared_t3=True)
s = Cadical195(bootstrap_with=cnf["clauses"]); s.conf_budget(20_000_000)
assert s.solve_limited() # about 11 min, 233,788 conflicts
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"], layers = 1; then make_submission.
CaDiCaL is deterministic for a fixed clause order; the first model is the code in this file (fingerprint 3643ab6e724d27d7).