Research log

Index of moonshot attempts (novel-math research track). Each entry links to attempts/<name>/result.md. Failures are first-class outputs — document what was tried and why it didn't work.

Format

- YYYY-MM-DD — <name> — <status: success | partial | failed> —
  <one-line summary>. [details](attempts/<name>/result.md)

Entries

• 2026-09-13 — bb-growing-fom — success — Weight-six separable BB family with exact attained seed distance, 3^s ≤ 2s d_s, and kernel-proved strictly increasing, unbounded actual kd²/n on s=16·4^t. Packaged as StabilizerCodeWithDistance; full validation and standard-axiom audit passed. The closed formula d_s=3^s-1 remains conjectural. details

• 2026-07-22 — a20-v7-completeness (A20) — success — The Y4 boundary-census completeness gap is closed analytically: band 18 is definitively 1,186 classes (the unterminated SAT census had already found every one), and the [[288,8,20]] tower's DangerousFloorNZ 20 is discharged outright — 5 of the 6 assembly hypotheses (A20 §7) now done, only the lift-aware seam floor remains for certified d = 20. Levers measured dead first: the A22-P1 analog (min-|f| over the 16 kernel translates has a band-18 tail to 23, min site-support to 8/8 — no small-f sweep) and A23's flat min-side strata (min side reaches 9 on 500 classes ⟹ ~6.2·10⁹ flat elements, 31× A23's scale; the gating fact ker A⋆ = ker B⋆ = ker ∂₂ itself VERIFIED at Y4, kernel δ₄-pure at exactly 6·active-sites). What closed it: two new finite facts on the a20 fibering — excess parity (site weight ≡ ε mod 2 ⟹ per-site excess even; the 54K-cell B₀ = 18 stratum is excess-0-only) and argmin = 3^cost (⟹ min-cost information sets of the [16,8] GF(64) graph code (w, C₆₄w) via matroid greedy bound each cell at 3^{cost(I)}), plus halved-budget two-sided passes for balanced cells (min-side excess ≤ 2⌊E/4⌋). Engine (a20_v7_completeness.py, A22-V7 grade — every ingredient a finite algebraic fact): 74,528 survivor cells, 674M candidates, 18 min single-core; 118,932 light vectors = Σ orbit sizes EXACTLY (every translate found exactly once); closed bands ≤ 16 match the SAT census exactly (469); zero new band-18 classes, so the existing 1,655 UNSAT floors already cover the definitive list (a20_v7_new_floors.py vacuous). Lean port assessed feasible-with-engineering (A22-L-style + ÷24 symmetry quotient). details

• 2026-07-22 — a23-analytic-seam-floor (A23, session 1) — partial — Every covering-style certificate for SeamCosetFloor 16 of f2a6f17e:y is refuted with exact numerics, but the whole Prop collapses to one tight two-trinomial inequality. Negative side (all on the single G-orbit rep; ker ∂₂ = 15 translates of one weight-40 element, stab ⟨(1,3)⟩): complete w8-cycle census (exactly 75 = one orbit of logicals, no w8 boundaries) ⟹ exact max disjoint odd-pairing dual-detector packing = 10; no S-orbit triple; fractional packing LP = 13.70→13.84 under column generation (< 15 needed) — a genuine binary-clutter covering gap; region-confined parity floors cap at 12 (confinement kills dual cycles; bands < 8 rows carry none). Also: the spawn brief's "|seamC ζ| likely small" premise is impossible (|seamC| ≥ 16 whenever the floor holds; actual 18/20), so the LightClassification triangle-reduction cannot close. Positive side: ker(A⋆) = ker(B⋆) = ker ∂₂ (one F₁₆ block) ⟹ the seam cosets are exactly the graph code {(β + A⋆f, B⋆f) : β ∈ ker∂₂∖0} (seam offset satisfies the transfer relation t′ = 0 exactly), and by orbit collapse SeamCosetFloor 16 ⟺ ∀f: |A⋆f + e₀| + |B⋆f| ≥ 16 (e₀ = the explicit weight-40 block idempotent; σ-symmetrizable to two weight-3 trinomials). Lean bridge = 4 decide facts + seamC additivity

  • kernel cert. Strata b ≤ 6 of the inequality verified exactly (13.7M elements, 0 violations; b ≤ 5 has slack ≥ 4; b = 6 is tight with exactly 15 pairs at (10,6) = the SAT-witness G-orbit and nothing else); b = 7 + σ-side pending — would give a no-SAT verification. 8/8-split makes the parity lemma unnecessary. details

• 2026-07-22 — a20-seam-wall-and-fibering (A20) — partial — The seam floor is FALSE as stated — the wall value appears in the seam — and the A22 fibering port validates on Y4 but its completeness sweep meets a measured obstruction. (1) Seam: the 15 seam classes of the Y-tower collapse to 2 G-orbits (12+3, both δ₂-injective); probe SAT@18 on class 0x1 — the seam-coset minimum sits at 18 = 2d₁ − 2, the wall value, at rung 2 of the tower whose rung 1 attained the wall in d. Not a d = 20 refutation (floor is sufficient-not-necessary); replaced by the lift-aware seam floor (a20_safe_m_floors.py): coset-element census ≤ 19 + per-element fiber-pinned lift queries (elements are auto-nontrivial by δ₂-injectivity — no signature clause), running. (2) Fibering (a20_fibering.py): z = x², G ≅ Z₉ fiber × Z₂×Z₄ local base; CRT F₂×GF(4)×GF(64); 512-triple bijection + exact site-weight formula verified; ε and δ₆₄ components invertible (augmentation = local-ring criterion), kernel localizes to the GF(4) component; the frame validates on ALL 1,655 census classes (0 mismatches). V7 obstruction, measured: budget-19/8-sites kills A22's active-site lever (min site cost 1; 820 all-site classes), and the invertible GF(64) component removes the overdetermination lever; W_min pre-filter cuts 16.7M → 1.19M outer survivors but the inner GF(64)⁸ enumeration lacks a finite reduction so far — the moonshot-grade residue. SAT census stopped at user request (checkpoint intact, resumable); band-18 exhaustiveness remains open via census-resume or the V7 residue. details

• 2026-07-22 — a21-analytic-base-floor (A21 session 1) — partial — Complete analytic proof (math level) of LogicalFloor 8 for the [[150,8,8]] f2a6f17e base — the ≥ 8 half of d(base) = 8, previously SAT-only (CaDiCaL UNSAT@7), now a solver-free split map with every residue a fixed instance table. Ingredients found: (i) the code is a twisted self-pairing — an involutive automorphism ψ with B = xy⁶·ψ(A) yields a chain symmetry Φ swapping the split (a,b)→(b,a), halving the work; (ii) a y-span lemma (rows of A⋆T under A = 1+x+y satisfy a 1-step recurrence; block analysis vs B's row-span 6/min-gap 2) kills (1,1),(1,3),(1,5) uniformly with no censuses; (iii) μ(Ann) = 40 exactly (single shared F₁₆ orbit; all 15 nonzero annihilator elements are translates of the trace idempotent, weight 5·8); (iv) the (3,3) crux dies by transversality (D2 forces B+t to hit each A-copy once) + an overlap lemma (mult-≥3 values of d(A⊖B) = dA∪dB exactly) localizing both sides to {±A+t}×{±B+s}, with the 3 non-generator combos killed by row-gap invariants of A⊕B/B⊖A/A⊖B — the only weight-6 cycles are the 75 generator columns; (v) (2,2)/(2,4) by D2-pigeonholes + word-metric spread bounds (Lemma W: wt(P⋆T) = 3|T|−2E+4N for Sidon P). Numeric falsify-first census independently re-derives UNSAT@7. NOTE: the code is OUTSIDE the A16 class ((iii) fails: A = 1+x+y is monomial in both axes), so this is also the first floor proof for a doubly-monomial neighbor-family instance, and the first past-2w depth rung (T5) executed anywhere. Lean layer STARTED same session: BaseFloor.lean on claude/a21-logical-floor builds green — logicalFloor_8 : coverData.LogicalFloor 8 compiles with the weights-≤5 layer fully machine-verified (6.75M-tuple check_four, largest SmallCycleData sweep yet) and a single sorry left (weight6_cycle_is_boundary, the §3.7 split map; two-stage discharge plan written). details

• 2026-07-22 — a21-analytic-base-floor (A21 session 2) — success (engineering grade) — logicalFloor_8 : coverData.LogicalFloor 8 is a THEOREM, sorry-free and axiom-clean (standard three + named native_decide obligations; QECLean claude/a21-logical-floor commit 1a98a97). The weight-6 sorry closed by the stage-A translation-reduced coset route: a cycle's u_R over a normalized u_L lies in the 16-element coset wAB⋆u_L + Ann(A) (Ann(A) = Ann(B), dim 4, certified by Gaussian pivot certificates), so five native_decide sweeps over 16-candidate classes (5,625 × 16 for the (3,3) crux, 2.5 min) kill splits (1,5)/(2,4)/(5,1)/(4,2)/one-sided and classify weight-3 completions into the generator columns ∂₂δ_t. One of the three hypotheses of cover300_pauli_distance_eq_16_of_classification is now discharged; the CaDiCaL UNSAT@7 certificate is replaced end-to-end. New certificate form forced by a small negative discovery: no-row-op pivot orders (KernelCert shape) provably do NOT exist for full-torus conv systems — every 4-cell free seed's peel closure stalls at ≤ 10/75 cells (the A17 "orders always exist" experience is a window-with-boundary artifact); the fix is the row-combination certificate (store the RREF combination mask per pivot; check its 3-term adjoint row; peel by one sum_eq_single) — simpler in Lean than the no-row-op peel and universally applicable. Stage B (analytic §3 flip of the sweep leaves) remains optional and leaf-local; Distance.lean wiring deferred to main-session review. details

• 2026-07-22 — a22-light-classification-fibering (A22 session 1) — partial — The 9.6 h SAT enumeration behind LightClassification ([[150,8,8]] f2a6f17e, 113 light-boundary classes) is re-derived in ~2 min of exact GF(16) linear algebra, via a new z = y³ CRT fibering: F₂[Z₅×Z₁₅] ≅ F₂[Z₁₅] × GF(16)[Z₁₅] with an exact 32-entry site-local weight table, the ε-side a FREE coordinate (Ā invertible downstairs), and the δ-side a single-character-check code with transfer τ⋆Ã = B̃. Weight ≤ 14 rigorously forces ≤ 7 active sites; sweeping all 16,384 site-subsets (Gaussian kernels) + finite ε-flip accounting reproduces the 113 classes EXACTLY. Structure corollaries: every light δ-part is Ãm with |supp m| ≤ 3; the near-kernel stratum = small configs + one N-fiber ε-flip (coset minima 31–33 explained); minimum weight d = 6 forced on Ā-triangle translates via a μ₃-coset trichotomy; Φ acts on δ-data as ζ^{2i}·Frob² block swap (94 α-classes → 55 families). Lean architecture assessed feasible: ~6·10⁵ tiny cost checks + 1.6·10⁴ pivot certificates (KernelCert pattern), no SAT, no 2⁷⁵ statement. Status partial only because the Lean layer is unstarted (session 2). details

• 2026-07-22 — bravyi360-m12-certified (A19 §8) — success — Certified d ≥ 12 for Bravyi's [[360,12,≤24]] via the A17/A20 (M)-kernel pipeline retargeted at the y-deck: exhaustive census of BY's light X-stabilizers (7 classes ≤ w11: one hexagon, six w10, no w8 — the Prop-10 gap's third instance), fiber-pinned UNSAT floors (all 7, 0.4 s), b = 0 stratum analytic via A16. With the τ-lift upper bound: 12 ≤ d ≤ 24, both ends certified/verified — the strongest bounds this code has had by any method. Route is y-deck-only (BX not a dependency). Compute: 227 s census + 0.4 s floors once the machinery existed. details

• 2026-07-22 — a20-dangerous-floor-certified (A20) — success — The (M)@20 dangerous floor of the [[288,8,20]] tower is certified over the full census, and the flagged analytic-tail risk is retired. Census (a20_m_census.py, XOR-native, orbit-blocking, resumable): bands 2–16 CLOSED — 469 classes (1×w6 hexagon, 6×w10, 33×w12, 54×w14, 375×w16), no weight-8 stabilizers (gross Prop-10's gap echoed at Y4) and µ(Y4) = 6 certified; band 18 at 1,186+ classes, enumeration ongoing (orbit-blocking clause load is the bottleneck — census redesign via canonical-form constraints is the porting lesson for A19's (M)@24). Floors (a20_m_floors.py): per-class fiber-pinned UNSAT — cover-cycle XORs + p(v) = b pinned by 144 fiber XORs + signature-OR nontriviality + cardinality on off-support fibers only; slice identity ⇒ |v| ≥ 20 over b. All 1,655 censused classes certified, 0 SAT hits, ~17 s of solver time — the hexagon's m ≥ 7 (deepest rung in the program) in 9 s. IBM's MILP d = 20 independently corroborated on the dangerous side. DangerousFloorNZ 20 awaits only the band-18 UNSAT close-out; the sole remaining rung-2 obligation is SeamCosetFloor 20. details

• 2026-07-20 — a20-ibm288-tower-opened (A20, new) — success — IBM's [[288,8,20]] is a gross-shaped all-(R) tower and the campaign to certify d = 20 is open. Instance study (scripts/a20_ibm288_tower.py, kernel-level): k = 8 deck-born at (18,2) — all decks jump, (R) fails there, A12-consistent — then (R) HOLDS on both y-rungs (18,2)→(18,4)→(18,8) with explicit Bezout witnesses saved (data/a20/bezout_y_18x{4,8}.json; 1+y^{m/2} ∈ (A,B) solved by F₂ linear algebra) — so the classical BBDoubling template applies at both rungs, DeckTrivialOnH1 dischargeable via deckTrivial_of_bezout, and bocksteinVanishes_of_orderFourLift applies (ZMod Frattini lifts). d₀ = 6 EXACT (0.5 s) and d₁ = 10 EXACT (180 s; weight-10 witness

  • UNSAT@9 on all 25 orbit reps) — so rung 1 ATTAINS THE DEFICIT WALL, 10 = 2·6 − 2, the first measured instance ever at exactly 2d − 2 (same day the [[288,12,18]] candidate was refuted; A17 §8b supersession logged), and rung 2 doubles perfectly, 20 = 2·10, with the τ-lift of the d₁ witness verified as a weight-20 nontrivial logical of Y8 (scripts/a20_tau_lift.py) — d(Y8) ≤ 20 constructive, independent of IBM's solver. Rung-2 template ledger: LogicalFloor 10 DONE (UNSAT@9), DeckTrivialOnH1 DONE (Bezout), τ-tightness DONE (witness); open: (M)@20 census over Y4 (weight-19 classification) and SeamCosetFloor 20 (first live (R)-tower consumer of the A13 transport machinery; odd part Z₉ ⇒ F₂/F₄/F₆₄ components). One tower carrying both the maximal-deficit cell and a perfect doubling: the deficit mechanism is per-rung, not per-code. Pathfinder for A19 full-24 at half scale. details

• 2026-07-20 — a19-wall-refutation-and-catalog-survey (A19 follow-through) — success — The [[288,12,18]] wall-attainment candidate is REFUTED and the deck-birth design principle is confirmed catalog-wide. (1) The Bravyi [[288,12,18]] (6,12) base: floor@9 and floor@11 all-UNSAT over all 155 orbit reps (191 s / 21.7 min, 8 workers) certify d(base) ≥ 12 — the A19 §7 prediction "d(base) = 10 ⟹ the cover attains the wall 18 = 2d−2" is dead. Closed same session: floor@13 found nine weight-12 witnesses (4.0 h) — d(base) = 12 EXACT, the cell certified at 18 = 2d − 6, deficit-6 recurring 2-for-2 with bb108-y (docket cells logged, A17 §8b, incl. the BX/BY deficit-4 rungs). The base is [[144,12,12]] — gross parameters, perfect y-double of its bb72 half — so [[288,12,18]] is bb72 doubled twice: perfect rung then deficit-6 rung, the mirror of A20's wall-then-perfect stacking. (2) Catalog-wide recursive deck-birth survey over IBM's supplemental Tables I–III (scripts/a19_deck_survey_catalog.py; 220 rows parsed, 218 k-validated against recomputed F₂ ranks; implementation reproduces all four A19 §7 Bravyi verdicts): every k = 12 class has a unique deck-birth rung (literal presentations) — five of seven born at (6,6)/bb72, two born at the top ([[288,12,16]] class a and Bravyi-360 class V). New taxonomy: top-born (d ∈ {16,22,24,≤30}), deep-born long propagators (the (18,·) family, born (18,2): [[288,8,20]] d = 20 exact, [[288,8,18]], [[288,8,16]]×3), and odd-core all-(R) towers ([[360,8,18]] over (15,3)) — k need not be deck-born when k ≠ 12. Follow-up targets: [[288,12,16]] (second deck-nontrivial-top flagship, A19-playbook candidate at friendlier scale) and [[288,8,20]] (cheapest known d ≥ 20 certification target; bases at n = 144/72). Caveats: greedy first-branch descent; jumps literal pending orbit sweeps; one parse-suspect row (n288/e (16,9): table k = 40 vs computed 36). details

• 2026-07-20 — a13-seamc-delta2-transport (A13 L2 continuation) — success — The seamC↔δ₂ homological transport — A13 L2's sole remaining gap and the paper's main-theorem bridge — is now an axiom-clean Lean theorem (BBBocksteinTransport.lean, branch claude/a13-seamc-delta2-transport): the element fact δ₁δ₂ = 0 (BocksteinElementForm, in convolution language) implies BocksteinVanishes, closing dim (1+σ)H₁ = k̃ − k, E + k = k̃, and dim ker ε_* = k for every XDoubleCoverData. The proof route is simpler than the paper's: no δ₁/H₀/LES exactness — the element form's Bezout witnesses directly correct the sheet-0 lift of seamC ζ into a cover cycle with the same pushforward (exists_cycle_push_eq_seamC), so im δ₂ ⊆ im p_* is chain-level explicit. The element form is discharged from any order-4 deck lift (elementForm_of_orderFourLift; kernel of 𝔽₂[Ĝ] → 𝔽₂[G] computed by the repo's own fiber-sum exactness on a zero-polynomial hat bundle) and unconditionally for every doubled-axis cover ZMod (2n) × ZMod m with deck (n, t), twists included — i.e. for the program's entire free-ℤ₂ BB doubling family (finrank_range_epsH1_eq_of_zmod_double). Remaining from A13: only the D-module structure iso (f.g. 𝔽₂[ε]/(ε²)-module classification). details

• 2026-07-20 — bravyi360-deck-nontrivial-tower (A19) — partial — Bravyi's [[360,12,≤24]] flagship fails deck condition (R) on all three decks (x¹⁵, y³, diagonal) in every monomial presentation — the first natural code outside the doubling template — with k 8→12, dim(1+σ)H₁ = 4 = k̃−k verified for every deck (the A12 quantitative conjecture, ×3), and the doubly-new sector = im τ_* = the A13 D-summand deck-independently. Tower certified: GB (15,3) = [[90,8,8]] exact, BY (30,3) = [[180,8,12]] exact (both rungs k-preserving, both deficit-4), BX (15,6) = [[180,8,≤12]] (floor round in flight); all three bases pass the A16 class certificate ⇒ first certified lower bound d ≥ 6 for the 360-qubit cover, and its weight table is pure transfer-lift arithmetic (24 = 2·12 both decks, 32 = 4·8; d ≤ 24 now constructive). Gap audit: gross Thm-C slice/(M) machinery is (R)-free — (M)@12 over BY (Prop-10 depth, n=180) would certify d ≥ 12; the only genuinely new theory needed for full 24 is safe-sector confinement without (R) (A13 seamC↔δ₂ route, F₁₆ components). details

• 2026-07-07 — class-small-cycle-theorem (A15/A16, goal 2) — success — The A5 goal-2 target statement is an unconditional theorem: every weight-3 BB instance with Sidon disjoint difference sets (D1 ∧ D2), mirrored projections (iii), Ann ≠ 0, and a floor-bearing frame (4∤ℓ, 4∤m) has no nonzero 1-cycle of weight ≤ 5 — d ≥ 6, with every free-Z₂ cover inheriting the floor. Mechanism: a field-generic widened engine for the one-sided floor (the F₄ co-point dichotomy is support-generic; only value-rigidity is F₄-locked); the (1,3) kill via char-2 chirality identities (the weight-3 triangle image IS the Frobenius square B² + c, and (iii) ∧ D1 exclude dA = 2·dB — subsuming the is_frobenius_related gate on the class); the (2,2) kill via exact difference-multiset accounting (atoms → translate-rigidity → a D2 funnel; size-4 via a matching dichotomy whose exceptional torsion families die against D1/D2/counting/ Ann — the pentagonal family by "no vanishing weight-3 sums of 5th roots of unity in char 2"). Two instance-independent fixed censuses (Z₅², Z₁₅²; embedding-complete by torsion factoring) carry the exceptional-family kills. Consequences: the 58-member corpus class

  • 111,840 battery members certified analytically; bb_72/bb_108/ bb_90 subsumed; Z₆×Z₁₄ [[168,12,6]] certified — first instance off the Z₃² odd part; per-instance certificates are uniform O(|G|²) gate-checks (a15_class_certify.py). Write-up of record: experiments/bb_lab/notes/A16_class_theorem_writeup.md; track log A5_goal2_log.md Entries 8–13. Lives in experiments/bb_lab/ (not attempts/).

• 2026-07-07 — bb-literal-lift-criterion (A11, Entry 3) — partial (criterion refuted weight-agnostic; line paused) — The Entry-2b counterexample hunt found its target, and it VERIFIES: first observed dangerous-sector bind. A weight-4×4 pair on Z₅×Z₅ ([[50,2,5]]), y-lift [[100,2,8]]: C-safe holds two-sidedly at enumeration grade (k, tight witness, safe minima 11 ≥ 10 both sides, (R)) yet d(cover) = 8 < 10 = 2d — the weight-8 X-logical pushes to a weight-6 nonzero stabilizer. "C-safe ⟹ doubling" is FALSE weight-agnostic; parity is the load-bearing hypothesis (d(base) = 5 and the safe minima are odd — impossible with |A|, |B| odd), the Entry-2b twice-refined residue is exactly the cell hit (D5 concentration violated), and A17's (M)-robustness conjecture (deficit-wall §9, corpus-class-scoped) becomes non-vacuous and provably scope-critical — not refuted: the odd-weight record stays 2,058/2,058. details

• 2026-07-06 — deficit-wall (A17-P3) — success (theorem + a correction) — A14 §16's deficit-wall OQ answered: the wall value is a theorem, the mechanism is a pushforward, and the "stalls at exactly 2d − 2" premise is retracted as a measurement artifact. Math (notes/A17_deficit_wall.md, machine-validated by a17_deficit_wall_checks.py): (L0) the safe sector is the transfer kernel — im δ₂ = ker τ₁ (LES; span-verified on 9 covers incl. both bb_288 presentations and the Z₁₈×Z₃ re-decomposition), so d_safe = min weight of a base logical whose class dies in the double cover; (L1, parity) with |A|, |B| odd every base and cover 1-cycle has even weight (augmentation ring hom), so d, d̃, d_safe are all even and — since d_safe ≥ 2d ⟺ SF — 2d − 2 is the unique maximal SF-failing value: that is the whole "parity/duality mechanism" §16 asked for; (L2/T1) the collision sets K_z = {g : (1+g)[z] safe} ⊇ Stab₀(z) are subgroups with [G : K_z] ≤ 2^{k/2}, and where the containment is proper the difference classes give d_safe ≤ 2d − 2·overlap — fires on bb90-y (bound 10, tight at the freeze), provably silent on bb108-y (all 54 min-weight logicals have K_z = Stab₀, exhausted by SAT — the hypothesized "2(d−1) base object" does not exist there); (T2, the load-bearing mechanism) under (R) im p₁ = im δ₂ makes the pushforward of any surviving-class cover logical a safe base logical: d_safe ≤ d̃_safe, so a cover failing through its safe sector hands the safe floor its witness at no weight cost, and conversely SF forces the cover's whole safe sector to ≥ 2d (the template re-derived; "SF-true ⟹ doubles", A11's 111/111, reduces to the new (M)-robustness conjecture: the dangerous sector never binds alone). Coupling observed tight everywhere: doublers at 2d = 2d with overlap-free lifts; bb108-y at 14 = 14. The correction: §15/§16's "orbit ceiling 18" and bb_288's "32–34" were first-found SAT witness weights at the query bound, not minima — exact descending ladders put stored bb108-y at d_safe = 14 = 2d − 6 exactly, certified both sides (base UNSAT@12 on all orbit reps; cover d̃_safe = 14 exactly, its UNSAT@12 ≈5 h of CaDiCaL at n = 216 — T2's coupling tight at 14 = 14), every ladder-sampled v1 finalist at ≤ 12 (first witnesses 16), while bb90-y's freeze value = 10 = d exactly (UNSAT@9, certified) — no measured instance attains the wall; correction blocks added to A14 §§15–16. Residue: the code invariant maxSF ∈ {2d} ∪ {even ≤ 2d − 2} (true value per code now measurable by ladders; A17-P1's corpus battery must report S4 weights as "≤"), the (M)-robustness conjecture, and the T1/T2-both-silent corner of the ≤ 2d ceiling. Lean layer LANDED (same session, axiom-clean, zero warnings): Framework/Homological/BBDeficitWall.lean — L1 parity (sum_conv, cycle_support_even, base+cover instantiations with descending hypotheses), L0 as the chain-level iff pull1_mem_boundaries_iff_seamCoset (sibling to ker_pushH1_eq_range_pullH1), T2 as push1_mem_seamCoset_of_deckTrivial + not_seamCosetFloor_of_light_cover_cycle (d_safe ≤ d̃_safe against the repo's own SeamCosetFloor/DeckTrivialOnH1, deliberately routing around A14.1(2)'s dimension count via deck-triviality), and the wall as the even-step upgrades seamCosetFloor_of_even_of_pred / safeFloor_of_even_of_pred. theorem+battery

• 2026-07-04 — safe-floor-screens (A14) — success — A12's OQ4 answered in its own terms: the safe sector is canonical under (R), and a certified necessary-screen battery now decides condition-3 targets. Math (Prop A14.1): under (R) — equivalently the Bezout membership ε ∈ (A,B) — p₂ = 0, the connecting map Δ = δ₂ is injective, im p_* = im Δ = Δ(ann_R(A,B)) of dim k/2 (the extensibility doc's per-instance "half of k" observations are theorems), with closed-form seam-carry representatives (= BBCover.seamC, matched bit-for-bit against SeamTables.lean) and coset minima constant on G-translation orbits (gross: 63 classes → 13 y-orbits = the MIm transport count → 5 full-G orbits); at k̃ = k the deck-Bockstein composite vanishes automatically (OQ2's remaining content lives off the doubling regime). Screens (necessity-by-construction — every rejection exhibits an explicit light coset element): S0 raw seams → S1/S1+ descent → S2 CRT-block kills → S4 per-orbit-rep coset SAT. On the 638-row T1 corpus with exact ground truth recomputed for every row (A9-profile cross-validation 0/152 mismatches): the cheap tiers reject 86% of the 506 SF-failures at zero false rejections, and every k-preserving short is SF-false — on the direct-sweep frames the safe floor alone separates doubles from shorts (111/111). S4 with the 5-orbit transport: hit3/4/6-y SeamCosetFloor 12 all SAT-certified (~25 s each, floors exactly tight — all three engine targets viable, none overlap-rescued); gross's Lean-proven floor independently SAT-cross-checked (24 s); bb_288 SF-refuted on both axes (x: raw seam weight 24, turning the previously SAT-derived d_safe ≤ 24 into a polynomial identity; y: witness weight 34, provably beyond the cheap tiers). Scripts a14_{seam_formula_check,safe_floor_screens,phase2_screens,s4_ladder}.py; columns wired into the A9 profiler (a14_columns). Residual (queued): the Phase-3 Lean package for A14.1(1)–(2), sharing the A13-L2b exactness chase. Tower follow-up (§13): every proven rung-1 double, re-doubled on the same axis, freezes at its rung-1 distance — all five rung-2 safe floors refuted by S0 alone (raw seam = d(rung-1) exactly), SAT confirms d_X ≤ d(rung-1) (pair72-x full ladder d_X = 8; both n = 288 towers SAT@12). This is the toric same-axis bottleneck, certified on the gross lineage; distance > 12 must come from a larger-d base or a mixed (tour-de-gross) lift, not from towers. d=10-base follow-up (§14): all four bb_90/bb_108 literal-lift axes fail in three distinct modes — freeze-pattern light classes (bb90 both axes; bb90-x is the first S0-pass/S1+-reject), a first in-the-wild condition-2 death (bb108-x: 1+x⁹ ∉ (A,B)), and bb108-y's deficit-2 near miss whose overlap rescue is refuted by an explicit weight-18 cover logical (3 s SAT). No d = 20 doubles from stored corpus presentations; the hunt moves to presentation orbits (bb108-y first), mixed lifts, and wider d ≥ 7 base enumeration. plan+results

• 2026-07-02 — bb-literal-lift-criterion (A11, Entry 1) — success — A checkable doubling criterion emerges, and the A8 audit FLIPS the hit2/hit5 negatives. Literal-lift doubling is presentation-sensitive within a (code, axis): the anchorable A8-presentations of ALL six engine-frame classes have d = 12 covers on BOTH axes (7 fresh SAT ladders, all 12), while their stored forms stay at 6/8 — A9's "hit2/ hit5 do not double" was a presentation artifact. The discriminator is template condition 3's safe half: doubling ⟺ safe-class coset minima ≥ 2d on every engine-frame cell tested (base-side SAT probe, no cover SAT; 4/4 prospective predictions), and safe-floor ⟹ doubling with 0/465 violations on the full A9 hunt stream. Certificates (R0-sq…R2, linchpin) are universally satisfied — never discriminating (one-line mechanism: 1+δ ∈ (A,B) forces σ_* = id). A8's squaring identity alone is refuted as sufficient (62 small-frame shorts); its full package stands at 7/7 + gross + Z₆×Z₁₄, zero counterexamples. Dead end (first-class): the reachable-coset repair of the 41 overlap-rescue rows fails 0/41 — the necessity gap is genuine slice mathematics. details

• 2026-07-02 — descent-twist-screen (A10) — success (screens halted by design) — The doubling-existence question ANSWERED: universal claim FALSE, marquee bases RESCUED. Full descent-space (256-cover) twist screens over the anchorable Z₆×Z₆ frame: hit2 rescued by an x-class single-bit twist and hit5 by the mixed extension class at zero twist (both DRAT-certified d = 12 = 2d), so all five gross siblings carry exact [[144,12,12]] covers — while 13 small-frame bases (Z₃×Z₃/Z₃×Z₄/Z₃×Z₅) have their ENTIRE descent space fail (3328 witness rows, numpy-re-verified, certificates committed — A14's must-catch corpus). Lemma L1: descent covers are presentation-invariant (screens are code-level exhaustive); constructive corollary — twist rescues ≡ presentation moves. R9 keystone: 14101/14101 k-preserving fail witnesses break in the SAFE sector (mechanism later proven as A17-P3's transfer-kernel/pushforward theorems). Grids deliberately halted at the efficiency crossover (R11). details

• 2026-07-02 — deck-tower-descent (A13) — success — Deck-trivial ⟺ k constant along ℤ_{2^r} doubling towers (A12 OQ1), answered YES. For a free ℤ_{2^r} BB cover, σ_* = id on H₁(top) forces k(top) = k(base) (r ≥ 2; r = 1 is A12). The hard direction is a completed elementary proof: A12 on the top ℤ₂-step gives the entry ε^{N/2} ∈ (A,B), then a descent — apply deck-triviality to the canonical cycle ε^{N-t}(f,g); the boundary coefficient satisfies ε^t z = 0, so ε-freeness divides it (z = ε^{N-t}u), yielding ε ∈ (A,B) + ε^{N-t}S — plus a ring-algebra tail-elimination. Simpler than the planned Bockstein-SS / obstruction-class route (none needed). Lean payoff (public-side, axiom-clean): QEC/Stabilizer/Framework/Homological/BBDeckTower.lean — eps_mem_of_deckTrivial (the ⟹), descent, boost/iterate over an abstract char-2 ring with the EpsFree/DeckTrivial predicates; pairs with the existing BB.deckTrivial_of_bezout (the ⟸) for the full ring iff. Builds 1.4 s; axioms = standard three, no sorry/native_decide. Screens (refutation-first, all clean): a13_deck_tower_block_sweep.py (endpoint + mechanism + intermediate identities, exhaustive to deck order 8) and a13_gross_ladder.py (gross x-tower k≡12 + full deck-triviality to [[576,12,·]] from the level-free witness (1+x²)B²=1+x⁶; genuine Z₁₂×Z₃ cover pairs). Residual (paper-level, plan item L1): the H₁ ↔ DeckTrivial / 𝔽₂[G]-free ↔ EpsFree bridges. The family paper's k-row is now a theorem (T1–T3 + A13); growing distance still lives in the safe floor (condition 3), untouched here. plan+resolution

• 2026-07-03 — bockstein-equality (A13) — success (core) — A12's OQ2 sharpest element-level form is now a machine-checked Lean theorem, and the full failure-danger zone is swept exhaustively clean. Math: the transfer SES is the mod-ε̂² reduction of the 4-fold cover — the analogue of the integral lift behind classical β² = 0 — and freeness over F₂[ℤ/4] (Ann(ε̂) = (ε̂³)) kills the composite at the element level (W = A·ε⁻¹(Bz) + B·ε⁻¹(Az) = 0 on the nose), for arbitrary order-2 decks incl. twisted. A toy 3-term free-D self-dual complex with δ₁δ₂ ≠ 0 shows the originally scoped structural route (LES + Frobenius self-duality) is provably insufficient — liftability is the content. Lean (W3, axiom-clean): Framework/Homological/BocksteinLift.lean — bockstein_element_form (abstract capstone: element form from char 2 + Ann(ε)=(ε³)) and bockstein_element_form_deck (unconditional on the ℤ/4 chain block); only propext/Classical.choice/Quot.sound. Sweeps (W1, exhaustive): every (A,B) pair over F₂[Z₁₆], F₂[Z₈×Z₂], F₂[Z₄×Z₄], F₄[Z₈], F₄[Z₄×Z₂], F₈[Z₂], F₈[Z₄], F₈[Z₂²] (all decks; ≈ 2³² weighted pairs per |P|=16 block; hundreds of millions of live pairs) has E = 2g, maxdef = 0 — closing OQ2's own "cheapest falsification path." W0 red-team agents were cut off by a session limit (Lean kernel now the referee). L2 progress (commit b7ee838, BBEpsFree.lean, axiom-clean): the ring hypothesis shared by OQ2 (BocksteinLift) and OQ1 (BBDeckTower's EpsFree, on-branch after rebasing onto merged PR #54) has its reusable core proven — epsFree_quotXpow (chain ring R[X]/(X^N)) + epsFree_of_free (transfer across a free module) + hann_of_epsFree (bridge). General L2a now reduces to one wildcard: Module.Free 𝔽₂[⟨σ⟩] 𝔽₂[G] (coset basis, no mathlib support). L2b core (commit 67b947e, BBBocksteinRank.lean, axiom-clean): the transfer-inequality heart — finrank_ker_comp_le + finrank_sub_le_finrank_range_comp (ker p = range τ, ε = τ∘p ⟹ dim Hc − dim Hb ≤ dim (range ε)), i.e. E ≥ k̃−k once instantiated on homology. Phase-1 instantiation landed (2026-07-04, axiom-clean): the inequality E ≥ k̃ − k is now a Lean theorem for every XDoubleCoverData — BBCover.lean gained push0_surjective + exists_pull_eq_add_boundary (the chain-level diagram chase), and the new BBTransferH1.lean induces pushH1/pullH1 on H₁ via Submodule.mapQ, proves the exactness ker p_* = range τ_*, identifies epsH1 = τ_*∘p_* with (1+σ)_* pointwise, and concludes finrank_H1_sub_le_finrank_range_epsH1 : dim H₁(cover) − dim H₁(base) ≤ dim (1+σ)H₁(cover) — A12 part 2, previously paper-only, now kernel-checked. The L2a wildcard is also CLOSED (2026-07-04, BBEpsFreeGroupAlgebra.lean, axiom-clean): the group algebra k[G] is free directly over the chain ring k[X]/(X^N) via X ↦ x^σ − 1 (coset-transversal basis: spanning by x^g = (X+1)^j·C c • x^{t i}, independence by modByMonic representatives + the invertible substitution ∘(X±1) + orbit coefficient extraction), giving epsFree_one_add_single_of_addOrderOf : EpsFree (1 + x^σ) (2^r) for ANY abelian G (finite or not) and any char-2 base — the shared ring hypothesis of BOTH deck lines (OQ1 eps_mem_of_deckTrivial, OQ2 bockstein_element_form via hann_of_epsFree) is now unconditional for group algebras. The L2 linear-algebra wiring is also COMPLETE (2026-07-04, axiom-clean): BBBocksteinRank gained the exact defect identity E + dim Hb + dim(range p ⊓ ker τ) = dim Hc + dim(ker τ) and the tightness criterion ker τ ≤ range p → E = dim Hc − dim Hb; BBTransferH1 instantiates them as BocksteinVanishes D (ker τ_* ≤ range p_* = δ₁∘δ₂=0), finrank_range_epsH1_eq (E = k̃−k under BocksteinVanishes — the headline deck_finrank_eq), finrank_ker_epsH1_eq (dim ker ε_* = k), and epsH1_epsH1_apply (ε_*²=0, unconditional). On the ring side, BBEpsFreeGroupAlgebra §7 bockstein_element_form_group_algebra composes L2a into L1 to give the element form δ₁δ₂=0 unconditionally in every order-4 deck group algebra k[G]⧸(ε²). The conv↔group-algebra bridge is also landed (BBConvRing.lean, axiom-clean): convEquiv + convEquiv_mul (conv = the 𝔽₂[G] product) + the deck-operator identifications, so L2a/element-form now speak about the repo's actual conv/deck action. The SOLE remaining gap is the homological transport identifying the element fact with BocksteinVanishes — the seamC↔connecting-map δ₂ step (seamC_mem_cycles is already δ₂ at chain level) reading cycles/boundaries/H₁ as convEquiv-modules — the paper's main theorem, genuinely open (the toy self-dual free-D complex has δ₁δ₂≠0, so it is not automatic). Payoff once closed: H₁(cover) ≅ D^{k̃−k} ⊕ F₂^{2k−k̃} (rank data all in hand; needs the 𝔽₂[ε]/(ε²)-module classification for the iso), with Theorem A12 as its a = 0 slice. result · plan · L2 plan

• 2026-07-02 — bb-pair72-packaging (S3.9) — success — pair72StabilizerCodeWithDistance : StabilizerCodeWithDistance 72 4 8 (Codes/BivariateBicycle/Z3Z6/StabilizerCode.lean): the second doubling instance packaged as a first-class code object, mirroring the gross Phase-5 packaging at pair72 scale (trimmed 68-generator list, decoder-certified independence, 4 logical qubits, distance transport). Axiom-clean (standard three + native_decide oracles, no sorry). Data generator with 15-check ALL-PASS gate: experiments/bb_lab/scripts/gen_pair72_packaging_data.py. plan

• 2026-07-02 — deck-homotopy-R-characterization (A12) — success — The doubling template's condition 2 (homotopy R) is solved: (R) ⟺ k(cover) = k(base) ⟺ 1+x^ℓ ∈ (A,B) for every free ℤ₂ BB cover (transfer-LES inequality dim (1+σ)H₁ ≥ k̃−k, plus the constructive Koszul/Bezout converse). (R) is not automatic: explicit weight-3 counterexamples exist (dead-character blocks), the strict IBM monomial shape fails too, and among ~1.04M weight-3 cover pairs swept 11,307 violate (R) — the majority (9,612) via subtle non-dead-block mechanisms. Every historically checked cover (157/157: gross both directions, pair72, Z₆×Z₁₄ both directions, all 152 A9 doubles) is k-preserving, where (R) is forced — the observed universality dissolved. Resolved in passing: the F₂-additive certificate form is complete (semantic (R) ⟺ certificate solvable), and the im p_* ⊆ im Δ linchpin is an iff. Lean payoff: deckTrivial_of_bezout in BBDoubling.lean (module-map homotopy from any Bezout witness; both instance identities are its P = 0 case); pair72's (R) leg retrofitted to a kernel-decide 36-point identity. Open remainder: the quantitative dim (1+σ)H₁ = k̃−k (⟺ vanishing of the deck-Bockstein composite δ₁∘δ₂), exact on every instance and on ~10⁶ exhaustively swept local blocks. details

• 2026-07-02 — bb-doubling-layer-second-instance — success — The free-ℤ₂ doubling template is a parametric Lean layer, and the [[36,4,4]] → [[72,4,8]] pair is proven through it (chain+Pauli d = 8 = 2·d(base), gross axiom bar; packaging: see the S3.9 entry above). The A9 target screen found 152 direct-sweep doubling pairs and corrected the Z₆×Z₆ census: gross has five anchorable siblings, three with exact [[144,12,12]] y-covers — in-frame engine-necessary follow-on targets. details

• 2026-06-12 — gross-bb-analytic-bound — partial — d(gross [[144,12,12]]) ≥ 6 fully analytic (3× the published Lin–Pryadko floor of 2; goal 3 of the Phase-A program), via the small-cycle theorem (d_base ≥ 6 by hand) + the h=2 cover transfer with the dangerous-sector factor-2 lemma (M) proven unconditionally. The adversarial re-review passed (Entry 15: all links HOLD under an independent 49-check re-implementation + hand re-derivation of every prose argument) — the theorem is write-up grade. Goals 1 (d = 12) and 2 (BB-class bound) remain open. Lives in experiments/bb_lab/ (not attempts/): handoff, A3 log entries 11–15.

• 2026-06-12 — gross-bb-analytic-bound (goal 1 closed) — success — d(gross [[144,12,12]]) = 12: the last statement (M-im) is proven by the confined-floor program (A3 Entries 22–26): hand engine lemmas (kill-multiset supports, T-classifiers from ψ₂² = ψ₃ψ₄ and ψ₄ = ψ₁ψ₃, slope level-sets, the ρ²= 0 confinement with c₁ = c₂ = 0 derived via column transforms) + finite residues (spine C-tables, 118 one-line ρ-link kills), double-cross-checked by the two independent machine closures. The adversarial skeptic pass over Entries 16–26 passed (Entry 27: all eight links HOLD under an independent 75-check re-implementation + hand re-derivation; two sharpenings found, off₀ = off₂ = 0 identically and a one-line c₂ = 0). Epistemic grade per the review: verified-finite with a fully hand-proven analytic spine — the Entry-24 C-table evaluations and the completeness of the Entry-25 achiever lists remain machine-certified; paying that debt is write-up organization (compressed-table walks), not new mathematics. Owed: the A4-style standalone write-up; goal 2 (BB-class bound) remains open. A3 log entries 16–27.

• 2026-06-12 — gross-bb-analytic-bound (write-up debt paid) — success — d(gross [[144,12,12]]) = 12, fully analytic (A4 Part II, Theorem D): both Entry-27 residues discharged by hand. New structure that made the compression work: m′² = ω²m (only two slot labelings up to scale), the confined comps as full affine lines, the Γ₄ tie V₄L = ωV₄R + w₄, the pair-ratio lemma for fibre degeneration, and the hyperbolic-quadruple form of the slope lemma (no three points of uv = c ∪ {0} collinear). The ~6k-row wt-24 closure collapses to one standard form S(a,b) walked in 33 buckets (all ≥ 6); the achiever-list completeness follows from the achiever-structure lemma (parity-locked per-(V₀,γ) block minima ⟹ achievers = argmin products over sum-10 loci) + rule-derived per-cell locus tables (118 achievers, each killed by a one-convolution ρ-link check). Certifier a3_a4ext_recheck.py all-PASS. Owed: the Part-II skeptic pass; goal 2 remains open (the slot frame is instance-generic). A3 log entry 28.

• 2026-06-12 — gross-bb-analytic-bound (goal 1 update) — partial — d(gross) = 12 now holds at the verified-finite level, doubly machine-verified by two independent routes: the value-grammar completion sweep (Entry 20: CRT value dictionary + affine-graph completions, no coset element of weight ≤ 11 in any nonzero Smith class) and the light-cycle flux census (Entry 21: all 990 weight-8 and 13248 weight-10 non-boundary cycles have nonzero seam flux). The last open statement (M-im) is reduced to three bounded hand obligations (Entry 22: the confined ρ-floor already closes two of the five orbits outright; the rest reduce to a weight-exactly-10 equality analysis). All other links — (M), (R) ker δ = im Δ via the B²-homotopy, the no-double-wrap flux characterization, the inversion duality — are fully analytic. Support-only COST floors (Entry 19) and route-B hand classification at weight 10 (368 orbits, Entry 21) are documented dead ends. A3 log entries 16–22.

• 2026-05-27 — bb_distance_conjecture_family_d_v3_h2_minwt_formula — partial — Pinned down the (4/9)|G| empirical pattern from session 1 as a rigorous structural identity for weight-3 BB codes: when there exist linearly- independent Z_3-homomorphisms φ_A, φ_B: G → Z_3 with each sending one polynomial's support to {0,1,2} and the other's to a constant, the element 1[φ_A ≠ 2 AND φ_B ≠ 2] is in H_2 with weight (4/9)·|G|. Verified 437/437 corpus instances, 0 violations. Conjectured generalization ((w-1)/w)²·|G| for weight w (untested for w ≥ 4). Implemented as Tier-1 feature bb_lab.h2_minwt_formula with 14 tests. Not a distance bound (per §6m); a positive structural identity. details

• 2026-07-22 — A22 light-boundary completeness (f2a6f17e session 2) — success — lightClassification : LightClassification is a sorry-free Lean theorem (branch claude/a22-light-classification): the 9.6-hour SAT enumeration-completeness verdict behind the [[300,8,16]] dangerous floor is replaced by a CRT fibering (z=y³, w=y⁵: F₂[Z₅×Z₁₅] ≅ F₂[Z₁₅] × GF(16)[Z₁₅]) — per-site 32-entry weight tables, the free ε-coordinate (Ā invertible downstairs), the ≤-7-active-sites bound, and a 16,384-subset GF(16) kernel sweep with row-combination pivot certificates (per A21's closed-torus discovery) + ε-flip accounting, reproducing the 113 classes. 3 standard axioms + 9 native_decide. Discharges the second of the [[300,8,16]] hypotheses. details

• 2026-07-22 — A23 seam-coset floor (f2a6f17e:y session 2) — success — seamCosetFloor_16 : coverData.SeamCosetFloor 16 is a sorry-free Lean theorem (branch claude/a23-seam-transfer): the CryptoMiniSat XOR-native UNSAT@14 certificate (975.8 s + 6.85 GB DRAT) behind the [[300,8,16]] safe floor is replaced by analytic certificates. Route = the A22 CRT-fibering site sweep: δ-type of a 5-point z-fiber is a function of Hamming weight alone, the ε-parity link decouples per site, and the ≤7-active-site systems collapse to 16,084 one-mask inconsistency certs + 300 RREF classification certs (3,000 reps, min cost exactly 16, zero violations). One native_decide checks the whole 32,768-subset table in ~100 s. With A21's logicalFloor_8, the [[300,8,16]] distance theorem now rests on the single hypothesis LightClassification (A22). details

• 2026-08-11 — A33 IBM [[288,8,20]] = 20 via the tower calculus — success — the A32 port to A20's all-(R), same-axis tower closed H5 (the lift-aware seam floor, the theorem's one open hypothesis) two independent ways — a direct coset-BZ seam census at n = 144 (1,680 elements; the second seam orbit's coset is EMPTY at ≤ 18, so the "false" naive floor was false on one orbit only) with 1,680 rungs all passing, and the descent through Y2 reproducing the element list exactly (the trisection collapses to one branch under (R)) — and upgraded every other hypothesis solver-free: d([[288,8,20]]) = 20 END-TO-END at certificate tier, the program's first certified d = 20 for a previously published code (A30 got both [[360,4,20]] doubled covers to the same tier on 2026-08-07 — this is the first for a code someone else published, and the first by the tower calculus), on ~105 s of critical-path compute (vs ~16.5 h of banked SAT partials). Portability scorecard: the calculus's lemmas held verbatim on two twisted (R)-rungs; iterated Z₂ sufficed; sector space is 2^k on both towers; (R) buys exactness + σ* = id + the k/2-dim seam + one-branch descent. Falsify-first: the port's audit caught an empty-window edge in the A32 census helper (+15/+2 vectors; orbit tables and the d = 24 assembly unaffected; fixed at source and re-verified to the digit). details

• 2026-08-10 — A32 tower slice calculus — success — the analytic-pathway moonshot for Bravyi's [[360,12,≤24]] delivered both the landscape contribution and, as a corollary, the certification: a two-level slice/shadow calculus down the tower C→BY→GB ((R)-free and twist-generic; both rungs of this tower are twisted lifts), with an overflow square and a trisection of every d = 24 violation candidate on the second shadow [β]. All obligations moved from n = 180/W = 22 enumeration scale to n = 90 censuses + bounded-overflow lift fibers + top rungs: 49,855 rungs over ~274k fibers, ALL PASS, ~9.4 min wall — ~250× under the coset-BZ baseline — and the flat band-22 β = 0 branch dies by pure parity. d([[360,12,≤24]]) = 24 EXACT at certificate tier, no SAT on the critical path (Bravyi et al. Table 3's "≤" resolved); d(BY) = 12, d(GB) = 8, and the BY stabilizer-census completeness ≤ 20 re-derived solver-free by the same machinery. Independently re-run end-to-end with every count exact. Portable per §7 of the note: the lemmas hold for any free Z₂-deck BB tower; next instances ranked ([[288,8,20]], the A30 doubles as 3-level towers, [[756,16,≤34]]). details

• 2026-08-07 — A30 coset-BZ doubling certificates — success — safe floors recast as coset weights and decided by the A28 two-window enumeration seeded at A29's seam offsets (asymmetric (r, r−1) complete pairs; exact node-count invariants; multi-offset shared walks). All three remaining A17-docket UNKNOWNs certified inside a 15-min/code budget: both Z₁₅×Z₆ [[180,4,10]] codes SF-20 on every axis (37a70e02:x 378 s; 5e50a976:x+y 499 s one pass) — the docket has zero UNKNOWN cells left — plus a 0.6 s second-species cross-check of the CMS-certified Z₂₁×Z₃ 16884e06:y (A29 §5.3's "4 UNKNOWNs" was a stale-row miscount). With base floors certified both sides + weight-10 exactness witnesses + A28 censuses + (R), the full [[360,4,20]] doubling template input sets exist at certificate tier: the program's first d = 10 → 20 doublings and the first codes to clear the 2d − 2 deficit wall. Validation 10/10 against every recorded coset ground truth (A29's ac46bbea/38d3c884 decisions independently reproduced by a second certificate species). Lean packaging (A15 pattern) is the named follow-on. details

• 2026-08-06 — A28 light-stabilizer classification theory — success — the light census (input I2 of the doubling template) is now cheap and independently certified: a Brouwer–Zimmermann census certifier (a28_bz_census.py, two disjoint information windows ⟹ completeness is a counting invariant, not an UNSAT refutation) re-derives the f2a6 113-class census in 4.5 s (SAT lane: 9.6 h; exact agreement) and produces the two Z₁₅×Z₆ [[180,4,10]] docket censuses the SAT lane could not reach (2,203 + 2,371 classes at W = 18, ~11–15 min each). ε-trisection theorem: over G = Z₂×H the census decomposes into doubled H-census ⊔ coset censuses ⊔ bounded lifts (proved + validated 4,574/4,574) — the even-factor recursion complementing A29's odd-fiber ε-recursion residue. van Lint–Wilson shifting as a (CLASS) kill engine: REFUTED by measurement — a BZ-certified-empty cell where the exhaustively-computed best game value is 8 against a needed 15; ρ = B̂/Â survives as the uniform endgame vocabulary (it is A4 §6.3's C-ratios). Depth-10 dichotomy tree quantifies the wall (119 kills / 730 giveups, frontier ×12). Bottom-of-census universality across all five censused codes: one stamp class at |A|+|B|, six D-pair classes at 2(|A|+|B|)−2, tail onset near 2d−2. details

• 2026-08-06 — A29 general fibering engine — success — the A22/A23 fibering is now a code-agnostic library (bb_lab.fibering): exact weight formula in field-free residue coordinates for ANY odd fiber order, automatic fiber enumeration + ε-monomial-link detection, τ-twisted state sweep with consistency-pruned DFS, batched exact ε-costs, seamC offsets per Prop A14.1, verified refutation witnesses. Validated bit-for-bit against pair72/A23/A22 (including the 113-class census). New results: 3 of the A17 docket's 7 UNKNOWN safe-floor cells decided (Z₅×Z₁₅ [[150,8,8]] trio: ac46bbea:y and 38d3c884:x at d_safe = 16 EXACT, 38d3c884:y ≥ 18) and the A8 §4.3 open core CLOSED — the [[168,12,6]] Z₆×Z₁₄ safe floor 12 certified in 10 s, completing the [[336,12,12]] doubling's template inputs without the heterogeneous-dictionary program. Includes an A27 §3.3 P5 erratum (the ≥2-per-site bound needs the ε-link). Named residue: the ε-recursion chapter (Z₂₁×Z₃, Z₁₅×Z₆ floor-20). details