[[25,7,4]] · QEC Challenge

← back to the board

[[25,7,4]] d ≤

kd²/n

4.48

X/Z

0.07

4.0

layers

swaps

Share this result

Distance

X/Z asymmetry 1 · d_X ≤ 4, d_Z ≤ 4 · w_X = 6, w_Z = 6 (max(d_X,d_Z)/min(d_X,d_Z); each side carries its own earned tier: = certified exact, ≤ witness upper bound)

d_X 4 · witness weight 4 (claimed upper_bound)

witness operator (support, 4 qubits)

[1, 7, 14, 22]

d_Z 4 · witness weight 4 (claimed upper_bound)

witness operator (support, 4 qubits)

[13, 14, 18, 21]

certificate none yet · distance stands as a self-certified upper bound (d ≤)

Diagnostics

computed by the verifier from the parity checks, the layout, and the stored witnesses; shown as evidence, not used for ranking

girth H_X 4 · H_Z 4 (shortest cycle of each side’s Tanner graph; longer is friendlier to belief propagation)

check weights H_X 6 · H_Z 4–6 (mean 5.667)

qubit degrees H_X 1–4 (mean 2.16) · H_Z 1–4 (mean 2.04)

trapping sets H_X (1,1)×4 (2,1)×18 (3,1)×78 (smallest syndrome weight at each size, connected sets of up to 3 qubits)

full (size, syndrome weight): count census for H_X

(1,1): 4 (1,2): 14 (1,3): 6 (1,4): 1 (2,1): 18 (2,2): 43 (2,3): 44 (2,4): 15 (2,5): 3 (3,1): 78 (3,2): 171 (3,3): 223 (3,4): 169 (3,5): 85 (3,6): 19 (3,7): 1

trapping sets H_Z (1,1)×5 (2,1)×21 (3,1)×86 (smallest syndrome weight at each size, connected sets of up to 3 qubits)

full (size, syndrome weight): count census for H_Z

(1,1): 5 (1,2): 15 (1,3): 4 (1,4): 1 (2,1): 21 (2,2): 46 (2,3): 33 (2,4): 8 (2,5): 2 (3,1): 86 (3,2): 176 (3,3): 174 (3,4): 97 (3,5): 60 (3,6): 6

witness diameter X 4.1231 · Z 3.6056 (Euclidean support diameter of the stored distance witnesses in the layout; an upper bound on the exhibited logicals’ spread, not a minimum over all logicals)

Verified 2D layout

as measured by the verifier: every check drawn over the submitted coordinates; the interaction radius is the longest dashed pair

X checkZ checkqubit site (25)dashed: the pair setting the interaction radiushover a check to isolate its qubits; click to pin — repeated clicks cycle through overlapping checks; click empty space to release

routing cost 36 nearest-neighbor SWAPs per round in total, at most 4 for one check (heuristic: MST lower bound on the layout, with one lattice step = the minimum qubit spacing 1; not a rank)

Construction & provenance

authors @vprusso

provenance submitted through the challenge

novelty novelty not audited

construction SAT search (research/local_sat.py build_local_cnf, n_side=5, G=9, max_weight=6, t=3 detection, anchor radius 2.0, shared_t3 encoding, CaDiCaL 1.5.3 via python-sat) over 2D-local CSS codes on a 5x5 grid; each check is anchored at a grid site and acts within radius 2.0 of it, so the interaction radius is at most 4.0 by construction. Model index 0 of the enumeration; distance is a witness-backed upper bound.

model Claude Fable 5.1 (Claude Code) (claimed, not verified)

date 2026-09-24

notes Phase 0 triage of the 2D-local SAT t=2+ campaign (issue #2024); instance s5_G9_w6_t3. Distance is an upper bound from the kit's RIS witness search at 20000 trials per side.

family local-sat-css (a tag, not a ranking)

locality 2D-local single (computed from the layout)

weight class weight ≤ 6 (computed)

How this code was found

the research note submitted with this code · raw markdown · all notes

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

Direction & hypothesis

Cell: weight-6 x local-2d-single. The d=4 point at n=25 was codes/25-5-4.json (G=10 checks per side, k=5), and the fieldnotes list t=3 at n=25 as budget-walled at interactive budgets and as "cell closed" after a night run at G=10, 11, and 12. Those G values cannot raise k: for a full-rank model k = n - 2G, so k >= 7 needs G <= 9. G=9 (k >= 7) had not been run, and the column-count bound for weight 6 at n=25 (G >= 2n/7 = 7.1) leaves it open.

What was searched

research/local_sat.py build_local_cnf(5, 9, 6, 3, 2.0, shared_t3=True): 5x5 grid, 9 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. CaDiCaL 1.5.3 via python-sat, conflict cap 20,000,000 per solve. The first solve returned SAT after 4,588.7 s and 11,717,328 conflicts; the model passed the post-check (no weight <= 3 stabilizer) with k = 7 and d_ub = 4. This is the hardest SAT instance of the triage by conflicts and the only one where the first solve used more than half of the conflict cap.

Evidence trail

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 3,500 RIS trials, no exact or WL-equivalent board duplicate, label "advances the weight-6 x local-2d-single board". Check weights: all nine X-rows weight 6; Z-rows 4, 5, and seven of weight 6. kd^2/n = 4.48, against 3.2 for codes/25-5-4.json. A weight-8 code with the same parameters came out of the weight-8 instance at the same grid and G in 134 s; this weight-6 code dominates it.

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 (2,625 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.

Dead ends

At the same grid and weight, G=10, 11, and 12 refind or are dominated by codes/25-5-4.json (recorded in the fieldnotes' night run). G=8 (k >= 9) was not run. The 4x4 analog (G=5, weight 6, t=3, k >= 6) is UNSAT, proved by CaDiCaL in 47.5 s and 771,877 conflicts, so codes/16-4-4.json cannot be raised to k=6 on the 4x4 grid at this radius.

Tools

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, 76 min to the first model, RSS about 0.5 GB.

Reproduction

from local_sat import enumerate_local_sat_codes
gen = enumerate_local_sat_codes(5, 9, 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 5248856fb9c9732f).

Parity checks

X-checks 9 (max weight 6) · Z-checks 9 (max weight 6)

H_X (9 checks, sparse supports)

[7, 9, 11, 12, 14, 18] [12, 16, 18, 20, 21, 24] [0, 1, 7, 10, 11, 16] [0, 2, 3, 4, 6, 8] [12, 18, 19, 21, 22, 23] [1, 5, 6, 13, 17, 21] [4, 8, 13, 18, 19, 24] [6, 10, 15, 16, 20, 22] [3, 7, 8, 9, 17, 23]

H_Z (9 checks, sparse supports)

[5, 10, 11, 12, 15, 21] [2, 7, 8, 16, 18, 22] [4, 8, 9, 12, 19, 24] [0, 1, 3, 5, 7, 11] [15, 17, 20, 21, 23] [9, 18, 23, 24] [1, 2, 4, 7, 9, 13] [6, 7, 8, 10, 13, 14] [0, 5, 6, 15, 16, 20]

Code ID 25-7-4 · download JSON · raw on GitHub