n
64
Cell: weight-6 x local-2d-single. codes/64-22-3.json came from the same encoding at G=21 checks per side in the Phase 0 triage of issue #2024, where G=23, 22, and 21 were run and G=20 and 19 were left for Phase 1. For a full-rank model k = n - 2G, so G=20 forces k >= 24 and G=19 forces k >= 26. The column-count bound for weight 6 at n=64 (G >= 2n/7 = 18.3) makes G=19 the last rung that can hold a code at all.
research/local_sat.py build_local_cnf(8, 20, 6, 2, 2.0, shared_t3=True): 8x8 grid, 20 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 (266,720 variables, 998,576 clauses, 2 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 194.9 s and 701,946 conflicts; ten distinct models in 483 s (1.71M conflicts), all k = 24 with d_ub = 3. Model 0 is the code here. The G=19 rung (k >= 26) then ran to its 20,000,000-conflict cap in 5,521 s with neither a model nor an UNSAT proof.
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 (2,080 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,060 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-single board". Check weights: X-rows two of weight 5, eighteen of weight 6; Z-rows two of weight 4, five of weight 5, thirteen of weight 6. kd^2/n = 3.38. On (n, k, d, w) it dominates codes/64-22-3.json.
G=19 (k >= 26) at the same grid and weight: 20,000,000 conflicts in 5,521 s, no answer; it is the column-count minimum and the analog of the 7x7 G=14 wall, which likewise sits one rung below the last yield. The 7x7 pattern (yield at the bound plus one, wall at the bound) now holds at 4x4, 5x5, 6x6, 7x7, and 8x8.
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, 3.2 min to the first model, RSS under 0.5 GB.
from pysat.solvers import Cadical195
from local_sat import build_local_cnf
cnf = build_local_cnf(8, 20, 6, 2, 2.0, shared_t3=True)
s = Cadical195(bootstrap_with=cnf["clauses"]); s.conf_budget(20_000_000)
assert s.solve_limited() # about 3 min, 701,946 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 abd6357fd1cd631e).