Adopt GH-146 Stern finder as default (both engines); tier5 stems get verified upper bounds

MODIFICATIONS.md

@@ -31,6 +31,7 @@ New code, not derived from MaxCDCL.
 | Frontier branching with a structural selector (GH-129 + GH-130; default since 2026-10-18, PI decision) | Split MaxSAT path only. `Solver::pickFrontierLit` (new, +190 lines in `src/solver/Solver.{h,cc}`): with frontier branching on, a decision first looks for an odd parity row of the half (true qubits of odd parity, some qubits unassigned), takes the row with the fewest unassigned qubits (ties by index) and decides its most active unassigned qubit (VSIDS or LRB score, whichever phase is current) to 1; if no row is odd, the normal decision is used. The half's parity rows are passed from `run_css_half()` (as GH-121 did); the odd-row state is updated lazily from the trail at each decision (< 1% of the profile). Only the decision order changes, never the formula. `-frontier=auto` (default) enables it per CSS half iff the half's parity matrix has fewer than 3 Tanner 4-cycles per row (sum over row pairs of C(\|r ∩ s\|, 2) divided by the number of nonzero rows), computed once before the search and printed with `-v`; `-frontier=off` = the search of main before GH-130 (byte-identical `-v` logs); `-frontier=on` = every half; `postsol` / `presol` = only after / before the probe's first solution; `-frontier-stats` per-probe counters, `-frontier-check` re-verifies the incremental row state (debug). Evidence: GH-129 (`on` everywhere: tiers 1-2 0.4-0.6x main on 5-seed medians, but every TN cell slower, refutations ~36% more time per conflict) and GH-130 (`auto`: BB/GB/LP cells 0.14-0.90x, TN cells identical to main, Tier 5 no cell worse, LP_714/LP_1020 solved 2.3-3.9x sooner). Caveats recorded in `optimization/experiments/GH-130/REPORT.md`: the 4-cycle count separates TN from BB/GB/LP on the bundled codes but was not shown to be the cause of the TN slowdown, and it depends on how the parity matrix is written (redundant rows raise it). |
 | Odd-cap skip (GH-133; default on since 2026-10-21, PI decision; `-oddcap-skip=off` = previous search) | Split MaxSAT path only, `-oddcap-skip=on`: for a CSS half whose parity matrix H has only odd column weights every element of ker H has even weight (proof below, `src/cc/`), so an odd probe cap m is equivalent to the cap m - 1 and a NONE at an even cap 2t certifies the lower bound 2t + 2. Phase 1 (doubling caps): cap 1 is not probed (lb 2), and after a NONE the lower bound is raised to the next even value; Phase 2a: cap U-1 -> U-2 when U-1 is odd; Phase 2b/3: an odd optimisation cap U-1 (dual-half elimination) -> U-2. The decision per half is printed with `-v` (`c oddcap X: ...`). `-oddcap-skip=off` (default) leaves main's cap sequence byte for byte (identity verified on tier0+1 x 2 modes). The encoding, the cardinality constraints and the solver are unchanged. See `optimization/experiments/GH-133/`. |
 | Verified upper-bound pre-pass for the MaxSAT split (GH-144; `-ub-pre=off\|on\|S`, default on = 60 s since 2026-10-23, PI; silently off with -joint/-roundingsat unless given explicitly) | Split MaxSAT path only. Before Phase 1 the GH-140 finder (`src/cc/cc_ubsearch.h`, `UbFinder`) runs on every half that has logicals (X half: H = Hz, G = Gx, S = Hx; Z half: H = Hx, G = Gz, S = Hz) for at most S seconds (`on` = 60 s), always looking for a word lighter than the current bound; a half stops after `-ub-pre-hits=H` (16) re-hits of the bound or max(`-ub-pre-plateau=P` (1000), 4 x the iteration of its last improvement) iterations without improvement (iteration based: deterministic for a given `-seed` unless S ends it). Every word is verified (`ubpre_verify`: Hpar e = 0 and Glog e != 0 directly on the input matrices, plus `distcc::verify_logical`); a failure discards the pre-pass. The lightest weight U0 is the initial UB (pipe `UB U0`, printed `c d_ub: U0`) and each half's lightest word its incumbent. With U0: Phase 1 still probes a half with a pre-pass incumbent but only at caps < U - 1; Phase 2a runs on both halves (not only on ties) with feasibility probes at U - 1 and reports the global lower bound after each probe; Phase 2b optimises each unfinished half with cap U - 1. `-ub-pre=off` or no verified word = main byte for byte (identity verified on tier0+1 x 2 modes). Soundness below (GH-144). See `optimization/experiments/GH-144/`. |
+| Stern / Dumer collision mode of the shared finder (GH-146; `-ub-isd=off\|stern\|dumer[:P,L,W,B,R]`, default stern since 2026-10-23, PI; `-ub-isd=off` = previous finder, GH-140) | Applies to the CC `-ub-search` finder and to the MaxSAT `-ub-pre` pre-pass (both use `UbFinder`). Per round: W Canteaut-Chabaud pivot swaps on the stored systematic columns (or a fresh elimination), a random split of the information set into two halves and a random window of L reduced rows; all subsets of size <= P of each half (`dumer`: the window pivot columns are elements too), bucketed by the window part of their column sum; every colliding pair with different detector parities is weighed, kept words go through the unchanged detector check, stabilizer local improvement and the driver's / pre-pass's independent verification. Single systematic words are also tried every round. Defaults from S0: P 2, L automatic (about log2 of the list size), W 32, B 1 round per iteration. `-ub-isd=off` = the GH-140 enumeration byte for byte (identical to GH-144's 6d2b7a1 on tier0+1). Soundness below (GH-146). See `optimization/experiments/GH-146/`. |
 | CC engine switch (GH-124 S0, experimental) | `-engine=maxsat` (default) leaves the search above unchanged (byte-identical `-v` logs); `-engine=cc` runs the connected-cluster level search of `src/cc/` on the same CSS split through the same pipe protocol and output; `-engine=auto` is a structural selector (not the default): CC unless a half's parity matrix has a row of weight > 32 or, for n >= 64, a mean row weight > n/4 (pre-S1 rule; every bundled code goes to CC). `-seed=N` (timing seeds): N > 0 sets `random_seed` of every MaxCDCL solver on the MaxSAT path from the application layer (the engine source is unchanged; N = 0 or no flag keeps main's search byte for byte) and equals `-cc-seed=N` with the CC engine. A CC no-answer stop sends `RESULT -1 TRAP` on the pipe, and the parent withdraws the bounds it had received (MaxSAT never sends it). `find_dual_maps` additionally keeps the verified qubit maps (its report output is unchanged). Flags: `-seed`, `-cc-rules`, `-cc-dual`, `-ub-basis`, `-ub-search` and `-cc-ub-*` (GH-140), `-cc-seed`, `-cc-trace`, `-cc-stats`, `-cc-mutant` and `-cc-schedule` (tests only). Conflicting combinations are rejected (exit 1): CC flags without `-engine=cc\|auto`; `-joint`, `-roundingsat`, the dumps and `-native-parity-opb` with `-engine=cc\|auto`; the cardinality flags and `-dualshare-stats` with `-engine=cc` (`-engine=auto` warns about the flags its choice ignores). See `optimization/experiments/GH-124/`. |
 
 ### `src/cc/` (GH-124, experimental; new code, not derived from MaxCDCL or any third-party code)
@@ -40,7 +41,7 @@ Optional engine, off by default (PI 2026-10-16): enable with `-engine=cc` (or `-
 | File | Description |
 |------|-------------|
 | `cc_half.h`, `cc_half.cc` | Exact connected-cluster (CC) level search for one CSS half (Dumer, Kovalev, Pryadko 2017): clusters grown from a seed along one odd parity row at a time; syndrome-free clusters below the level are dead ends (a nontrivial one is reported as an inconsistency); rules `excl` (sibling exclusion), `pack` (disjoint odd-row packing bound), `orbf` (orbit seeds from the GH-85 verified per-half orbits, replacing the index rule), `mrv` (fewest-candidate branching), `parity` (GH-133: odd levels skipped on a half whose column weights are all odd; per-node parity check), `leaf` (GH-133: Zobrist hash from column to qubit; the closing qubit is looked up at budget 1, and at budget 2 each candidate is completed by one lookup), `overlap` (GH-138: a minimum logical meets every same-type stabilizer row g in at most floor(\|g\|/2) qubits; incremental counters, the rest of a tight row is forbidden); uint64 bitsets with an incremental syndrome; `-cc-seed` relabeling; test-only mutants 1-3 (1 forbidden set not restored, 2 packing prune `>=`, 3 orbit seed rule off by one) and 5-7 (5 parity forced on a half with an even column weight, 6 leaf budget off by one, 7 leaf closure without the detector check) and 8-10 (GH-138: 8 overlap limit off by one, 9 parity checks used as stabilizer rows, 10 even-weight tie cut). |
-| `cc_ubsearch.h`, `cc_ubsearch.cc` (GH-140) | Randomized low-weight logical finder for one CSS half (`-ub-search`): random information sets (random column order, Gauss-Jordan elimination of H with pivots in that order, systematic kernel basis), words of 1-2 (optionally 3) systematic basis vectors below a weight threshold, detector check (G c != 0), greedy local improvement by same-type stabilizer rows; deterministic per seed; test mutant 11 (no detector check and no improvement). |
+| `cc_ubsearch.h`, `cc_ubsearch.cc` (GH-140, GH-146) | Randomized low-weight logical finder for one CSS half (`-ub-search`): random information sets (random column order, Gauss-Jordan elimination of H with pivots in that order, systematic kernel basis), words of 1-2 (optionally 3) systematic basis vectors below a weight threshold, detector check (G c != 0), greedy local improvement by same-type stabilizer rows; deterministic per seed; test mutant 11 (no detector check and no improvement). GH-146 collision mode (`-ub-isd`): Stern / Dumer collision step with Canteaut-Chabaud pivot swaps (`cc_swap`, `isd_round`, `iterate_isd`), parser `parse_isd`. |
 | `cc_driver.h`, `cc_driver.cc` | Driver: start-up detector check (rank[H;G] + rank S = n and commutation), both halves interleaved level by level (cheaper half first) or one half under a verified XZ-dual map, stop rule (a hit at level w ends the run once the other half's lower bound is >= w), anytime `TRY`/`LB`/`UB`/`RESULT` lines, witness verification (H e = 0, independent GF(2) rank test against the same-type stabilizers, dual image check), its own check of the XZ-dual map (pi(rs Hz) = rs Hx and pi(rs Hx) = rs Hz), always-on traps (`RESULT -1 TRAP`, never a value; earlier bounds withdrawn), optional `-ub-basis`, `-cc-trace`, `-cc-stats`; test-only sequential schedule (`-cc-schedule=sequential`) and driver mutant 4 (stop rule without the other half's lower bound, run under the sequential schedule). |
 
 Tests: `tests/test_cc_engine.cc` (`make test-cc`): brute-force oracle on random halves and random consistent CSS
@@ -218,6 +219,41 @@ d = 3..5). `make test-cc-flags`: values, conflicts (`-engine=cc`, `-joint`, `-ro
 `-ub-pre`), `-v` lines, the first `c d_ub` line, the probe caps on BB_90_8_10, no output with `-ub-pre=off`.
 *Evidence.* `optimization/experiments/GH-144/REPORT.md`.
 
+GH-146 (`-ub-isd=off|stern|dumer[:P,L,W,B,R]`, `src/cc/cc_ubsearch.{h,cc}`; `stern` by default since 2026-10-23, `off` = GH-140). *What it adds.* A second
+enumeration inside `UbFinder::iterate` for both users of the finder (CC `-ub-search`, MaxSAT `-ub-pre`); the drivers,
+their schedules, stop rules and verification are unchanged. Written from the published algorithms (Stern 1988;
+Dumer's and Finiasz-Sendrier's split with an overlapping window; the Canteaut-Chabaud random walk on information
+sets); no third-party code was read. *Why every word is still a nontrivial logical.* (1) *Systematic invariant.* After
+the first random elimination the finder stores, for each information column j, the column A_j of the reduced matrix
+over the r pivot rows, so c_j = e_j + sum_i A[i][j] e_{P_i} is in ker H (row i reads A[i][j] + A[i][j] = 0). A
+Canteaut-Chabaud swap picks an information column j with A_j != 0 and a pivot row i with A[i][j] = 1 and performs the
+GF(2) row operations "add row i to every other row with a 1 in column j": column j becomes the unit vector e_i (the
+new pivot of row i), the old pivot column P_i takes the vector A_j (it now has a 1 in row i and in every row that
+received row i), and every other information column j' with A[i][j'] = 1 gets A_j' + A_j + e_i. Row operations keep
+the row space of the reduced matrix equal to that of H, so the invariant (identity on the pivots, ker H spanned by
+the c_j) holds after any number of swaps; `build_word` reconstructs a word from its information indices with the
+current columns and pivots. (2) *Collision.* A colliding pair contributes the word sum_{j in T1 u T2} c_j (T1, T2
+disjoint sets of information indices), which is in ker H by (1); in Dumer mode a window element contributes only to
+the key and never to the word, so the word is still a sum of c_j. The weight used for the threshold is |T1| + |T2| +
+|sum A_j| (exactly the word's weight). The detector-parity precheck skips pairs whose words have G c = 0 (trivial);
+it is an optimization (a skipped word could only be trivial), and every kept word still passes the same check as in
+GH-140 (G c != 0, computed from the cached detector parities of the c_j) before local improvement by rows of S (G g =
+0, H g = 0: same logical class). (3) *Independent verification.* Unchanged: the CC driver verifies every word with
+`verify_in_half` (H e = 0, e not in rs S by its own echelon form; with a dual map also the image) before it lowers
+ub_h / U, and the MaxSAT pre-pass with `ubpre_verify` (H e = 0 and Glog e != 0 on the input matrices, plus
+`distcc::verify_logical`); a failure traps (CC) or discards the pre-pass (MaxSAT). So no lower bound and no answer
+depends on the collision step; it only changes which verified words are found and when. *Determinism.* The swaps,
+splits and windows come from the finder's seeded splitmix64 stream, so the word sequence is fixed per `-seed` (the
+pre-pass, being iteration based, stays deterministic). *Tests.* `make test-cc`: six collision configurations (Stern /
+Dumer, P 1 and 2, windows automatic / 0 / 2 / 3, walks 0 / 1 / 8 / 32, batches 1-3, refresh 5) on the 400 Part B
+halves (every word in ker H, nontrivial, below the target and >= the true half distance; same seed, same words; d_h
+reached on >= 90 % of the halves is required, 400/400 observed), mutant 11 in collision mode (trivial words returned),
+the CC driver in collision mode (pre-pass, late start, finder-only; mutant 11 must trap, mutant 12 - words reported
+without verification - must answer wrongly), the MaxSAT pre-pass in collision mode (budget 1 s, cut after 2
+iterations; mutant 1 stays correct, mutant 2 must answer wrongly) and rotated surface codes. `make test-cc-flags`:
+values, conflicts (`-ub-isd` without a finder), `-v` lines, finder-only output, mutants 11/12 with `stern` and
+`dumer` on BB_90_8_10. *Evidence.* `optimization/experiments/GH-146/REPORT.md`.
+
 Fix round 1 (S0a): the S0 spec's literal mutants 3 ("orbit seeds without forbidding earlier orbits") and 4 ("stop
 rule without checking the other half's lower bound") are equivalent mutants as built: the first only drops a
 restriction, so every level verdict stays exact; the second skips a check that the lockstep pick order (lowest

NOTICE

@@ -221,3 +221,7 @@ DistQLDPC's optional CC engine (GH-133).
 
 Renamed 2026-10-22 (PI decision; same matrices): BB_756_16_ge30, BB_864_4_ge30, BB_1080_4_ge30
 (were ..._ge28): lower bound 30 from DistQLDPC's optional CC engine with the GH-138 overlap rule.
+
+Renamed 2026-10-23 (PI decision; same matrices, lower bounds unchanged): upper bounds added from
+nontrivial logical operators found by DistQLDPC's GH-146 finder and independently verified
+(optimization/experiments/GH-146/witnesses/): BB_1080_4_30to48 (was BB_1080_4_ge30), BB_756_16_30to34 (was BB_756_16_ge30), BB_864_4_30to40 (was BB_864_4_ge30), TN_288_2_9to24 (was TN_288_2_ge9), TN_324_4_9to25 (was TN_324_4_ge9), TN_360_4_17to24 (was TN_360_4_ge17), TN_396_4_17to26 (was TN_396_4_ge17), TN_432_8_9to29 (was TN_432_8_ge9), TN_468_4_17to29 (was TN_468_4_ge17), TN_496_2_17to30 (was TN_496_2_ge17), TN_504_2_17to34 (was TN_504_2_ge17), TN_540_4_9to34 (was TN_540_4_ge9), TN_576_2_9to37 (was TN_576_2_ge9), TN_612_2_17to40 (was TN_612_2_ge17), TN_648_10_9to32 (was TN_648_10_9to52), TN_648_14_9to28 (was TN_648_14_ge9), TN_684_2_9to29 (was TN_684_2_ge9).