n
81
Cell: weight-6 x local-2d-single. The t=2 SAT method had produced the d=3 records on the 4x4 to 8x8 grids (codes/16-6-3.json, codes/25-9-3.json, codes/36-12-3.json, codes/49-17-3.json, codes/64-22-3.json, and the [[64,24,3]] submitted separately from this campaign), each at the smallest number of checks per side G that is still satisfiable, one above the column-count bound G >= 2n/(w+1). At n=81 and weight 6 that bound is G >= 23.1, so G=25, 24, and 23 were queued; for a full-rank model k = n - 2G, so they force k >= 31, 33, and 35.
research/local_sat.py build_local_cnf(9, 25, 6, 2, 2.0, shared_t3=True): 9x9 grid, 25 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 weight <= 2 Pauli error (512,192 variables, 1,929,945 clauses, 4 s to 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 1,224.6 s and 2,865,685 conflicts; ten distinct models in 5,086 s (14.9M conflicts), all k = 31 with d_ub = 3. Model 0 is the code here.
research/kit/submit.make_submission (20,000 RIS trials per side) embedded a weight-3 X-logical and a weight-3 Z-logical; every weight <= 2 error is detected by the CNF, and an exhaustive enumeration after staging of every X-type and every Z-type error of weight at most 2 (3,321 supports per side, plain GF(2) column sums) found none with zero syndrome, so d = 3 exactly (labeled upper_bound by the kit). verify/validate_candidate.py: verifier ok (weight class weight-6, locality class local-2d-single, interaction radius 4.0), no lighter logical in 5,740 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, three of weight 5, twenty-one of weight 6; Z-rows one of weight 4, one of weight 5, twenty-three of weight 6. kd^2/n = 3.44. It is the first single-layer 2D-local d=3 point at n=81 in the weight-6 cell; the board's codes/81-1-9.json is a d=9 point at a different corner of the frontier.
G=23 (k >= 35) at the same grid and weight ran to its 20,000,000-conflict cap in 4,890 s with neither a model nor an UNSAT proof. G=24 (k >= 33) likewise ran to the cap in 6,435 s with no answer. The pattern from the smaller grids (yield one rung above the column-count bound, wall at the bound) therefore holds at 9x9 as well.
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, 20 min to the first model, RSS about 0.6 GB.
from pysat.solvers import Cadical195
from local_sat import build_local_cnf
cnf = build_local_cnf(9, 25, 6, 2, 2.0, shared_t3=True)
s = Cadical195(bootstrap_with=cnf["clauses"]); s.conf_budget(20_000_000)
assert s.solve_limited() # about 20 min, 2,865,685 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 6f6a7fa2419fab90).