Two Ladders, One Search
The search has two orthogonal axes. A G-rung asks whether a mechanism is real; an R-rung asks whether it shrinks the byte budget enough. Both must pass.
G-ladder — Mechanism
Is this compression mechanism real? Falsified by random-null controls, kill thresholds, and Lean-certified invariants.
R-ladder — Impact
Does it bend the byte budget enough? Each rung targets a concrete GB reduction toward the sub-10 GB capstone.
Historical Rungs
The ladder evolved as we deepened. These rungs were retired or reframed; their impact is recorded on the parent monorepo as a metric, and they are preserved here for methodological continuity.
Eckart-Young invariance: a learned gauge cannot improve rank-r reconstruction error. Mechanism is rotation-only (zero-cost), subsumed by SRHT. The proper byte-counted G₁.0' round-trip ran 2026-04-27 r1–r2; r2 killed: optimization adds < 3% over zero-cost orthogonal random.
The G-rung ladder asks 'is this mechanism real?'. The R-rung ladder asks 'does this bend the byte budget?'. Distinguishing the two prevented confusing dead-mechanism G_1.0 (learned gauge) with live-engineering R1 (RotorQuant), even though they share the rotation primitive.
residual_ratio 0.5 fractionKilled at all layer + expert scopes on OLMoE-1B-7B. Orthogonal-only rotations reshape spectrum by less than 5%; minimum-residual basis still leaves ≥ 88.9% energy outside any rank-(r_eff−1) projection.
Lean theorems
invertible_gauge_preserves_rank_family
PROVED
rank_mul_left_isUnit_det
PROVED
Empirical probe
cross-check/ffn-quant/mode_unfolding_full_spectrum.py
· JSON
vs_orth_advantage 0.05 fractionReclassified after G₁.0' r2: 24/24 vs_orth fail at 0.50 gate; learned gauges beat zero-cost cond=1 orthogonal random by only 2–3%. Reframes Paper 2 narrative as SRHT/structured-rotation rather than learned gauge.
Empirical probe
cross-check/ffn-quant/g1_0_prime_gauge_quant_r2.py
· JSON
r_eff 256 rankKilled on OLMoE: minimum r_eff across layer/expert/hidden Tucker reshape is 262.773, exceeding the 256 budget. Cross-mode reshaping cannot compress past the hidden-dimension barrier without losing > 99.6% energy.
Lean theorems
olmoe_tucker_cross_mode_no_compression
PROVED
olmoe_tucker_layer_no_compression
PROVED
olmoe_tucker_expert_no_compression
PROVED
olmoe_hosvd_joint_no_compression
PROVED
Empirical probe
cross-check/ffn-quant/g2_cross_mode.py
· JSON
r_eff_effective 16 rankModest constructive at q ∈ [16, 32]: 58–80% energy captured. Below q=8 the effective rank floor (≥ 3.89) prevents further compression. Two cross-references from the steady-state Lean library: (1) the q→r_eff floor of 3.89 is structurally aligned with the Class G stable-rank capstone `stableRank_smul_invariant` (`LeanMining/NeuralGeometry/SubspaceOverlap.lean`), giving a floor interpretation; (2) per-layer energy capture does NOT imply depth-composed pass — `DepthCompositionInflation.lean:per_layer_budget_clears_composed` requires per-layer budget ρ_l ≤ (1+τ_NLL)^(1/L) − 1 for an L-layer composed gate. Any G_3 deployment claim across stacks must declare a composed budget.
Lean theorems
effective_weight_gram_eq
PROVED
stableRank_smul_invariant
PROVED
per_layer_budget_clears_composed
PROVED
Empirical probe
cross-check/ffn-quant/routed_effective_weight_probe.py
· JSON
humaneval_inflation_pct 8.0 percentKilled at all stages. Uniform rank-(16,24) killed with strong nulls (r2: 8/12, r3: 9/12 — both below the locked 10/12 threshold). Task-conditional r4 killed: wikitext failed uniformly at all four layers and all ranks up to 32; no rank-32 basis from one task captures another. Full 16-layer deploy r6 (g4_3_deploy_r6, 2026-05-07): humaneval +9.903% exceeds 8% locked gate; gsm8k +60.9%; wikitext +110.5%. Task-conditional is NOT surviving. Class K cross-readout budget transfer (`BiasGenDecoupling.lean:cross_corpus_budget_violated_when_kappa_ratio_exceeds_headroom`, 2026-05-07) screens any cross-corpus deployment claim; R3f and R6.5 are further direct KILLs under this screen.
Lean theorems
task_union_basis_contains_task_basis
PROVED
global_delta_bytes_lt_per_task
PROVED
global_delta_bytes_lt_per_task_with_overhead
PROVED
Empirical probe
cross-check/ffn-quant/g4_task_conditional_probe.py
· JSON
lrh_plausibility 0.5 fractionLRH proxy collapses after deflation: 13/16 layers fall below the LRH-plausibility threshold once linear features are removed. Causal-circuit compression cannot rest on LRH for OLMoE.
Empirical probe
cross-check/ffn-quant/g5_lrh_activation_rank_probe.py
· JSON
route_flip_rate 0.1 fractionKilled at every tested rank. Route-flip rate exceeds the 10% tolerance even at r = router_dim − 4, ruling out unary low-rank routers.
Lean theorems
gap_preserved_under_perturbation
PROVED
topk_route_stability
PROVED
route_flip_zero_above_margin
PROVED
Empirical probe
cross-check/ffn-quant/g6_route_certificate_kill.py
· JSON
top100_coverage 0.95 fractionHot-set is too dispersed: top-100 dominant pairs cover only 72% of router traffic, well below the 95% gate. Lean machinery deferred until coverage gate is reopened.
Lean theorems
restricted_family_cannot_meet_target
PROVED
olmoe_joint_basis_no_low_distortion
PROVED
Empirical probe
TODO: g7_0_hot_set_diagnostic.py missing from cross-check/ffn-quant/
· JSON
held_out_residual_H 0.5 ratioKILLED 2026-05-02. RW1.x replacement ladder ran RW1.0 through RW1.5 on real OLMoE-1B-7B: frozen random features (RW1.0) fail quality (H≈1.12); learned features (RW1.1) overfit (train 0.054 vs held-out 0.477); shared/anchored/gated trims (RW1.2–RW1.3) stall on underfit/overfit frontier; source-layer mean fields through Noether-tangent constrained solves (RW1.4–RW1.4.8) stall near H=0.519 and kill at held-out gate; best oracle (RW1.4.8, all-layer source receptacle) H=0.686533 > 0.5; structured kernel mixtures (RW1.5) H≈1.12–1.16. Load-bearing block is train→eval generalization gap, not the worst-channel α≈0.984 replay amplification. RW2/RW3 replacement rungs are blocked. Mathematical Lean foundation grew to 20 theorems, 0 sorry (RWKVStability.lean): scalar Grönwall, per-channel envelope, sup-δ certification, L∞ + L2 aggregators, scan-monoid associativity, blockwise stability, hybrid attention split, low-budget kill certificates.
Lean theorems
error_le_geom_sum
PROVED
error_le_geom_closed
PROVED
affine_error_le_geom_sum
PROVED
affine_error_le_closed
PROVED
affine_error_le_closed_per_channel
PROVED
affine_error_le_closed_per_channel_sup
PROVED
affine_error_linf_le_per_channel_envelope
PROVED
affine_error_l2_le_per_channel_envelope
PROVED
affine_state_bound_geom_sum
PROVED
affine_state_bound_closed
PROVED
quotient_lipschitz
PROVED
combine_assoc
PROVED
block_error_le_geom_sum
PROVED
block_error_le_closed
PROVED
not_lowBudgetSmoothClosurePass_of_gate_failure
PROVED
lowBudgetGlobalG10_kill_certificate_of_smooth_gate_failure
PROVED
lowBudgetGlobalG10_kill_certificate_of_routing_gate_failure
PROVED
Empirical probe
TODO: rw_replacement_ladder_queue.py not found; scripts are per-rung in cross-check/rwkv-receptacle/
· JSON
hybrid_vs_smooth_only_ratio 0.5 ratioDiagnostic-constructive rung that explains the G_10 family's failures by separating compressible transport from incompressible routing. Decomposition probe on real OLMoE-1B-7B: 48/64 heads are hybrid (significant sparse mass), 16 transport-dominated, 0 pure routing-dominated; sparse mass mean 0.593 across all heads/layers. Hybrid reconstruction recovers attention output 3.7× tighter than RWKV alone. The routing-stability gate failed at 0.23 Jaccard between adjacent layers — sparse routing is dynamic and content-addressed, so the static-overlap metric is the wrong test. Future iteration G_10.6 should replace Jaccard with a subspace-overlap routing metric or per-layer head taxonomy. NOT a standalone compression mechanism: A_sparse must be preserved verbatim, only A_smooth is RWKV-compressible.
Lean theorems
attention_output_split
PROVED
hybrid_output_error_bound
PROVED
sparse_smooth_mass_decomposition
PROVED
Empirical probe
cross-check/rwkv-receptacle/g10_5_hybrid_decomposition.py
· JSON
KILLED 2026-04-28: Haar dense rotation harms the 16-layer OLMoE FFN path; dense rotation is not a ship lever.
Lean backing
ESCALATE 2026-04-29: INT4 SRHT beats Haar by +1.767 pp and is the only surviving shippable rotation lever.
Lean backing
All sub-rungs killed. R3a (SRHT INT2/INT1, 2026-04-29): INT2 SRHT +733.696% vs 15% ceiling; INT1 +1018%; mechanism gap holds (+4.34 pp at INT2) but lever insufficient. R3c (byte-budget, 2026-04-29): 26B SRHT INT4 = 12.902982 GB, 2.9 GB over sub-10GB gate; single-rung path killed. R3d (zero-output dormancy, 2026-04-29): 0/1024 strictly dormant cells after fixing accelerate hook; sanity figure 14.8% was hook-bypass artifact. See cross-check/preregistry/r3a_srht_bitwidth_sweep/, r3c_byte_budget/, r3d_dormancy_probe_2026-04-29/.
Lean backing
KILLED 2026-04-29: I_best K=64 +4.626% ≥ 4.234% ESCALATE ceiling. SRHT and top-K interact destructively — SRHT achieves isotropy (spreading channel activation energy uniformly), eliminating the concentrated outliers that top-K depends on. K sweep spans only 0.10 pp across all K values. Mechanism finding: srht_W_achieves_isotropic_floor (FFNGauge.lean:91, AXIOM) and top_k_optimal (MoEGauge.lean) preconditions are mutually exclusive. See cross-check/preregistry/r3e_srht_int4_topk_compose/decision.json.
Lean backing
Unblocks G_4 v1 stall
Lean backing
SHIP 2026-04-29: +0.972% at 16-layer; all four locked gates pass and wikitext-p99 anti-predictive failure is avoided. Per Class K (`BiasGenDecoupling.lean:equal_readouts_collapses`), single-readout calibration is required to declare a generation-path effect. The +0.972% quality delta uses logit sensitivity on baseline-greedy completion; future revisions must declare gen-path readout explicitly per `feedback_metric_matches_claim.md`.
SHIP 2026-04-30: joint +5.445% quality delta, mildly sub-additive vs +5.705% expectation; misses hard sub-10GB by ~0.5GB but validates task-conditioned quantization. Same Class K caveat as R5: the +5.445% quality delta is logit-sensitivity on baseline-greedy. SRHT structured-rotation effect on bias-path remains valid (per Paper 2 G_1.0' framing); generation-path declaration required for steering claim.
Lean backing
KILLED 2026-04-30: union16 misses bytes and fails all-corpus quality; union20 clears bytes but fails quality harder. Post-hoc Class K screen (`cross_corpus_budget_violated_when_kappa_ratio_exceeds_headroom`, 2026-05-07): union-all readout averages over corpora with disjoint κ-rankings, so the union prune budget cannot satisfy all per-corpus deployment budgets simultaneously.
Lean backing
KILLED 2026-05-07 (cross-check `r7_k16_full_quality_2026-05-07`): humaneval +6.230% PASS, gsm8k +7.367% PASS, wikitext +29.993% FAIL (Δ +5.187 pp vs k=13, headroom +2.0 pp). Class K cross-readout budget transfer: humaneval-side per-pp savings invert into wikitext-side per-pp cost at κ-ratio ≈ 6.6, exceeding the corpus-pair headroom ratio 2.55. Theorem-screened post-hoc by `cross_corpus_budget_violated_when_kappa_ratio_exceeds_headroom`; the screen would have predicted KILL pre-run from κ-ratio + headroom alone. Wall: 64.6 min; 16 layers; 3 corpora.
Lean backing
REOPENED 2026-05-07 under sub-10GB plan §5 all-three-fail clause (E1 mixed-precision standalone insufficient 2026-05-02; E2 task-conditioned KILLed at R6.5 2026-05-07; E3 repair gated on E2). Fresh pre-filter metrics required: any G_8 design must be theorem-screened by `cross_corpus_budget_violated_when_kappa_ratio_exceeds_headroom` (Class K) before allocation — selection corpus must be the deployment corpus, or the κ-ratio across the two must be bounded below the corpus-pair headroom ratio.
Lean backing
KILLED 2026-05-02 — RW1.x COMPLETE and KILLED: best oracle RW1.4.8 H=0.686533 > 0.5 held-out gate; train→eval generalization gap is the load-bearing block. Decision: KILL_RW1X_BLOCKS_RW2_RW3 (cross-check/preregistry/rwkv7_replacement_ladder_rw1_rw3/decision.json, 2026-05-02). Mathematical foundation: RWKVStability.lean 20 theorems, 0 sorry.
Lean backing
| Rung | Name | Status | Key evidence |
|---|---|---|---|
| G0 | Free orthogonal regauge | KILLED | r_eff ≥ 9 (layer), ≥ 32 (expert); residual ≥ 88.9% / 96.9% |
| G1 | Reclassified — spectrum diagnostic only | RECLASSIFIED | Spectrum-reshape diagnostic only; G₁.0’ (quantize round-trip) KILLED — 0/24 vs_orth pass at 0.50 gate (g1_0_prime_gauge_quant_r2, decision: kill) |
| G2 | Free Tucker on layer × expert × hidden | KILLED | r_eff ≥ 256; worst observed 262.773; residual ≥ 99.6% |
| G3 | Per-route weight aggregation | CONSTRUCTIVE | MODEST CONSTRUCTIVE — r_eff_eff min = 3.89, mean ≈ 5.6; q≈16–32 captures 58–80% energy |
| G4 | Task-conditional rank reduction | KILLED | KILLED — uniform rank-(16,24) killed (r2: 8/12, r3: 9/12, below 10/12 threshold); task-conditional r4 killed (wikitext fails at all ranks); full 16-layer deploy r6 killed (humaneval +9.90% > 8% gate, gsm8k +60.9%, wikitext +110.5%). |
| G5 | LRH-implied compression | KILLED | KILLED AT LRH PROXY — 13/16 layers LRH_IMPLAUSIBLE_AFTER_DEFLATION |
| G6 | Single-router rank reduction | KILLED | Route-flip rate above tolerance at all ranks |
| G7 | Pairwise router certificate (gated) | OPEN | HOT_SET_DISPENSED — C_pair r_eff=4.64, 153 dominant pairs; top-100 coverage 0.72 < 0.95 threshold |
| G10 | Contractive scan accumulation | KILLED | KILLED 2026-05-02 — RW1.x replacement ladder blocked: best oracle RW1.4.8 H=0.686533 > 0.5 held-out gate; train→eval generalization gap is the load-bearing block (not α≈0.984 replay). Decision: KILL_RW1X_BLOCKS_RW2_RW3 (cross-check/preregistry/rwkv7_replacement_ladder_rw1_rw3/decision.json). Lean foundation: 20 theorems, 0 sorry (RWKVStability.lean). |
| G10.5 | Smooth (RWKV) + Sparse (top-k routing) attention split | REFINE | DIAGNOSTIC-CONSTRUCTIVE 2026-05-02: hybrid output rel L2 0.213 vs RWKV-only 0.788 (3.7× improvement). Sparse mass mean 0.59 — confirms G_10’s failure was wrong target (RWKV trying to fit full A instead of A_smooth). Routing-stability gate failed (Jaccard 0.23 < 0.5) because routing is dynamic content-addressed, not static — methodology issue, not theory issue. |
| Rung | Name | GB delta | Status | Source mechanism |
|---|---|---|---|---|
| R1 | RotorQuant per-expert | -40 to -44 GB |
KILL | G_1.0′ (learned gauge, SRHT rotation) |
| R2 | SRHT/Hadamard structured rotation | -1.9 GB |
ESCALATE | G_1.0′ (SRHT bundle) |
| R3 | SRHT bit-width + dormancy pruning ladder | see sub-rungs |
KILL | G_5/G_6 (SRHT rotation, LRH deflation, task-deploy dropout) |
| R3e | SRHT INT4 + top-K per-token outlier compose | no additional saving over R2 |
KILL | G_5 (SRHT) + G_10 v4 (top-K activation outliers) |
| R4 | Task-conditional union basis | -0.6 to -1.0 GB |
pending | G_4 (task-conditional codebook, Gate 2) |
| R5 | Humaneval self-cal weak-expert pruning | quality lever |
SHIP | Task-conditioned weak-expert selection |
| R5+R2 | Weak-prune + SRHT INT4 composition | projects to ~10.5 GB on 26B |
SHIP | R5 task-self-calibration composed with R2 structured rotation |
| R6 | Union-all SRHT pruning | union16 10.048 GB; union20 9.335 GB |
KILL | Non-task-conditioned union of SRHT pruning decisions |
| R6.5 | Sub-10GB practical-escape triage (cross-check R7 step 1) | 9.892 GB byte projection (with attention 4→3); quality gate kills before bytes |
KILL | k=16 humaneval-self-cal weak-prune composed with SRHT INT4 (R5 + R2 at larger k), 16-layer OLMoE FFN |
| R7 | Trainable nullspace escape hatch | -1 to -2 GB (speculative) |
REOPENED-WITH-CONDITION | G_8 (trainable nullspace) |
| R8 | Recurrent receptacle replacement (KV-cache elimination) | potential 5–10 GB (KV-cache scaling, speculative) |
KILL | G_10 (RWKV-style contractive scan-monoid) |