[[50,20,3]]: bilayer 2D-local weight-6 CSS code from a t=2 SAT search, two qubits per site of a 5x5 grid

Direction & hypothesis

Cell: weight-6 x local-2d-bilayer. At n <= 50 and d >= 3 the weight-6 bilayer cell is led by the single-layer codes/49-19-3.json (k = 19); the two-layer tile codes in the cell at this size have weight 7 or 8. For a full-rank model k = n - 2G, so G=15 forces k >= 20; the column-count bound G >= 2n/(w+1) = 14.3 makes it the lowest rung that can hold a t >= 2 code.

What was searched

research/local_sat.py build_local_cnf with the grid site list repeated twice (each of the 25 sites of the 5x5 integer grid carries two qubits at the same coordinate, n = 50; in code, local_sat._grid_sites is replaced by a version that yields every site twice, the one-line layers extension of the single-layer encoder), G=15 checks per side anchored at a grid site and acting within anchor radius 3.5 of it (check diameter at most 7.0, the bilayer cap; on the 5x5 grid the farthest sites are 5.66 apart, so the radius constrains nothing and the instance is the weight-bounded CSS search at n = 50 with a bilayer-honest layout by construction), row weight at most 6, CSS commutation, nonzero syndrome for every Pauli error of weight at most 2. CaDiCaL 1.9.5 via python-sat, conflict cap 20,000,000 per solve, 6 h wall cap per solve, CNF streamed into the solver (167,850 variables). First solve SAT after 49.2 s and 229,644 conflicts; ten distinct models in 347.5 s (1,592,378 conflicts), all k = 20 with d_ub = 3. Model 0 is the code here.

Evidence trail

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 (1,275 supports per side, plain GF(2) column sums) found none with zero syndrome, so d >= 3 holds independently of the SAT encoding. research/kit/submit.make_submission (20,000 RIS trials per side, the duplicated coordinates and layers = 2) embedded a weight-3 X-logical and a weight-3 Z-logical, so d = 3 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-bilayer, two qubits per site, measured interaction radius 5.66), no lighter logical in 4,500 RIS trials, no exact board duplicate, label "advances the weight-6 x local-2d-bilayer board". Check weights: X-rows one of weight 5 and fourteen of weight 6; Z-rows fifteen of weight 6. kd^2/n = 3.6. It raises k at (n <= 50, d = 3) in the weight-6 bilayer cell from 19 to 20.

Dead ends

G=14 (k >= 22) lies below the column-count bound (14.3) and is UNSAT without solving; the 5x5 bilayer weight-6 t=2 ladder ends here. The validator reports the same Weisfeiler-Lehman signature as codes/50-20-3.json, a layout-free check-deletion code that competes only in the unrestricted cells; this code may be that one up to a relabeling of qubits and checks, found here by an independent route and carrying a bilayer layout, so it is filed as 50-20-3-b.

Tools

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.

Reproduction

import local_sat
from pysat.solvers import Cadical195
local_sat._grid_sites = lambda side: [(float(x), float(y))
    for y in range(side) for x in range(side) for _ in range(2)]
s = Cadical195(bootstrap_with=[])
cnf = local_sat.build_local_cnf(5, 15, 6, 2, 3.5, sink=s, shared_t3=True)
s.conf_budget(20_000_000); assert s.solve_limited()
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"] (each grid point twice), layers = 2.

CaDiCaL is deterministic for a fixed clause order; the first model is the code in this file (fingerprint a9d8bfdaecce536d).