CC: erasure bound (opt-in token) #195

Hub: #15. Stacked on #162 (rule tiebreak, PR #180, not merged); base main 6083e66 + PR #180 head 3475ff5.

Hypothesis

At nodes high in the CC tree the packing bound is often nearly tight: the p disjoint odd rows found by pack leave only extra = (w - |S|) - p <= 2 added qubits that are not charged to a packed row. A linear-algebra test on that situation ("erasure bound") can refute such a node without branching. The gain should show on mid-size BB codes at deeper levels (L14-16 on BB_288), where the node counts at those levels dominate.

Change

New opt-in token erasure in -cc-rules (default off; byte-identical output when off). Test-only mutants 22-24 (19-21 are used by the open GH-181 / GH-183 branches).

Rule and soundness sketch

Setting: half F = {v : H v = 0, G v != 0}, level w with the precondition that F has no element lighter than w. Node: cluster S, forbidden set B (sibling exclusion, orbit/index seed blocks, overlap / tiebreak forbids), packed rows j_1..j_p with pairwise-disjoint free candidate sets R_i (free = not in S, not in B). Region R = R_1 u ... u R_p; eligible set E = free qubits outside R.

1. Target invariant (existing). Every other rule keeps one fixed weight-w target e* reachable: S is a subset of e*, and e* avoids B ([Mac agent] CC-Ladder Hybrid: connected-cluster lower-bound engine (packing bound, orbit seeds) inside DistQLDPC #124/133/138 arguments; with tiebreak, the lex-least e* of the first useful seed, [Mac agent] CC engine: orbit-compatible even-weight overlap tie-break #162 Lemmas A-C). Nothing about e* is needed beyond e* in F, |e*| = w, S in e*, e* ∩ B = ∅.
2. Counting. Each packed row j_i is odd in syn(S) and even in syn(e*), so e* \ S has an odd number >= 1 of qubits in row j_i; they are free, so they lie in R_i. The R_i are disjoint, hence |(e* \ S) ∩ R| >= p and |(e* \ S) \ R| <= (w - |S|) - p = extra.
3. Relaxation. So e* = S + y + z with y ⊆ R arbitrary, z ⊆ E, |z| <= extra, H e* = 0, G e* != 0. The rule drops the weight constraint on y and asks: is there (y, z) with H_R y = H(S + z) and G(S + z + y) != 0? If not, no target lies under S: prune.
4. Deciding the relaxation. Eliminate the columns of R (peeling of degree-1 rows, then dense elimination of the residual stopping set, labels G carried along). (a) If some y in ker H_R has G y != 0, give up (no prune). (b) Otherwise build exactly, by back-substitution on the pivot rows, a 64-lane vector phi with phi H_R = 0 (random values on non-pivot rows) and a map F with F H_R = G_R. For any v: if phi·Hv != 0 then H v is not in colspace(H_R) (exact); if H v = H_R y then G(v + y) = G v + F H v (exact, full-width labels). The rule prunes only if every z (|z| <= extra, z ⊆ E) has phi·H(S+z) != 0 or G(S+z) + F H(S+z) = 0. A fingerprint collision (phi·H(S+z) = 0 although H(S+z) is outside the column space) can only make the rule give up; it never causes a prune.
5. Exactness. The rule never prunes a node S ⊆ e* with e* ∩ B = ∅, so the arguments of all other rules, and the level verdict, are unchanged. A FOUND is always a genuine element (closures are checked; the driver re-verifies witnesses in GF(2)).

Gate (cost only, not soundness): the test runs when extra <= 2 and 2|S| + 2 <= w, and the region has at most 128 qubits.

Plan

Tier 0: brute-force oracle ladders over rule subsets that include erasure (with and without tiebreak, all seeds, also with the gate removed by a test hook so that the rule fires at more nodes), 0 bad; mutants (22: one fewer outside qubit allowed, i.e. the bound weakened by one; 23: the fixed support S ignored; 24: the label consistency check on the region kernel skipped) must be caught; make test-cc and make test-cc-flags; smoke answers = stems, GF(2)-verified witnesses, byte identity with the token off. Tiers 1-4: 5-seed medians, +erasure vs the same rules without it, against (a) main default and (b) main default + tiebreak; nodes and time. Tier 5 (6 h) only if Tiers 1-4 pass. yfclab2 cores 44-59, one pinned process per core, 4 GB cap.

Credit: the erasure bound idea (packing-charged region plus at most two outside qubits, decided by elimination of the region with a random linear fingerprint) is from Qubitserf 04b9349 (S. Cercelescu, MIT). Re-derived for DistQLDPC's search state (forbidden set, orbit seeds, overlap, tiebreak); clean-room implementation, no Qubitserf code copied.