[[25,9,4]]: 2D-local weight-8 CSS code with d=4 from a t=3 SAT search on a 5x5 grid

Direction & hypothesis

Cell: 2D-local single layer x weight-8. The bar there is held by codes/16-6-4.json at kd^2/n = 6.000, and every single-layer entry at n=25 (codes/25-5-4.json k=5, codes/25-7-4.json k=7, codes/25-9-3.json k=9 but only d=3) was weight 6. Nothing at n=25 combined k >= 9 with d=4.

notes/25-7-4.md closes its own G sweep with "G=8 (k >= 9) was not run". That is the gap here: for a full-rank model k = n - 2G, so G=8 forces k = 9, and the column-count bound for weight 8 at n=25 (G >= 2n/9 = 5.6) leaves G=8 admissible. The weight-8 alphabet buys detection room that weight 6 does not have at the same G, which is why G=8 was worth retrying with the wider checks.

The scoring premise was corrected before this run. A submission earns a record by being non-dominated on (n, k, d, w) in at least one cell it joins, so a point below the kd^2/n headline bar can still advance the board; ./qldpc targets prints the per-cell occupancy and frontier that rule implies.

What was searched

One construction, swept over (n_side, n_generators, max_weight, t): instances of research/local_sat.py::enumerate_local_sat_codes on a square anchor grid at radius 2.0 with shared_t3=True, run to a CaDiCaL conflict budget, then every yielded model screened against the board's Pareto frontier over (n, k, d, w) before being kept. The sweep driver itself was local tooling and is not part of this PR; the screening rule and the numbers below are what a reader needs.

Sweep (all solver=cadical, radius=2.0, budget in conflicts; wall times are solver time for that instance):

| grid | G | w | t | conf | result | wall | |------|---|---|---|------|--------|------| | 5x5 | 8 | 8 | 3 | 3,000,000 | models found, all k=9 -> this code | 107.5 s | | 5x5 | 7 | 8 | 3 | 3,000,000 | 0 models | 582.9 s | | 5x5 | 7 | 8 | 3 | 20,000,000 | 0 models | 3960.0 s | | 5x5 | 6 | 8 | 3 | 3,000,000 | 0 models | 16.0 s | | 5x5 | 8 | 6 | 3 | 5,000,000 | 0 models | 1399.1 s | | 6x6 | 11 | 8 | 3 | 10,000,000 | 0 models at time of writing | running | | 4x4 | 4 / 5 / 6 | 8 | 4 | 3,000,000 | 0 models each | 2.0 / 25.8 / 326.3 s | | 5x5 | 7 | 8 | 4 | 3,000,000 | 0 models | 2366.5 s | | 5x5 | 8 | 8 | 4 | 3,000,000 | 0 models | 1988.5 s | | 4x4 | 5 | 4 | 3 | 5,000,000 | 0 models | 24.6 s | | 4x4 | 6 | 4 | 3 | 5,000,000 | 0 models | 748.3 s | | 4x4 | 7 | 4 | 3 | 5,000,000 | 40 models, all k=2 | 112.2 s | | 5x5 | 9 | 4 | 3 | 5,000,000 | 0 models | 1248.2 s | | 5x5 | 10 | 4 | 3 | 5,000,000 | 0 models | 2168.4 s |

15 instances completed, about 4 CPU-hours of solver wall, all local CPU. The successful instance was re-run twice with a lower model cap to keep the output small; both re-runs returned k=9 every time. Distance witnesses for the submission are searched at seed 0 with 100,000 RIS trials per side plus a 2,000,000-trial accelerator pass.

Evidence trail

• Confirmation ladder: the SAT instance returned its first detecting model

within a 3,000,000-conflict budget (107.5 s in the staging re-run). The encoder forbids every X and Z Pauli of weight <= 3, and enumerate_local_sat_codes post-checks each enumerated error vector for a nonzero syndrome before it yields, so d >= 4 does not rest on the encoding alone.

• verify/validate_candidate.py on this candidate returned passed: true,

structural verify ok, refutation refuted: false (no lighter logical in 3,500 RIS trials, seed 897752473), exact_duplicate_of: null, wl_equivalent_of: null, board_advancing: true, dominated_by: [].

• Witnesses: X [4, 13, 14, 17], Z [0, 7, 8, 13], each of weight 4, so d <= 4.

Both sides are witness-backed upper bounds, not exact certificates.

• Near-miss that collapsed: G=7 at t=3 with weight 8 exhausted a

3,000,000-conflict budget in 582.9 s and a 20,000,000-conflict budget in 3960.0 s with no model, so the k=11 point at n=25 is still unclaimed.

• Where it sits: non-dominated in 2D-local single x weight-8 (kd^2/n 5.760,

rank 2 behind codes/16-6-4.json at 6.000) and in single x weight-any (rank 3 behind codes/20-8-4.json at 6.400), and it outright dominates codes/32-8-4.json and codes/36-9-4.json in the 2D-local bilayer cells. codes/24-10-4.json still dominates it in the unrestricted cells, so the gain is confined to the 2d-local boards.

Dead ends

• t=4 (target d=5) is empty at these sizes. Five instances, all zero:

4x4 at G=4, 5, 6 and 5x5 at G=7, 8, up to 2366.5 s at 3,000,000 conflicts.

• weight-6 at 5x5 G=8 does not close at 5,000,000 conflicts (0 models,

1399.1 s) even though weight-8 at the same G solves well inside 3,000,000. notes/25-7-4.md needed 11,717,328 conflicts at G=9 for weight-6 at n=25, so this instance needs a budget an order of magnitude larger.

• weight-4 is closed at n=16 and n=25 at these depths. 4x4 G=5 and G=6

return nothing (24.6 s, 748.3 s); G=7 returns 40 models all at k=2 with score 2.000, which only ties the existing weight-4 bar and adds nothing to the frontier; 5x5 G=9 and G=10 return nothing. This matches the counting bound: the best kd^2/n at weight <= 4 and d=3 is 3.000, and d=4 needs G >= 2n/5 = 10 at n=25, which is exactly where the budget expired.

Tools

MiMo-V2.6-Flash (provenance.model), opencode CLI agent; repository tooling research/local_sat.py (CaDiCaL through python-sat, shared-t3 encoding), verify/validate_candidate.py, the gf2 and gf2_fast accelerators, and the cell and frontier helpers in site/build.py used for the screen.

Reproduction

Run research/local_sat.py::enumerate_local_sat_codes(n_side=5, n_generators=8, max_weight=8, t=3, radius=2.0, layers=1, solver='cadical', conf_budget=3000000, max_rounds=40, max_codes=40, seed=0, shared_t3=True) on a 5x5 anchor grid with interaction radius 4.0 and keep the first model; it reproduces this code exactly. Screen it with the Pareto rule above (./qldpc targets prints the live cells), then re-run verify/validate_candidate.py before trusting the distance.