n
18
Weight-6 x unrestricted cell. The board is 85% even-weight: 56 entries at w = 4, 114 at w = 6, 71 at w = 8, against 4 at w = 5 and 6 at w = 7. That is an artifact of which constructions have been run rather than a fact about codes. Two-block families give w = wt(a) + wt(b) and every sweep so far used symmetric supports; hypergraph and lifted products sum two degrees. Both land on even weights, and nothing had systematically searched an odd cap.
SAT is the tool that can, because an exact weight bound is a native constraint rather than something a construction happens to satisfy. The hypothesis was simply that the odd caps are unsearched rather than empty.
A caveat worth stating up front, because it nearly sank this submission: the board's weight classes are weight-4, weight-6, weight-8 and weight-9plus, so a weight-5 code competes in the weight-6 class against all 114 of its members. There is no weight-5 cell to fill. The code has to earn its place on (n, k, d) against weight-6 entries, with its lower raw weight as a ranking axis inside the cell. This one does: nothing on the board with n <= 18 reaches k >= 4 at d >= 3 with w <= 5.
research/sat_search.py (committed with PR #709): CNF over X/Z row-incidence variables, even-overlap commutation chains encoding HX HZ^T = 0, per-error detection clauses for every Pauli of weight <= 2, and a Sinz sequential-counter bound on each row weight; distinct solutions enumerated by blocking clauses.
Sweep over n in [18, 38] with w <= 5 and t = 2 (so d >= 3), taking the number of check rows per side as the second dial. The instance that produced this code is n = 18 with 7 rows per side, solved in seconds.
Submitted claim: d <= 3, a witness-backed upper bound, not exact.
d >= 3 by construction, since every weight-2 error isdetected.
qldpc submit at 20k RIS trials: d_X <= 3, d_Z <= 3.d = 3 exactly, though the entryrecords the honest upper-bound tier rather than claiming exactness through an argument the verifier cannot check.
k = 4 was recomputed from the check matrices rather than taken from the solver. Row weights are 4 and 5 on the X side and 5 throughout the Z side, so the computed class is weight-6 and the raw weight is 5.
row count, so that each n starts at the fewest checks, puts the hardest instance first: reaching k >= 3 needs FEWER checks than the sweeps that are known to work, and fewer checks makes detection harder to satisfy. That version burned a 240 s cap on the first instance and would have burned every cap in turn. Descending from the satisfiable boundary outward found this code in seconds. Same solver, same encoding, same budget.
k >= 3 looks genuinely hard, not merely unsearched. Atn = 12 every rank split summing to 9 returns UNSAT, so no weight-4 CSS code on 12 qubits with k >= 3 detects every weight-2 error, at any pair of check counts. n = 14 and n = 16 fall for every unbalanced split but their balanced splits did not resolve; one ran two and a half hours. That is the SAT phase transition sitting where the two check counts are nearly equal.
generator applies one row count to both sides and its solutions come out with rank(HX) = rank(HZ), so a sweep over that parameter walks the diagonal of the (rX, rZ) plane. Closing an n needs the splits, which needs an asymmetric variant of the generator.
Claude Fable 5, matching provenance.model. research/sat_search.py with python-sat / Minisat22; verify/qldpc_verify.py and verify/validate_candidate.py for the gate. Laptop-scale: seconds per satisfiable instance, and the unsatisfiable ones are where the time goes.
uv run --with python-sat python - <<'PY' import sys sys.path.insert(0, "research") from sat_search import enumerate_sat_codes spec, HX, HZ = next(iter(enumerate_sat_codes(18, 7, 5, 2, max_codes=1))) PY
n = 18, 7 rows per side, max row weight 5, detect every weight-<= 2 error.