n
36
Cell: weight-6 x local-2d-single. The d=4 points at n=36 in this cell were codes/36-6-4.json (G=15 checks per side) and codes/36-8-4.json (G=14), and the weight-8 codes/36-12-4.json sits in the weight-8 cell only. The board's codes/36-10-4.json is a different code with the same parameters, weight 8 and no layout, so it competes only in the unrestricted cells; this file takes the -b suffix. For a full-rank model k = n - 2G, so k >= 10 at weight 6 needs G <= 13. The G=13 instance had been a budget wall at every budget tried: interactive budgets in the earlier campaigns, and 3 h of CaDiCaL 1.5.3 (about 7.5M conflicts) in the Phase 0 triage of issue #2024, with no model and no UNSAT proof.
research/local_sat.py build_local_cnf(6, 13, 6, 3, 2.0, shared_t3=True): 6x6 grid, 13 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 (635,036 variables, 2,482,917 clauses, 6 s to build, 1 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 7,924.9 s and 8,594,790 conflicts; the model passed the post-check (no weight <= 3 stabilizer) with k = 10 and d_ub = 4. Further k = 10 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 (7,806 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 3,940 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-single board". Check weights: X-rows one of weight 4, twelve of weight 6; Z-rows two of weight 4, eleven of weight 6. kd^2/n = 4.44. On (n, k, d, w) it dominates codes/36-8-4.json and codes/36-6-4.json; it does not touch codes/36-12-4.json, which is weight 8.
The same instance under CaDiCaL 1.5.3 did not return in 3 h in the Phase 0 triage (about 7.5M conflicts at the measured 690 conflicts per second), and three permuted-CNF replicas under 1.5.3 did not return in 1 h each. The 1.9.5 solve needed 8.6M conflicts, so the 1.5.3 wall was a near miss in budget rather than a different search outcome, if the two versions follow similar paths; the conflict counts do not say whether they do. G=12 at the same grid and weight (k >= 12) is running 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, 2 h 12 min to the first model, RSS 1 GB.
from pysat.solvers import Cadical195
from local_sat import build_local_cnf
cnf = build_local_cnf(6, 13, 6, 3, 2.0, shared_t3=True)
s = Cadical195(bootstrap_with=cnf["clauses"]); s.conf_budget(20_000_000)
assert s.solve_limited() # about 2.2 h, 8,594,790 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 977a7846954fd0c0).