n
64
Cell: weight-6 x local-2d-single. The d=4 points in this cell stop at n=36 (codes/36-8-4.json, k=8); the fieldnotes record 8x8 t=3 at G=16 and G=12 as budget-exhausted after about 9 h at 500k and 5M conflict budgets. Those G values are below the column-count bound for weight 6 at n=64 (G >= 2n/7 = 18.3), so they were UNSAT by construction and the 8x8 t=3 cell had in fact never been probed at a G that can hold a code. With k = n - 2G for a full-rank model, k >= 9 (one above the incumbent) needs G <= 27; G=27 was run as the first rung.
research/local_sat.py build_local_cnf(8, 27, 6, 3, 2.0, shared_t3=True): 8x8 grid, 27 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 (about 7M variables and 27M clauses, 74 s to build, 4.7 GB RSS). CaDiCaL 1.5.3 via python-sat, conflict cap 20,000,000 per solve. First solve SAT after 8,609.1 s and 872,192 conflicts (about 100 conflicts per second on this formula); the model passed the post-check (no weight <= 3 stabilizer) with k = 10 and d_ub = 4. The second model came 1,597 s later. The first model is the one packaged here. The same instance in an earlier launch returned the same first model at the same conflict count.
Detection of every weight <= 3 error with no weight <= 3 stabilizer gives d >= 4. 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 eleven of weight 4, one of weight 5, fifteen of weight 6; Z-rows eight of weight 4, six of weight 5, thirteen of weight 6. kd^2/n = 2.5, below codes/36-8-4.json (3.56) on that metric; the code is a new Pareto point on (n, k, d) because no code with n <= 64 has k >= 10 at d >= 4 in the 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 (43,744 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=26 (k >= 12) at the same grid and weight ran for the full 3 h wall cap without a solve returning (about 1M conflicts), a budget wall. The weight-8 instance at G=27 returned six models in six SAT solves, all rejected by the post-check for a weight <= 3 stabilizer, and hit the 3 h wall cap during the seventh solve with no model kept. G=16 and G=12, the fieldnotes' instances, are UNSAT by the column-count bound and were not closed by CaDiCaL within the 1 h cap they were given.
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, CPython 3.12, one core, 2 h 24 min to the first model, RSS 4.7 GB.
from local_sat import enumerate_local_sat_codes
gen = enumerate_local_sat_codes(8, 27, 6, 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)
CaDiCaL is deterministic for a fixed clause order; the first model is the code in this file (fingerprint 3fd74db24101665c). Expect about 2.5 h on one core and 5 GB of memory.