Qec Construct

qec-construct — a QEC verifier-in-the-loop

Routing (brain: read this section, forward the rest)

Applies when RESEARCH.md's goal is a new or improved QEC code / code family / transversal-gate construction — construct, invent, design, discover, improve distance/FOM, and search-phrased variants ("find codes beating X") equally.

Does NOT apply to magic-state cultivation, lattice surgery, decoder, or imaging projects: the gate check is abelian/CCZ-only and those are out of scope regardless of wiring.

Brain's only two obligations (do not run the loop yourself):

1. Read this file BEFORE writing notes/plan.md.
2. Every code-construction/code-search experiment spawn task MUST (a) include the literal path skills/qec-construct/SKILL.md with the instruction to read it in the Design phase and wrap scripts/qverify as a tool, and (b) frame the experiment as a construct-loop (propose a parametrized ALGEBRAIC construction → qverify → debug the failure), never as random/grid sampling over supports — sampling is the mode that capped at FOM ~10.4 vs frontier 45.5.

The one rule: CONSTRUCT, don't search

Broad/random/hill-climb search over code supports is a known dead end for this problem (empirically caps far below the frontier; the good codes are rare isolated optima). Your job is to propose a parametrized ALGEBRAIC construction — a group + a generating rule for the supports + (for a new gate) the cup-product / Leibniz conditions — and debug it against the sound verifier, not to sample points and hope.

If you find yourself enumerating random supports, stop: that is the wrong mode.

The verifier: scripts/qverify (this is your Lean)

Call it at high frequency. Input a construction spec (JSON), get a SOUND verdict — including which condition failed, so you can fix it.

Copy code
echo '{"family":"abelian","group_shape":[3,4,5],
       "supp_a":[[0,1,3],[0,3,0],[2,1,3],[2,3,1]],
       "supp_b":[[1,1,4],[1,2,2],[2,1,1],[2,2,4]],
       "supp_c":[[0,0,4],[2,0,1]],
       "frontier_fom":14.4}' | scripts/qverify

What it checks, cheapest first:

• CSS validity (H_X H_Z^T = 0), n, k — exact GF(2), instant. Fails loudly if your construction isn't even a code.
• Cheap sound screen — a fast heuristic upper bound UB on d_Z (~sub-second, ~100x faster than exact). Reports FOM_upper = k*UB^3/n. If FOM_upper < frontier the code provably can't beat it → reject (never rejects a real winner, since UB ≥ d_Z). Otherwise → promote.
• Gate (CCZ) check (supply partition_a/b/c) — STCP/Leibniz conditions hold? logical CCZ non-trivial? K_CCZ (extractable gates). Abelian path is validated against all 11 published Menon codes.
• "exact":true — sound exact distance via ILP-to-optimality. Only this certifies distance. Run it only on promoted candidates.

The loop (this is the whole method)

1. Propose a construction (group + support-generating rule + preorientation).
2. qverify it (cheap). If css or gate fails → read which condition failed → fix the construction (this is the Menon-style derivation-debug; e.g. the naive cup-product conditions force d=2 — find the offset/structure that escapes it).
3. Keep the cheap screen as your fitness: iterate the construction rule to push FOM_upper up while keeping the gate valid.
4. On a promoted candidate, run "exact":true to certify.

The soundness gate — DO NOT violate

A code counts as a new frontier code ONLY if a single qverify run shows: css_valid ✓, gate.preserves_codespace/stcp_conditions_hold ✓, K_CCZ ≥ 1, and distance_exact.status == "optimal" with fom_exact strictly above the frontier. Estimated / biased-sampled / timed-out distances never certify a win. If you report a win on anything less, it is a hallucination, not a result.

Where the new codes likely are

The abelian families are heavily optimized (you will mostly re-find Menon). The upside is the under-explored non-abelian region ("family":"general", "group":{"kind":"dihedral","n":..} or {"kind":"perm","generators":[..]}). The CSS + distance + cheap-screen verifiers ARE general and sound for non-abelian. But two honest caveats: (1) the non-abelian CCZ gate check is NOT yet implemented in qverify — so a non-abelian code is CSS/distance-verified but cannot be gate-CERTIFIED here yet; implementing a group-agnostic direct-circuit coboundary-invariance check (validated against verify_stcp before ship) is the open next step. (2) Non-abelian is a high-risk region, not virgin territory: Tiew2026 already derived non-abelian weight-4 cup-product gate conditions, yet experts (Tiew, Menon) converged on abelian for deep reasons — the cup product is graded-commutative (abelian-aligned), and abelian gives Fourier/character analysis, analytic distance bounds, and hardware locality. Betting on non-abelian bets that their choice was driven by "harder to analyze" (which this skill's verifiers bypass) rather than "structurally worse" (which they don't).

Honest boundary

This skill gives you a sound, cheap, debuggable verifier and the construct-don't- search discipline. It does not guarantee a better code — proposing the right construction is still the hard part. But it is the machine that lets a construction loop actually converge instead of hallucinating, and it attacks the two real walls: no cheap classical proxy exists for quantum distance (so the screen measures the quantum quantity directly, cheaply, soundly), and the gate-validity that used to be guessed is now checked exactly.