n
64
Cell: weight-6 x local-2d-single. codes/64-10-4.json came from the same encoding at G=27 checks per side (first model after 2.4 h); for a full-rank model k = n - 2G, so k >= 12 needs G <= 26. The G=26 instance did not return in 3 h of CaDiCaL 1.5.3 in the Phase 0 triage of issue #2024 (about 1M conflicts at the measured 100 conflicts per second), so it was the first 8x8 rung of the Phase 1 list.
research/local_sat.py build_local_cnf(8, 26, 6, 3, 2.0, shared_t3=True): 8x8 grid, 26 checks per side anchored within radius 2.0 (interaction radius at most 4.0 by construction), row weight at most 6, CSS commutation, nonzero syndrome for every Pauli error of weight at most 3 (6,948,368 variables, 26,401,196 clauses, 59 s to build, 10.3 GB RSS with the in-memory build). CaDiCaL 1.9.5 via python-sat, conflict cap 20,000,000 per solve, 6 h wall cap per solve. First solve SAT after 6,084.9 s and 658,521 conflicts; the model passed the post-check (no weight <= 3 stabilizer) with k = 12 and d_ub = 4. Further k = 12 models followed within seconds under blocking clauses. 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 (43,744 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-6, locality class local-2d-single, interaction radius 4.0), no lighter logical in 5,060 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-single board". Check weights: X-rows six of weight 4, three of weight 5, seventeen of weight 6; Z-rows five of weight 4, five of weight 5, sixteen of weight 6. kd^2/n = 3.0. On (n, k, d, w) it dominates codes/64-10-4.json; against the [[49,11,4]] code submitted separately from the same campaign it trades n for k and both stay on the frontier.
The same instance under CaDiCaL 1.5.3 did not return in 3 h in Phase 0. The 1.9.5 solve returned after 658,521 conflicts, fewer than the roughly 1M the 1.5.3 run had spent, so the two versions took different search paths on this formula; the preamble's 2 to 5 percent throughput difference does not explain the gap. G=25 and G=24 at the same grid and weight (k >= 14 and k >= 16) are queued with the same budget.
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 41 min to the first model, RSS 10.3 GB (about 5 GB with the streamed build of enumerate_local_sat_codes).
from pysat.solvers import Cadical195
from local_sat import build_local_cnf
cnf = build_local_cnf(8, 26, 6, 3, 2.0, shared_t3=True)
s = Cadical195(bootstrap_with=cnf["clauses"]); s.conf_budget(20_000_000)
assert s.solve_limited() # about 1.7 h, 658,521 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 c35bce07214bdc2b).