n
49
Cell: weight-6 x local-2d-single. The d=4 points in this cell were codes/16-4-4.json, codes/18-4-4.json, codes/25-7-4.json, codes/36-8-4.json, and codes/64-10-4.json; nothing sat at n=49, and the 7x7 grid had never been run at t=3. For a full-rank model k = n - 2G, so k >= 9 (one above [[36,8,4]]) needs G <= 20, and k >= 11 (one above [[64,10,4]]) needs G <= 19. The column-count bound for weight 6 at n=49 (G >= 2n/7 = 14) leaves both open. G=20 and G=19 were the first two rungs of the Phase 1 list.
research/local_sat.py build_local_cnf(7, 19, 6, 3, 2.0, shared_t3=True): 7x7 grid, 19 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 (2.30M variables, 8.84M clauses, 21 s to build, 3.0 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 3,577.4 s and 898,354 conflicts; the model passed the post-check (no weight <= 3 stabilizer) with k = 11 and d_ub = 4. Two further k = 11 models followed within a second. The neighboring rung G=20 returned [[49,9,4]] after 2,737.7 s and 635,448 conflicts; it is dominated by this code.
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 (19,649 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 4,460 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-single board". Check weights: X-rows three of weight 4, one of weight 5, fifteen of weight 6; Z-rows four of weight 4, one of weight 5, fourteen of weight 6. kd^2/n = 3.59. On (n, k, d, w) this code dominates codes/64-10-4.json (n 49 < 64, k 11 > 10, same d and weight).
G=20 at the same grid and weight yields only k = 9 (dominated). G=18 (k >= 13) is queued after this instance; at 6x6 the analogous rung below the first yield (G=12 and 13 at weight 6) has not returned in 3 h at 1.5.3 or 1 h per permuted replica. The redundant column-count clauses and the permuted portfolio tested in the Phase 1 preamble changed no outcome and were not used here; CaDiCaL 1.9.5 was adopted from that preamble for a 2 to 5 percent throughput gain.
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, 60 min to the first model, RSS 3.0 GB.
from pysat.solvers import Cadical195
from local_sat import build_local_cnf
cnf = build_local_cnf(7, 19, 6, 3, 2.0, shared_t3=True)
s = Cadical195(bootstrap_with=cnf["clauses"]); s.conf_budget(20_000_000)
assert s.solve_limited() # about 60 min, 898,354 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.
enumerate_local_sat_codes(7, 19, 6, 3, 2.0, solver="cadical", ...) gives the same CNF with CaDiCaL 1.5.3, which returns the same model (the solver is deterministic for a fixed clause order; fingerprint d665285a83527f68).