Distance finding and fault-tolerance tooling: Rust engine, typed inputs, DEM fault distance, docs

[ciaranra]

Distance-finding and fault-tolerance work, consolidated into one PR (previously split as #439 and #440).

1. Expose the Rust distance search and verification workflow

The incremental-weight distance search in pecos-qec and the StabilizerCodeSpec verification machinery were fully implemented in Rust but had no Python bindings and no callers. This exposes them as a supported replacement for the legacy pecos.analysis.VerifyStabilizers development loop.

• StabilizerCodeSpec with a builder: check, logical_z, logical_x, and three build modes — build(), build_verified() (errors name the exact anticommuting generator pair), and build_with_discovered_logicals() (derives paired logicals and destabilizers by stabilizer simulation).
• distance(max_weight=None, css=False, verbose=False) returning DistanceResult; min_weight_logicals(); shortest_logicals(delta) for logicals within delta of the minimum. The search grows error weight from 1, so cost scales with the distance rather than the qubit count, reaching codes the coset enumeration in StabilizerCode.distance() (capped at k + rank <= 30) cannot.
• Xs, Ys, Zs multi-qubit Pauli helpers, so checks read as Zs([0, 1]) * Y(2).
• Typed matrix input: ParityCheckMatrix (pecos-qec, role-neutral) and SymplecticMatrix (pecos-quantum, [X block | Z block]), with CSS orthogonality validated (Hx * Hz^T = 0, errors naming the offending row pair) and width-bearing zeros constructors for single-stabilizer-type codes. Phase-dropping conversions are named honestly (to_positive_paulis, from_pauli_sequence_ignoring_phase) because symplectic form carries no sign.
• Invariant fix: all three StabilizerCodeSpec constructors now reject linearly dependent stabilizers (DependentStabilizers { rank, count }). Previously num_logical_qubits() returned n - stabilizers.len() while documenting "independent generators", so redundant generators silently corrupted k — which matrix input makes easy to hit.
• Removed pecos/tools/fault_tolerance_checks.py and pecos/tools/stabilizer_verification.py, byte-identical dead copies unreachable through the public path (pecos.tools is a deprecation shim re-exporting pecos.analysis).

pecos.analysis.VerifyStabilizers itself is untouched; retiring it is a follow-up now that every capability has a Rust-backed home.

2. Consolidate the duplicate searches and parallelize

Two independent implementations of the same weight-increasing search existed. Their predicates were verified equivalent — both test "commutes with every stabilizer generator AND anticommutes with at least one configured logical" — so StabilizerFlipChecker::{has_undetectable_logical, compute_distance} now delegate to the shared engine via a new has_logical_error_at_weight. The checker's existing tests are unchanged and act as the regression guard. The combinations/pauli_product/build_pauli_string helpers are deliberately retained: analyze_weight needs configurable X/Y/Z subsets the shared iterator cannot express.

The per-weight candidate scan now runs on rayon, partitioned over support combinations. Output is bit-identical to serial rather than merely equivalent — reduction is on enumeration index, so the same operator and the same vector order come back, and tests cover both the serial and parallel branch.

PARALLEL_CANDIDATE_THRESHOLD = 65_536 candidates at one weight, derived from a measured sweep, not intuition. Below roughly 22k candidates parallelism loses (forcing the toric [[18, 2, 3]] weight-3 tier, 22,032 candidates, parallel made that search 4.6x slower); above roughly 193k it stops engaging where the time is spent (the color [[17, 1, 5]] search is dominated by its weight-4 tier, 192,780 candidates, and a higher gate erased the speedup entirely).

Benchmark	Serial	Parallel	Effect
five-qubit [[5,1,3]]	7.70 us	8.46 us	9.9% slower
Steane [[7,1,3]]	15.04 us	16.83 us	11.9% slower
color [[17,1,5]]	41.7 ms	8.6 ms	4.8x faster
shortest_logicals delta=1, color [[17,1,5]]	2.77 s	215 ms	12.9x faster

This is a trade, not a free win: microsecond-scale searches pay about 10%, while searches long enough to wait on improve 5-13x. Small-code figures were confirmed by an A/B/A run after an initial measurement proved to be machine drift. Adds benches/modules/code_distance.rs; no distance benchmark existed before.

3. Detector-error-model fault distance

Code distance is not circuit distance. A distance-5 code whose syndrome extraction spreads one fault across multiple data qubits can have fault distance 3, so code distance alone can overstate real protection. Nothing in PECOS computed the circuit-level number — check_undetectable_logical_errors enumerates failing configurations but never reports a minimum.

This adds the DEM level: the minimum number of fault mechanisms whose XOR flips no detector but flips at least one observable. With H the detector-by-mechanism matrix and L the observable-by-mechanism matrix, that is minimum |e| with H*e = 0 and L*e != 0 — structurally the same problem as code distance, which is why it lands beside the existing fault-tolerance checkers rather than in a separate silo.

• graphlike_fault_distance is exact when every mechanism flips at most two detectors, searching the parity-doubled graph with every detector AND the boundary as a BFS root. Rooting only at the boundary is not exact: a DEM whose minimum cycle avoids the boundary (D0 D1 L0 / D1 D2 / D0 D2, distance 3) leaves the boundary isolated and finds nothing. That is now a regression test.
• exhaustive_fault_distance(max_weight) is correct for any DEM including hyperedges; max_weight is required because the cost is combinatorial in the mechanism count.
• Hyperedges make the graphlike method fail fast with a count rather than being ignored. This is deliberate: DemMatchingGraph silently skips hyperedges, so building on it would have returned quietly wrong distances. The implementation reads to_mechanisms() directly and reuses FaultMechanism::{xor, is_graphlike, is_hyperedge}.
• Both methods return the witnessing mechanism set, mirroring DistanceResult::min_weight_operator — knowing which faults conspire is the point.

Guarded by a seeded property test over 512 random small graphlike DEMs asserting both methods agree on distance and on solution existence. Fixture tests alone shared a blind spot with the original design (every case happened to have a boundary edge); cross-validating an exact special case against a general reference catches the class rather than one instance. Verified by mutation: restricting the roots to boundary-only fails both the boundary-free regression and the property test.

4. Documentation

New docs/user-guide/stabilizer-code-verification.md, replacing the legacy stab_code_verification.rst narrative on the current API: the builder workflow, the ten-qubit design storyline (anticommuting pair diagnosed, then [[10, 3]] at distance 2, then [[10, 1]] at distance 3), logical-operator exploration, matrix input with its error diagnostics, and a note on choosing between the two distance methods. Ten executable doc tests, no skip markers, wired into the mkdocs nav.

Verification

Run on the combined branch:

• cargo test -p pecos-qec -p pecos-quantum: no failures
• uv run --frozen pytest across the stabilizer-code binding suites, the fault-distance suite, and the generated doc tests: 40 passed
• just build-debug and just lint (new files staged first, since pre-commit only inspects tracked files): clean

[ciaranra]

Two fault-tolerance correctness fixes have been folded in (previously #441 and a follow-on), alongside the distance tooling.

Multi-fault propagation

propagate_faults XORed every fault into the initial PauliProp and propagated from min_tick, so a fault at tick 5 was injected as though it existed earlier and intervening gates acted on a Pauli that should not yet have existed. Any weight >= 2 result was untrustworthy. It also ignored before entirely, so it disagreed with propagate_fault even at weight 1 for a before=false fault whose own tick contains a gate on its qubit.

Faults are now injected at their own tick and before/after position. The duplicated Pauli-injection mapping that let the two functions drift is now a single shared helper.

Single-leg fault enumeration

PauliFaultIterator assigned a non-identity Pauli to every qubit of a location, so at a two-qubit gate it generated only 9 of the 15 non-identity two-qubit Paulis — IX, XI, IY, YI, IZ, ZI were structurally unreachable. Each leg now chooses from identity plus the enabled Paulis, with identity-only locations rejected. The weight convention is unchanged: weight counts locations, since a two-qubit gate failing is one fault however many qubits it corrupts. pauli_types() keeps its existing public meaning; identity is handled inside the iterator.

These two bugs were masking each other. Three tests described injecting a single data-qubit X, the iterator actually produced XX, and the buggy propagation pushed XX through the CX a second time, cancelling one leg and accidentally reproducing the intended effect. Those tests now construct the single-leg fault directly and keep their original assertions, including that naive three-qubit syndrome extraction is not 1-fault tolerant.

The DAG path was already correct (possible_faults offers the identity option per qubit), so the DEM builder and the fault-distance work in this PR were unaffected.

What the enumeration fix surfaced

The omission erred toward false confidence: faults that are never enumerated cannot be found to break a circuit.

test_is_fault_tolerant_method previously reported its circuit (CX(0,1) then MZ(1)) as 1-fault tolerant for X errors. It is not. The newly reachable fault is XI after the tick-0 CX: an X on data qubit 0 alone, which the ancilla measurement never sees, leaving an undetected logical error. The test computes the verdict and only prints it, so it passed either way — its own comments enumerate XX and X-on-qubit-1 but never X-on-qubit-0-alone, matching the enumerator's blind spot.

Conversely test_repeated_syndrome_measurement_concept documents in prose exactly this fault class ("X error on data qubit AFTER its CX gate -> no syndrome in this round"); its undetectable count moves 0 -> 3, so the fix makes that description true.

No test containing an actual fault-tolerance assertion fails. Reported counts move widely, as expected when more faults are tested — for example test_fault_checker_three_qubit_code 54 -> 90 configurations, test_steane_code_fault_enumeration 16 -> 64, and the gadget-checker suites roughly triple. The full old/new delta list is available on request.

Two follow-ups worth separate attention, deliberately not changed here:

• Several diagnostics compute a fault-tolerance verdict without asserting it, so they cannot fail. test_is_fault_tolerant_method is the clearest case.
• Two tests now conflict with their own prose: test_syndrome_detection_three_qubit_code says "should be 0" and reports 3, and test_analyze_with_follow_up_resolves_ambiguity shows ambiguity rising from 3 to 15 with follow-up.

Verification

• cargo test -p pecos-qec: 829 passed, no failures
• uv run --frozen pytest python/quantum-pecos/tests/qec -q: 1140 passed, 1 skipped, 1 xfailed
• just build-debug, just lint: clean
• Both fixes mutation-verified: reverting the before/after injection order fails the after-tick equivalence and property tests; removing identity from the per-leg choices fails all four single-leg enumeration tests.

[ciaranra]

Hook-error diagnosis added (crates/pecos-qec/src/fault_tolerance/hook_errors.rs).

What it reports

PauliPropChecker::diagnose_hook_errors(data_qubits, z_ancillas, x_ancillas, logicals, min_data_weight) returns, for each amplifying fault: the responsible gate (SpacetimeLocation — tick, gate type, qubits, gate index), the injected single-qubit fault, the resulting error support restricted to the data block, whether it is detected, and whether it causes a logical error.

A hook error is defined as a fault whose OWN Pauli weight is exactly 1 but whose propagated support on the data qubits has weight at least min_data_weight. Both halves matter: a weight-2 fault landing as a weight-2 data error is not amplification and is deliberately not reported, which is what distinguishes this from a plain output-weight filter. min_data_weight is explicit with no default; 2 is the standard threshold.

detected and causes_logical_error are carried because an amplified error that still trips a syndrome does not reduce distance — only an undetected one does. Without that distinction the report would be a list of alarming faults with no way to tell which ones cost you anything.

This is why circuit fault distance falls below code distance, so the point of the diagnostic is attribution: not "your fault distance is 3 rather than 5", but which gate makes it so.

Design notes

It is a readout over existing machinery, reusing analyze_all_faults, has_syndrome, and anticommutes_with_logical; no new propagator or enumerator. data_qubits is caller-supplied rather than guessed. Output is sorted by tick, gate index, qubits, then Paulis so results are reproducible.

FaultChecker::check_output_weight_expansion is left untouched. It flags configurations exceeding an output weight but returns only the offending configurations — no resulting support, no amplification test, no gate attribution.

This diagnosis is only meaningful because of the single-leg enumeration fix in this PR: an ancilla-only fault on a CX was previously unreachable, so the analysis would have found nothing and looked correct doing it.

Rust-only for now. PauliPropChecker is not exposed to Python, so bindings are a follow-up rather than something bolted on here.

Verification

• cargo test -p pecos-qec: 835 passed, 0 failed (669 unit, 108 integration, 58 doctests)
• just build-debug, just lint: clean, with the new file staged so pre-commit actually inspects it
• Mutation-verified: relaxing the own-weight-equals-one condition fails weight_two_fault_with_weight_two_data_support_is_not_a_hook; replacing the data-qubit restriction with all propagated qubits fails the amplification test on its expected support.

[ciaranra]

Circuit fault distance and DEM search pruning added.

Circuit fault distance as a number, per logical

FaultChecker::check_undetectable_logical_errors enumerates failing configurations but never minimises — create_fault_iterator builds an iterator at exactly config.max_weight and does not scan 1..=max_weight, so the API could answer "does it fail at weight w" but never "what is the smallest w". A single aggregate also hides which logical is weakest.

Added circuit_fault_distance(...) returning CircuitDistanceResult { distance, witness, logical_index }, and per_logical_circuit_fault_distances(...) returning one entry per supplied logical. Both share one increasing-weight loop differing only in the stopping rule, and both take an explicit max_weight because the enumeration is combinatorial. The overall distance equals the minimum over the per-logical values, asserted on a case where they genuinely differ ([1, 2]).

The existing single-weight methods are untouched — they are shipped API with dependents.

Mutation-verified: collapsing the weight loop to a single weight turns the discrimination result from [Some(1), Some(2)] into [Some(2), Some(2)]; stopping the per-logical search on first hit gives [Some(1), None]; inverting the per-logical bit gives [Some(1), Some(1)].

DEM cross-validation was investigated and deliberately NOT added: the two fault models are not directly comparable. FaultChecker creates one location per TickCircuit gate batch spanning all qubits in that batch, whereas the DAG path splits locations per qubit and reconstructs two-qubit noise mechanisms separately; DEM prep/measurement faults are noise-channel-specific while this API enumerates a configured Pauli set; and DEM logical outputs come from measurement metadata rather than anticommutation with supplied final Pauli logicals. A synthesised DEM would have papered over those differences and produced a test that resembled validation without being it.

Connected-cluster pruning for the DEM search

exhaustive_fault_distance enumerates blind k-subsets, which is correct but unusable at real scale — a distance-3 surface memory DEM already has ~1300 contributions at 3 rounds and ~2050 at 5 rounds, and the literature reports ~43,000 mechanisms for an 11-round surface circuit.

Added connected_cluster_fault_distance(dem, max_weight), exact for any DEM including hyperedges, using two provable prunes:

• Connectivity. A minimum-weight undetectable observable-flipping set is connected in the shared-detector graph. If it split into components, each would be individually detector-free (no detector spans components and each appears an even number of times), observable parity XORs across components, so some component alone would be a strictly smaller solution. So clusters grow outward from a seed rather than enumerating arbitrary subsets. This is the published Connected Cluster approach (arXiv:2603.22532), credited as such in the module docs.
• Unique-detector peeling. A detector appearing in exactly one mechanism means that mechanism can never belong to an undetectable set, since the detector would flip an odd number of times. Removal can make further detectors unique, so it iterates to a fixpoint.

exhaustive_fault_distance is retained deliberately as the simple reference implementation used to validate the pruned one.

Measured on a 594-mechanism DEM with non-peelable cycle padding, so the numbers isolate the connectivity gain rather than peeling collapsing the input:

Search	Weight 3	Result
blind exhaustive_fault_distance	25-31 ms	3
connected_cluster_fault_distance	0.8 ms	3

About 38x, same answer. At weight 4 the pruned search completes in 0.8 ms; the blind search would have to consider 5.13e9 candidate subsets.

A bug this work exposed in the existing code

The extended property test caught an inconsistency introduced earlier in this PR. graphlike_fault_distance handled the weight-1 detector-free case BEFORE checking for hyperedges, so a DEM containing both a hyperedge and a detector-free observable-flipping mechanism returned Ok(Some(1)) instead of the documented hyperedge error — the distance was right, but the function sometimes refused hyperedge DEMs and sometimes answered them, depending on whether such a mechanism happened to exist. The hyperedge check is now unconditional and first. Callers wanting an answer regardless have the two methods that handle hyperedges.

Only the randomised generator surfaced this: it needs a DEM with a hyperedge AND a weight-1 detector-free mechanism together, which was case 27 of 512 and which no hand-written fixture had produced.

Tests

The seeded property test now generates hyperedge DEMs as well as graphlike ones, and asserts the blind and pruned searches agree on distance and solution existence for every case, with the graphlike method additionally agreeing where applicable. Plus fixtures for peeling reaching a fixpoint without changing the distance, and peeling preserving a witness whose detectors are all shared.

Mutation-verified: making peeling over-prune (deactivating a mechanism whose detectors are all shared) fails four tests including the property test and both distance-3 witness fixtures.

Verification

• cargo test -p pecos-qec: no failures
• cargo clippy --locked -p pecos-qec --all-targets -- -D warnings: clean
• just build-debug, just lint (files staged so pre-commit inspects them): clean

[ciaranra]

Flag fault-tolerance verification added (crates/pecos-qec/src/fault_tolerance/flag_verification.rs).

What it checks

PauliPropChecker::verify_flag_fault_tolerance(data_qubits, flag_qubits, measured_stabilizer, t) verifies the propagated-fault half of the Chao-Reichardt t-flag condition (arXiv:1708.02246): for every fault configuration of weight v in 1..=t, if no flag qubit is raised then min(wt(E), wt(E * P)) <= v, where E is the propagated data error and P the stabilizer being measured. Violations are returned with the offending configuration, v, and the computed weight.

The min encodes stabilizer equivalence: E and E * P are the same error modulo the stabilizer being measured, so checking wt(E) alone reports violations that are not violations. Worked example from the tests, on the unflagged weight-4 XXXX measurement with an X on the measurement ancilla after CX(a, 0):

E     = X1 X2 X3        wt(E)     = 3
P     = X0 X1 X2 X3
E * P = X0              wt(E * P) = 1

At v = 1, min(3, 1) = 1, so that configuration is correctly not a violation.

Scope limitation, stated rather than implied

The paper's definition also requires that a fault-free run does not flag. That is not checked here, and cannot be: PauliProp is a Pauli-frame model tracking deviations from the ideal execution, so a fault-free run has an empty frame by construction and any flag-outcome field would be permanently false while appearing to verify something. Establishing that half needs stabilizer simulation of the ideal circuit.

The verdict field is therefore named fault_condition_satisfied, not is_t_flag, and both the function and module docs say which half is covered and which must be established separately.

Tests

Six tests, built around a discriminating pair rather than a single circuit: the standard single-flag weight-4 stabilizer measurement satisfies the condition at t = 1, and the same measurement without flag interleaving fails it with a weight-1 fault producing a weight-2 data error. If both circuits returned the same verdict the check would be measuring nothing.

Also: the stabilizer-equivalence case above, restriction of weights to the caller-supplied data qubits, determinism, and a negative t = 2 case. The weight-4 flagged circuit turned out to satisfy the propagated condition at t = 2, so the negative test uses a weight-6 single-flag circuit instead of asserting something false about the weight-4 one.

Mutation-verified:

• replacing min(wt(E), wt(E*P)) with wt(E) fails the stabilizer-equivalence test (computed weight 3 instead of 1) and two others
• inverting flag detection swaps the verdicts of the good and unflagged circuits
• widening the weight computation past the caller's data qubits fails the restriction test

Verification

• cargo test -p pecos-qec: 848 passed, 0 failed (682 unit, 108 integration, 58 doctests)
• cargo clippy --locked -p pecos-qec --all-targets -- -D warnings, cargo fmt --all -- --check: clean
• just lint with files staged: clean

Python exposure is the outstanding follow-up; PauliPropChecker is not currently bound.

[ciaranra]

Exact distance certification for qLDPC-scale codes added, closing the algorithm-import item of the distance roadmap.

Method choice, from evidence rather than reputation

The large-scale empirical study arXiv:2606.12445 was read before choosing: Brouwer-Zimmermann no longer holds its traditional advantage on qLDPC codes; branch-and-bound MaxSAT wins; scalability is governed by cardinality-constraint handling (sequential counter / totalizer), XOR-aware reasoning does not systematically help; exactness comes from an incremental loop where UNSAT at weight w proves d > w and the first SAT weight is d.

DistanceProblem (crates/pecos-qec/src/distance_problem.rs)

One (H, L) GF(2) encoder serves both existing problem shapes: CSS code distance (from ParityCheckMatrix pairs or a CSS StabilizerCodeSpec; non-CSS errors clearly) and DEM fault distance (from to_mechanisms()). Tseitin XOR chains for parity, a Sinz sequential counter for the weight bound, DIMACS and new-format WCNF export with commented variable-range roles.

The trust model is the point of the design: verify_witness checks H e = 0 and L e != 0 natively, so the SAT half of any answer needs no solver trust at all; UNSAT answers (and therefore exactness) rest on the solver, and the docs say so rather than implying both halves are certified.

Tested without any solver: an exhaustive evaluator over the emitted CNF (aux variables are functionally determined, so no search) proves, for every assignment of small instances, satisfiability at bound w iff the native predicate holds — cross-checked against the existing distance searches on Steane and the repetition-triad DEM, with both sides of the sequential-counter boundary pinned and lying-solver mocks rejected. Mutation-verified at every layer, including a Tseitin polarity flip (kills five tests) and counter off-by-one.

In-process backend: certified_distance via batsat

Per the backend decision, a pure-Rust solver: batsat 0.5 (MiniSat 2.2 reimplementation, MIT, sole transitive dependency bit-vec). Fed from the internal clause representation; a fresh deterministic solver per weight. batsat receives no more trust than an external solver — its models pass through verify_witness before being believed, and that guard is mutation-proven: an off-by-one in model extraction is caught by the certification layer as InvalidWitness (OddCheck), not accepted.

Measured capability, not aspiration

Bivariate bicycle codes built in-test from their polynomial definitions, sanity-checked (n, CSS orthogonality, k via F2Matrix rank) before timing:

Code	Result	Total time
BB [[72,12,6]]	d = 6 certified, witness verified	~0.4 s
BB [[144,12,12]] (the gross code)	d = 12 certified, witness verified	~15 min

Per-weight profile on the gross code: UNSAT proofs escalate (w=10: 163 s, w=11: 674 s), then SAT at w=12 in 1.3 s — proving d > 11 is where the time goes. For comparison the study's MaxCDCL does this instance in ~48 s, so the pure-Rust backend is roughly 19x off the state of the art but completes the flagship qLDPC benchmark entirely in-process. The WCNF export is the documented path to external MaxSAT solvers for anyone needing the faster regime; both were measured, neither is guessed.

These are regimes the existing weight search cannot touch (C(72,6) * 3^6 alone is ~1e11 candidates).

Verification

• cargo test -p pecos-qec: 697 unit + 108 integration + 58 doctests, 0 failures (BB probes are #[ignore]d timing tests, run separately)
• cargo clippy --locked -p pecos-qec --all-targets -- -D warnings, cargo fmt --all -- --check: clean
• just lint including the dependency-integrity gate over the new lockfile entries: clean

Python bindings for DistanceProblem/certified_distance are the noted follow-up.

[ciaranra]

Generic CSS syndrome extraction via Tanner-graph edge coloration — and its measured distance cost.

Any CSS code's (Hx, Hz) now builds a valid memory circuit: exact Delta-edge-coloring of each Tanner graph (Konig; construction per arXiv:2308.08648), each color class a depth-1 CNOT matching, entangling depth DeltaZ + DeltaX. The coloring helper is general graph machinery in pecos-num with its own tests; the detector/observable wiring is factored into shared machinery now used by both this builder and the specialized BB one. Validity is guaranteed and tested (fault-free DEMs are empty; a corrupted coloring is rejected independently by the matching verifier and by TickCircuit's same-tick qubit exclusivity).

Distance preservation is deliberately NOT claimed — it is measured, and the first measurement is a finding:

• Steane, two cycles of naive coloration: circuit fault distance 2 against code distance 3, per-observable minimum at observable 0, witness = two mechanisms with identical detector support [3,4,5,6] where exactly one flips the observable. A hook-error path, located by the check-driven cluster search in ~210 us and reproduced independently.
• BB [[72,12,6]] under coloration: 12 entangling layers/cycle versus the specialized schedule's 7 (31 vs 18 ticks for the two-cycle experiment).

So the generic builder gives every CSS code a correct schedule and, combined with the fault-distance tooling in this PR, a measurement of what that schedule costs — which is precisely the workflow for judging whether a specialized schedule is worth designing. The direction-bracket scheduler family (arXiv:2504.02673) is noted as a possible future addition.

Verification: cargo test on pecos-qec and pecos-num clean; cargo test -p pecos --features neo clean (gate-handling blast-radius guard); Python QEC suite 1155 passed; clippy/fmt/build/lint clean.

[ciaranra]

Bounded-enumeration exact distance (the Brouwer-Zimmermann family) added, CPU only — completing the exact-method portfolio with the dense-code regime.

Method per the modern treatment in arXiv:2408.10743, with the random-information-set upper seed of arXiv:2308.15140: greedily peeled disjoint information sets over a kernel basis of H; level loop enumerating d-row combinations per active systematic generator; lower bound LB(d) = sum max(0, (d+1) - (K - r_i)) with even-weight upward rounding; exact termination when LB >= UB. Both bounds are computed natively, so the certificate carries NO trust caveat — unlike the SAT path's solver-trusted UNSAT half. Budget exhaustion returns the honest interval (proven lower bound plus best witness) rather than None. Witnesses are natively verified before acceptance, as everywhere else in this PR.

Entry points mirror the connected-cluster family (code/x/z/stabilizer variants, the last via the same three-mechanism reduction, so the five-qubit non-CSS code is covered), with Python bindings.

Measured regime map (release, reproduced independently):

Case	Bounded enumeration	Check-driven CC	SAT
Dense seeded CSS [[40,8]]	1.2 ms	3.7 s	3.4 s
Steane (sparse)	71 us	11 us	152 us
BB [[72,12,6]] (sparse)	35 ms	2.6 ms	66 ms

Roughly 3,200x over both other methods on the dense case; connected-cluster keeps the sparse regime, as expected and as now documented by data in both directions. The seeded property test cross-validates bounded enumeration against the exhaustive DIMACS minimum alongside the other methods.

Mutations: the d+1 -> d lower-bound off-by-one moves a hand-analyzed [6,2,4] termination from level 1 to level 2 and is caught; disabling even-weight rounding demotes an exact certificate to an interval and is caught; disabling the L-trigger is caught by three-way agreement.

Verification: cargo test -p pecos-qec full suite clean; workspace clippy -D warnings; cargo test -p pecos --features neo (blast-radius guard); Python QEC suite 1157 passed; build/lint clean.

[ciaranra]

wgpu backend for the bounded-enumeration level loop — shipped with an honest verdict, and the packet's real win was on the CPU.

The seam and the CPU windfall

The level loop now runs through a backend seam: the packed CPU backend (bit-packed word-major rows, prefix-cached XOR walk) is the default, and it transformed the method — a dense [[80,16]]-class instance that previously ran 14+ minutes without finishing now certifies in 91 ms. All existing results are bit-identical; the full regression net passes untouched.

The GPU backend, measured on real hardware

The WGSL kernel (combination unranking, packed XOR, popcount, atomic-min per level; witnesses reconstructed deterministically on CPU so results are bit-identical) was audited on an RTX 4090: the seeded 64-case CPU/GPU agreement suite, level boundaries, and the hand-analyzed termination case all pass on hardware.

Performance (RTX 4090, Vulkan, release):

Dense case	CPU	GPU
[[40,8]]	0.98 ms	313 ms
[[64,12]]	8.1 ms	266 ms
[[80,16]] (d=13 instance)	91 ms	276 ms

The GPU loses every measured case to a ~270 ms dispatch floor. It is retained anyway, with this framing documented: it is an additive optional backend in pecos-gpu-sims behind a clean seam (no core-path cost, unlike the reverted incremental-SAT experiment), correctness is hardware-verified, and the deep regime is genuinely open — instances exist (by seed draw, not construction shape) where the packed CPU backend still runs 10+ minutes, and the [[80,16]] ratio suggests GPU break-even near CPU-seconds with plausible wins beyond. The CPU backend is the recommendation until such a case is measured end to end.

GPU-availability handling follows the repository policy (explicit adapter detection and rejection of software rasterizers; the sandbox environment sees only llvmpipe and skips cleanly — hardware verification above was run outside it).

Verification: cargo test on pecos-qec and pecos-gpu-sims audit clean; clippy -D warnings on both; neo blast-radius guard; Python QEC suite 1157 passed; build/lint clean.

[ciaranra]

Operator coset weights and classical distance — the first packet implemented directly rather than dispatched, and the trust architecture caught its own author.

What landed

• certified_coset_weight(group, representative, max_weight) — exact minimum weight of representative + rowspan(group). Coset membership is an affine condition (D e = D p for the dual basis D), so the DistanceProblem encoder gained affine parity targets (a target-1 row negates its Tseitin chain's final forcing literal). No nontriviality constraint: weight 0 legitimately means the representative is in the group, certified without a solver call.
• certified_stabilizer_coset_weight(spec, operator, max_weight) — the same for any stabilizer code via the plain symplectic representation with per-qubit-support weight, so Y costs one. The discriminating fixture: the five-qubit logical XXXXX has raw weight 5 but coset weight 3 (XXXXX * XZZXI = IYYIX).
• logical_coset_weight_profile(spec, max_weight) — the per-logical minimum-weight table (Z basis then X basis); Steane profiles to all 3s, and any stabilizer element costs 0. This complements the existing whole-group minimizers (find_min_weight_logicals_with_info classifies classes; shortest_logicals walks the spectrum): same question, per-coset and exact at scale.
• certified_classical_distance(h, max_weight) — minimum nonzero kernel weight, since the quantum constructions in this PR are built FROM classical codes whose distance controls the quantum bounds. Cross-validated against the bounded-enumeration route.

All four bound to pecos.qec and driven end to end from Python as verification.

The bug story, told on myself

The first implementation of the affine path returned None for cosets that provably contained weight-3 elements. The discriminating probe was the architecture's own: verify_witness ACCEPTED a hand-constructed coset element that the emitted CNF rejected — native verification disagreeing with the encoding localizes the bug to the encoder in one step. The cause: with an empty logical block, the nontriviality encoder emitted an EMPTY CLAUSE (instant unsatisfiability); the requirement flag had been wired into the verifier but not the encoder. The same asymmetric-trust design that guards against lying solvers guards equally against a wrong encoder.

Mutations, both killed with sha-verified restores: ignoring the affine targets fails all five coset tests; dropping the nontriviality requirement drives classical distance to 0 against the asserted 3.

Verification

• cargo test -p pecos-qec: full suite clean (24 in the module, 5 new)
• cargo test -p pecos --features neo: clean (blast-radius guard)
• clippy -D warnings both crates, fmt, just build-debug, just lint: clean
• Python QEC suite: 1157 passed; smoke-driven from a user's REPL

[ciaranra]

Hypergraph-product code construction — the family unlock, closing the second item of the borrow list.

HypergraphProductCode::new(h1, h2) builds the Tillich-Zemor product (arXiv:0903.0566) of any two classical parity-check matrices: Hx = [H1 (x) I | I (x) H2^T], Hz = [I (x) H2 | H1^T (x) I] on n1*n2 + r1*r2 qubits, with CSS orthogonality asserted (it holds identically; the assertion fails fast on implementation error, and the factor-swap mutation confirms it fires — caught by three tests). Logical bases come from the same discovery machinery the coloration and BB builders share. A F2Matrix::kronecker primitive was added where general GF(2) machinery lives, with its own direct unit test.

Oracles, both engines agreeing:

• repetition [3,1,3] squared -> [[13,1,3]], distance 3 (connected-cluster and bounded enumeration)
• Hamming [7,4,3] x repetition [3,1,3] -> [[27,4,3]], with the transpose-code arithmetic derived in the test comments (both inputs full row rank, so the transpose contributions vanish) and the distance measured rather than assumed

Bound to pecos.qec and driven from Python. With the previous packet's certified_classical_distance, the full pipeline now closes: grade the classical inputs, construct the quantum code, certify its distance, build its extraction circuit with the coloration scheduler, and measure the circuit-level cost — end to end in one library.

Verification: pecos-qec + pecos-quantum suites clean; neo blast-radius guard clean; clippy -D warnings across the three touched crates; build/lint clean. Implemented directly (solver-tooling outage), same packet discipline: oracle fixtures, mutation kill with sha-verified restore, user-driven smoke.

[ciaranra]

Subsystem-code dressed distance — closing the fifth borrow-list item via pure engine reuse.

subsystem_dressed_distance(num_qubits, stabilizers, gauge_generators, logical_zs, logical_xs, max_weight) computes the dressed distance of a gauge code by the stabilizer-only reduction: the (H, L) problem with H from the STABILIZER generators alone and L from the BARE logicals. Gauge operators need no special handling — they commute with the stabilizers and with the bare logicals, so they are excluded from witnesses automatically, while dressed representatives (bare logicals times gauge factors) remain reachable. The search is the check-driven cluster engine; nothing new was built below the validation layer.

Validation enforces the subsystem structure before searching, with named indices on failure: every gauge generator must commute with every stabilizer, and every bare logical with every gauge generator. Skipping the validation is caught by both rejection tests (mutation run with sha-verified restore).

Oracles: Bacon-Shor on the 3x3 grid gives dressed distance 3 (agreed independently by the certified SAT path over the same specification), and the rectangular 2x3 grid gives 2 — the min(m, n) law, measured. The fixtures build the full gauge/stabilizer/bare-logical structure from the grid definition in test code.

Rust-only for now (Python binding to follow with the remaining item). Verification: pecos-qec suite clean, neo blast-radius guard clean, clippy -D warnings, build/lint clean. Implemented directly, same packet discipline.

Remaining from the borrow list: item 4 (BP-OSD randomized upper bounds for large DEMs), queued as a dispatch packet — it needs decoder-API reconnaissance that a fresh implementer session does best.

[ciaranra]

The open circuit-distance question is now closed, exactly.

BB [[72,12,6]] depth-8 schedule: circuit fault distance = 6 = code distance

The check-driven connected-cluster search completed the two-cycle circuit DEM (4,284 fault mechanisms, 12,564 contributions) and returned exact distance 6 with the natively verified witness [0, 2, 51, 100, 163, 259]. Runtime was about 14 hours single-threaded — three orders of magnitude slower than the same engine on the code-level problem, which matches the structural reason: circuit DEM detectors have far higher degree than code Tanner checks, so the check-driven branching factor grows accordingly.

The earlier reported bound of 4 <= d <= 6 is therefore an equality, and the showcase this PR set out to demonstrate is complete: PECOS constructs the published depth-8 bivariate-bicycle syndrome-extraction schedule and independently certifies that it preserves the code distance — measured with PECOS's own tooling, not assumed from the design intent.

For contrast, the same engine certifies the [[144,12,12]] gross code's CODE distance in about 22 seconds. Circuit-level exactness at this scale is reachable but expensive; the randomized upper-bound path (BP-OSD sampling over the same (H, L) DEM formulation) remains the practical tool for larger circuits and is the one outstanding item on the improvement list.

Also in this push: renamed an ambiguous single-letter variable in the certification binding tests (ruff E741 — CI's ruff enforces it, the locally pinned version does not).

[ciaranra]

Randomized decoder-based upper bounds on DEM fault distance — the last item of the improvement list, and it reaches the regime every exact method in this PR cannot.

The result

randomized_fault_distance_upper_bound(dem, config): for a sampled nonempty observable subset S, decode the augmented system [H; l_S] e = [0; 1] with the in-tree BP-OSD decoder (arXiv:1904.02703), keeping the lightest verified candidate. Sampling strategy follows the randomized information-set idea of arXiv:2308.15140.

DEM	Mechanisms	Samples	Verified upper bound	Time
BB [[72,12,6]], 2 cycles	4,284	1	24	0.2 s
"	"	4	9	0.8 s
"	"	8	6	1.5 s
BB [[72,12,6]], 5 cycles	13,212	24	8	17 s
"	"	48	6	35 s

The two-cycle exact circuit distance is 6, established earlier in this PR by a search that ran about 14 hours. The sampler reaches the same value in 1.5 seconds — roughly a 34,000x reduction in time to that number, with the crucial difference that it is a bound rather than a certificate. The five-cycle DEM is beyond any exact method here; its bound of 6 is reported as a bound and nothing more.

Why a heuristic decoder is safe here

Every candidate passes DistanceProblem::verify_witness (all H e = 0 rows plus L e != 0) before it may tighten the incumbent. A misbehaving decoder can therefore only fail to help; it cannot corrupt the answer. That guarantee is tested directly: a stub returning a deliberately invalid vector is rejected and leaves the bound unchanged. Same asymmetric-trust architecture as the SAT path.

The API is named and documented so the result cannot be mistaken for an exact distance — FaultDistanceUpperBoundResult carries an explicit bound_kind, and the docs never use "distance" unqualified. The config is fully explicit (samples, seed, subset strategy, and every BP-OSD parameter), consistent with the repository's no-silent-defaults policy; the same seed reproduces the same bound and witness exactly, verified.

Also guarded: bound >= exact on cases where the exact value is known (repetition triad and a distance-3 surface memory, both reaching equality), zero samples returns None rather than a meaningless number, and a DEM with no undetectable logical error returns None however many samples run.

Deviation worth noting: seeded randomization currently varies the observable subset only, not per-sample priors or column orderings — a possible future tightening.

Verification: cargo test -p pecos-qec 752 unit tests plus integration and doctests clean; Python QEC suite 1,162 passed; clippy -D warnings, fmt, just build-debug, just lint, and the --features neo blast-radius guard all clean. Headline reproduced independently from Python before shipping. pecos-ldpc-decoders added as a workspace dependency of pecos-qec (in-tree crate, no external dependency).

[ciaranra]

External validation: the exact engine reproduces a third party's published qLDPC code parameters.

A publicly available MIT-licensed qLDPC processor toolkit ships finalized code families as raw check matrices (Hx, Hz, Lx, Lz) with documented invariants. Taking its [[150,30,10]] mitten code — data this library has never seen, ten times the qubit count of the largest code tested in this PR so far — and verifying the source's own invariants first (CSS orthogonality, logical kernel membership, Lx Lz^T = I, all hold):

Search	Result	Time
check-driven connected-cluster, Z side (Hx, Lx)	distance exactly 10	83 s
check-driven connected-cluster, X side (Hz, Lz)	distance exactly 10	65 s
lower bound d > 8 alone	proven	7.8 s

This matches the published [[150,30,10]] parameters. Every previous test in this PR used fixtures PECOS constructed itself; this reproduces an independent group's result from their raw matrices, and produces an exact certificate where the tooling that discovered those codes yields randomized upper bounds.

Scaling is roughly 40x per two additional weights of exhaustive proof, which places the larger members of that family (up to [[1200,240,20]]) beyond exact reach — the honest boundary of the exact engines, and the case for the randomized-bound tooling already in this PR at DEM level.

No external data or code was copied into the repository; this was a local validation run against the cloned toolkit.

[ciaranra]

Adversarial review cycle closed: two independent review rounds, fourteen findings, all fixed and regression-tested.

Round 1 (10 findings against the recently added distance/coset machinery) and round 2 (4 findings against round 1's own fixes) are both fully addressed. The second round existed because fixes written under review pressure are biased toward the reviewer's exact cases — and it proved the point: round 1 added a logical-count check, and round 2 demonstrated that count without kind still certifies false distances in both directions.

The last commit closes round 2:

• Every distance entry point now validates the full premise, not just the logical count: stabilizer isotropy, logical-vs-stabilizer commutation, and canonical pairing, composed into one StabilizerCodeSpec::verify_as_complete_code(). The reviewer's live counterexamples — a frozen-qubit-tensor-Steane spec that certified distance 1 (true distance 3), a duplicated logical pair that reported 3 (true distance 1), and an anticommuting "stabilizer" set with no code space at all — are now named rejections and permanent regression tests. Both new guards are mutation-verified.
• subsystem_dressed_distance applies the same full structural verification to its bare logicals (with completeness deliberately replaced by the gauge-aware count relation).
• Search budgets clamp to the maximum possible witness weight, making the budget-exhausted lower_bound = max_weight + 1 invariant overflow-free and removing the saturating-arithmetic workaround.
• The validation found real fixtures wrong: a long-standing test fixture and five user-guide examples used X0 as the three-qubit bit-flip code's logical X — an operator that anticommutes with the Z0Z1 stabilizer and was never a logical at all. All corrected; the guide's Steane distance example now asserts distance == 3 in its generated doc test instead of silently skipping inside an if let.

What the second round confirmed sound, after targeted attack: the gauge-center rank correction under dependent generators, the outcome enums and their Python attribute surfaces, the fallible-API migration (no panicking callers), and all of round 1's edge-case fixes.

Full verification on the final state: 775 Rust unit tests plus integration and doctests, regenerated guide doc tests, clippy -D warnings, fmt, debug build, 1,166 Python QEC tests, and the neo feature guard — all green.

[ciaranra]

Review round 3 — a final scoped pass over the one previously unreviewed diff (the round-2 fixes themselves) — is closed. Two findings, both fixed in the last commit; the declining yield across rounds (10, then 4, then 2) says review has converged.

Fixed:

• Mismatched logical lists — the Rust mutators (add_logical_z/add_logical_x) could build a spec with unequal Z/X lists; completeness counted only the Z side and the pairing checks iterate over the shorter list, so a one-sided spec passed full validation and a search could certify a wrong distance while the Z-only engines saw an empty logical matrix. Now rejected with a MismatchedLogicalLists error naming both counts; regression test from the reviewer's exact construction; guard mutation-verified.
• Doc examples and weak fixture assertions — the crate-level docs and README still showed X0 as the bit-flip code's logical X (the invalid operator the round-2 fixture fix corrected elsewhere), and the fixture-dependent tests asserted only inequalities that the invalid fixture would also have satisfied. Docs corrected; the weight-1 analysis test now pins exact counts (0 stabilizer-equivalent, 3 undetectable, 6 detectable-with-logical) that discriminate the valid fixture from the invalid one — values confirmed by execution.

Verified clean under targeted attack, closing the questions round 3 was scoped to answer: discovered logicals are index-paired by the tableau invariant, so the stricter validation cannot reject any discovered spec (exhaustively checked through three qubits, including Y-containing cases); non-CSS handling is intact; budget clamping covers every outcome-producing path; and the subsystem bare-logical pairing argument holds by commutation with the full gauge group, not by fixture luck.

Three review rounds, sixteen findings total, all fixed, every counterexample now a permanent regression test. Full gates green on the final commit.