n
36
Cell: weight-8 x local-2d-single. The d=4 points at n=36 were codes/36-6-4.json (G=15) and codes/36-8-4.json (G=14), both weight 6; the weight-8 cell held nothing above them at this n. The fieldnotes list weight-8 t=3 at n=36 as UNSAT at anchor radius 2.0, but the record does not say at which G. With k = n - 2G for full-rank models, G=12 forces k >= 12, and weight 8 relaxes the column-count bound to G >= 2n/9 = 8, so the instance is not trivially empty.
research/local_sat.py build_local_cnf(6, 12, 8, 3, 2.0, shared_t3=True): 6x6 grid, 12 checks per side anchored within radius 2.0 (interaction radius at most 4.0), row weight at most 8, CSS commutation, and nonzero syndrome for every Pauli error of weight at most 3 (the shared-aux t=3 encoding: 586k variables, 2.3M clauses, 5 s to build). CaDiCaL 1.5.3, conflict cap 20,000,000 per solve. First solve SAT after 1,323 s and 868,695 conflicts; the model passed the post-check (no weight <= 3 stabilizer) with k = 12. Continued enumeration with blocking clauses returned further k=12 models at roughly one per 2 to 5 minutes; all had d_ub = 4.
Detection of every weight <= 3 error with no weight <= 3 stabilizer means d >= 4. 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 3,940 RIS trials, no board duplicate, label "advances the weight-8 x local-2d-single board". Check weights: X-rows 8, 8, 8, 8, 7, 7, 6, 6, 6, 6, 6, 6; Z-rows seven of weight 8, two of weight 7, three of weight 6. It is the first d=4 point at n=36 with k > 8 in any 2D-local cell; it does not enter the weight-6 cell.
An exhaustive check after staging, plain GF(2) arithmetic outside the repo, enumerated every X-type and every Z-type error of weight at most 3 (7,806 supports per side) and found none with zero syndrome, so d >= 4 holds independently of the SAT encoding and its post-check; with the weight-4 witnesses, d = 4 exactly. The JSON keeps confidence upper_bound.
G=13 at the same grid and weight is also SAT (40 models, all [[36,10,4]], first in 322 s) and is dominated by this code. The weight-6 t=3 instances at G=12 and G=13 did not return a model or an UNSAT proof within the same conflict cap. The 8x8 G=27 weight-8 t=3 instance returned six SAT solves inside its 3 h wall cap and every model was rejected by the post-check (a weight <= 3 stabilizer), a reminder that the shared-aux encoding over- approximates detection and the post-check is load-bearing.
research/local_sat.py, research/kit/submit.py, research/kit/surrogate.py, verify/validate_candidate.py. CaDiCaL 1.5.3 via python-sat 1.9.dev15, one core, about 22 min to the first model, peak RSS 1 GB.
from local_sat import enumerate_local_sat_codes
gen = enumerate_local_sat_codes(6, 12, 8, 3, 2.0, max_codes=1,
solver="cadical", conf_budget=20_000_000, stream=True, shared_t3=True)
spec, HX, HZ, coords, ax, az = next(gen)
The first model is the code in this file (fingerprint c9e04b554775f49e); the same conflict count (868,695) was reproduced in two independent runs.