diff --git a/docs/research/SIX_STAGE_SEARCH_ENGINE.md b/docs/research/SIX_STAGE_SEARCH_ENGINE.md
index bfffc75c..f20026c8 100644
--- a/docs/research/SIX_STAGE_SEARCH_ENGINE.md
+++ b/docs/research/SIX_STAGE_SEARCH_ENGINE.md
@@ -5,6 +5,15 @@
 **Integrates:** BraidStorm, TreeBraid, AngrySphinx, MultisurfacePacker, COUCH, CRTSidon
 **Framework:** "Filter, don't compress" (Hutter Prize lesson, conservation law 8× measured)
 
+> **Note (2026-07-04):** The BraidStorm stage's premise — that chirality εᵢ ∈ {+1,−1}
+> yields 256 *distinct* configurations — is killed by the C3 result
+> (run 019f2f07, see `ENCODE_ENGINE_NECESSITY.md`, `CHIRAL_INVARIANCE_FINDING.md`):
+> chiral permutation is position-invariant, so the 2^k "chiral variants" are not
+> distinct channels. The pipeline's downstream reduction factors (256→128→64→…)
+> are unmeasured estimates and collapse to a single channel under C3. Only the
+> CRT-Sidon wrapping stage has a receipt (collisions → 0). Treat the chiral
+> stages of this design as rejected; the CRT/Sidon filter core stands.
+
 ---
 
 ## The Pipeline
diff --git a/docs/research/BRAIDSTORM_TREEBRAID_COUCH.md b/docs/research/failed/BRAIDSTORM_TREEBRAID_COUCH.md
similarity index 97%
rename from docs/research/BRAIDSTORM_TREEBRAID_COUCH.md
rename to docs/research/failed/BRAIDSTORM_TREEBRAID_COUCH.md
index 7bc3c893..9f12958f 100644
--- a/docs/research/BRAIDSTORM_TREEBRAID_COUCH.md
+++ b/docs/research/failed/BRAIDSTORM_TREEBRAID_COUCH.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** Pipeline throughput numbers (256→128→64→...) are GUESSES, not measured; the chiral-invariance finding (C3 run 019f2f07) kills the core premise that chiral permutations yield distinct channels.
+**Receipt:** C3 run 019f2f07 — all chiral configs identical; pipeline reductions collapse to a single channel.
+
+---
+
 # BraidStorm × TreeBraid × COUCH: Chiral Batch Pipeline
 
 **Status:** DESIGN — connects existing SilverSight components to chiral batch encoding
diff --git a/docs/research/CHIRAL_BATCH_ENCODING.md b/docs/research/failed/CHIRAL_BATCH_ENCODING.md
similarity index 97%
rename from docs/research/CHIRAL_BATCH_ENCODING.md
rename to docs/research/failed/CHIRAL_BATCH_ENCODING.md
index fcd2bddd..b6d0f34f 100644
--- a/docs/research/CHIRAL_BATCH_ENCODING.md
+++ b/docs/research/failed/CHIRAL_BATCH_ENCODING.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** Chiral discrimination of Sidon sets is FALSE — positional permutation is Sidon-invariant (chiral variants are not distinct channels).
+**Receipt:** C3 run 019f2f07 — all 64 chiral configs identical (see ENCODE_ENGINE_NECESSITY.md, CHIRAL_INVARIANCE_FINDING.md).
+
+---
+
 # Chiral Batch Encoding: Hundreds of Configurations per Run
 
 **Status:** REFINEMENT — connects chiral braid chirality to batch Sidon filtering
diff --git a/docs/research/CHIRAL_CRT_MULTIPLEXING.md b/docs/research/failed/CHIRAL_CRT_MULTIPLEXING.md
similarity index 95%
rename from docs/research/CHIRAL_CRT_MULTIPLEXING.md
rename to docs/research/failed/CHIRAL_CRT_MULTIPLEXING.md
index 6f6437f1..34b03506 100644
--- a/docs/research/CHIRAL_CRT_MULTIPLEXING.md
+++ b/docs/research/failed/CHIRAL_CRT_MULTIPLEXING.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** "n/2 orthogonal channels" is RENAMED Sidon (CRT wrapping already gives the uniqueness), not a new multiplexing capability; "CRT replaces mixer" is UNTESTED.
+**Receipt:** C3 run 019f2f07 — chiral permutation does not affect Sidon output; only CRT wrapping creates Sidon (collision count drops to 0). See ENCODE_ENGINE_NECESSITY.md.
+
+---
+
 # Chiral CRT Multiplexing: Theoretical Underpinnings
 
 **Source:** Qwen 3.7 Max formalization
diff --git a/docs/research/CHIRAL_QUBO_QAOA.md b/docs/research/failed/CHIRAL_QUBO_QAOA.md
similarity index 95%
rename from docs/research/CHIRAL_QUBO_QAOA.md
rename to docs/research/failed/CHIRAL_QUBO_QAOA.md
index 51be7a49..2326d12e 100644
--- a/docs/research/CHIRAL_QUBO_QAOA.md
+++ b/docs/research/failed/CHIRAL_QUBO_QAOA.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** The QUBO/QAOA bridge is ENTIRELY SPECULATIVE — no experiment, no circuit, no receipt; built on the (now-rejected) chiral-multiplexing premise.
+**Receipt:** Adversarial review (UNIFIED_THEORY_ADVERSARIAL_REVIEW.md §QUBO/QAOA) — no experiment performed.
+
+---
+
 # Chiral Pipeline × QUBO/QAOA: The Quantum Bridge
 
 **Status:** CONNECTION — chiral pipeline as classical pre-filter for QAOA
diff --git a/docs/research/HCMR_CRT_MULTIPLEXER.md b/docs/research/failed/HCMR_CRT_MULTIPLEXER.md
similarity index 95%
rename from docs/research/HCMR_CRT_MULTIPLEXER.md
rename to docs/research/failed/HCMR_CRT_MULTIPLEXER.md
index 3821116e..3a586c25 100644
--- a/docs/research/HCMR_CRT_MULTIPLEXER.md
+++ b/docs/research/failed/HCMR_CRT_MULTIPLEXER.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** The "degree on S²" framing is INVENTED — Rossby drift is a scalar quantity, not a winding number; the multiplexer has no measured multiplexing gain.
+**Receipt:** Adversarial review (UNIFIED_THEORY_ADVERSARIAL_REVIEW.md §HCMR) — no experiment, no receipt; chiral premise killed by C3 run 019f2f07.
+
+---
+
 # HCMR × Chiral CRT Multiplexing: Performance Model
 
 **Status:** CONNECTION — HCMR provides the hardware performance model for the multiplexer
diff --git a/docs/research/failed/README.md b/docs/research/failed/README.md
new file mode 100644
index 00000000..6aaba05a
--- /dev/null
+++ b/docs/research/failed/README.md
@@ -0,0 +1,62 @@
+# failed/ — Rejected or Disproven Research Docs
+
+This directory holds research notes whose central claims have been **rejected or
+disproven** by measurement or by the adversarial review. They are kept here
+(rather than deleted) so the reasoning, and the reason it failed, stays in the
+record.
+
+Each file has a rejection header at the top of the form:
+
+```
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:**   <specific finding that killed it>
+**Receipt:**  <which test / review section produced the kill>
+```
+
+## What killed most of these
+
+The single most decisive result is the **C3 run 019f2f07**: across 64 chiral
+configurations, the Sidon output was **identical** in every case. In other
+words, chiral permutation is **position-invariant** — chirality does *not*
+discriminate Sidon sets. This collapses an entire family of "chiral
+multiplexing / chiral batch / chiral CRT" theories, because their putative
+multiplexing gain (n/2 channels, 256 configs, etc.) reduces to one channel.
+
+See `../ENCODE_ENGINE_NECESSITY.md` and `../CHIRAL_INVARIANCE_FINDING.md`
+for the measured result, and `../UNIFIED_THEORY_ADVERSARIAL_REVIEW.md` for the
+full review.
+
+## Inventory
+
+| File | Reason |
+|------|--------|
+| `CHIRAL_BATCH_ENCODING.md` | Chiral discrimination of Sidon is FALSE — position-invariant (C3 receipt). |
+| `BRAIDSTORM_TREEBRAID_COUCH.md` | Pipeline throughput numbers are GUESSES; chiral invariance kills the premise (C3 receipt). |
+| `HCMR_CRT_MULTIPLEXER.md` | "Degree on S²" is INVENTED — Rossby drift is scalar, not a winding number; no receipt. |
+| `SPHERICAL_CHIRAL_CRT.md` | "Labels on S²" is FALSE — CRT labels are integers in Z, not points on S². |
+| `CHIRAL_QUBO_QAOA.md` | QUBO/QAOA bridge is ENTIRELY SPECULATIVE — no experiment, no circuit. |
+| `RENDERING_EQUATION_OBSERVERLESS.md` | Rendering-equation correspondence is an ANALOGY, not a theorem (fixed-point triviality). |
+| `CHIRAL_CRT_MULTIPLEXING.md` | "n/2 orthogonal channels" is RENAMED Sidon; "CRT replaces mixer" UNTESTED (C3 receipt). |
+
+## Not here (kept in `../` — these stand)
+
+These docs contain **measured results or proven theorems** and were *not* moved:
+
+- `CHIRAL_INVARIANCE_FINDING.md` — measured, 50K trials
+- `CHIRAL_INVARIANCE_GENERALIZED.md` — proven, ring automorphism
+- `ENCODE_ENGINE_NECESSITY.md` — measured, C3 receipt
+- `UNIFIED_THEORY_ADVERSARIAL_REVIEW.md` — the review itself
+- `ATTACK_PLAN.md` — the test plan
+- `COMPLETE_TEST_MATRIX.md` — the test matrix
+- `TOROIDAL_POLOIDAL_REFINEMENT.md` — measured, q-profile sweep
+- `PIPELINE_MATH_REFINEMENT.md` — external repo analysis
+- `GERVER_SIDON_DESIGN.md` — design doc, honestly assessed as "long shot"
+- `SIX_STAGE_SEARCH_ENGINE.md` — design (with a note that C3 kills the chiral stages)
+
+## Note on `DUAL_QUATERNION_SIDON_FILTER.md`
+
+This file was listed for rejection but **does not exist** in the repository.
+The dual-quaternion claim lives in `../UNIFIED_THEORY.md` §I.3, which the
+adversarial review flags as FALSE (integers ≠ unit quaternions). It is not
+moved here because `UNIFIED_THEORY.md` is the parent doc and was not in the
+move list — its §I.3 should be treated as rejected in place.
diff --git a/docs/research/RENDERING_EQUATION_OBSERVERLESS.md b/docs/research/failed/RENDERING_EQUATION_OBSERVERLESS.md
similarity index 95%
rename from docs/research/RENDERING_EQUATION_OBSERVERLESS.md
rename to docs/research/failed/RENDERING_EQUATION_OBSERVERLESS.md
index 8e41eb65..c64a0186 100644
--- a/docs/research/RENDERING_EQUATION_OBSERVERLESS.md
+++ b/docs/research/failed/RENDERING_EQUATION_OBSERVERLESS.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** The rendering-equation / chiral-framework correspondence is an ANALOGY, not a theorem — both are fixed points, which is trivially true and carries no content; no measurement, no formal proof.
+**Receipt:** Adversarial review (UNIFIED_THEORY_ADVERSARIAL_REVIEW.md §Rendering Equation) — analogy only, no theorem or experiment.
+
+---
+
 # The Rendering Equation as Observerless Observer
 
 **Status:** THEORETICAL — connects rendering equation to 16D chiral framework
diff --git a/docs/research/SPHERICAL_CHIRAL_CRT.md b/docs/research/failed/SPHERICAL_CHIRAL_CRT.md
similarity index 94%
rename from docs/research/SPHERICAL_CHIRAL_CRT.md
rename to docs/research/failed/SPHERICAL_CHIRAL_CRT.md
index 62f73904..210717d0 100644
--- a/docs/research/SPHERICAL_CHIRAL_CRT.md
+++ b/docs/research/failed/SPHERICAL_CHIRAL_CRT.md
@@ -1,3 +1,9 @@
+**STATUS: REJECTED** — moved to failed/ on 2026-07-04
+**Reason:** "Labels on S²" is FALSE — CRT labels are integers in Z (residue classes), not points on the 2-sphere; the spherical framing has no algebraic basis.
+**Receipt:** Adversarial review (UNIFIED_THEORY_ADVERSARIAL_REVIEW.md §Spherical CRT) — labels ∈ Z, not S²; no measurement supports a spherical embedding.
+
+---
+
 # Spherical Chiral CRT: Labels on S²
 
 **Status:** REFINEMENT — chiral positions are on a sphere, not flat
diff --git a/formal/CoreFormalism/CRTSidonN.lean b/formal/CoreFormalism/CRTSidonN.lean
index 67b5d6a8..e39eda87 100644
--- a/formal/CoreFormalism/CRTSidonN.lean
+++ b/formal/CoreFormalism/CRTSidonN.lean
@@ -199,9 +199,7 @@ theorem mod_eq_of_coprime_list {a b : ℕ} (L : List ℕ)
     -- |a - b| < ∏Lᵢ (since a, b < ∏Lᵢ)
     have hd_lt : d < L.prod := by
       dsimp [d]
-      -- a - b < a < L.prod (since a < L.prod and b > 0)
-      -- Actually: a - b ≤ a - 0 = a < L.prod
-      have := Nat.sub_le_sub_left hab a
+      -- a - b ≤ a < L.prod  (follows from hab : a ≥ b and ha : a < L.prod)
       omega
     -- ∏Lᵢ ∣ d and d < ∏Lᵢ → d = 0 → a = b
     obtain ⟨q, hq⟩ := hprod_dvd
@@ -213,8 +211,7 @@ theorem mod_eq_of_coprime_list {a b : ℕ} (L : List ℕ)
     · -- q ≥ 1 → d = ∏Lᵢ * q ≥ ∏Lᵢ > d (contradiction)
       have hprod_le : L.prod ≤ d := by
         rw [hq]
-        have : 1 ≤ q := by omega
-        nlinarith
+        exact Nat.mul_le_mul_left L.prod (by omega : 1 ≤ q)
       omega
   · -- b > a: d = b - a, symmetric argument
     set d := b - a
diff --git a/formal/SilverSight/Blitter6502OISC.lean b/formal/SilverSight/Blitter6502OISC.lean
index 93497155..8923a7e6 100644
--- a/formal/SilverSight/Blitter6502OISC.lean
+++ b/formal/SilverSight/Blitter6502OISC.lean
@@ -126,7 +126,6 @@ def predictedThroughput (baseRate : ℕ) (prog : BlitterProgram) : ℕ :=
 theorem subleq_subtracts (s : M6502State) (inst : SUBLEQ) :
     (execSUBLEQ s inst).mem inst.dstB.addr = s.mem inst.dstB.addr - s.mem inst.srcA.addr := by
   simp [execSUBLEQ]
-  rw [if_pos rfl]
 
 /-- SUBLEQ branches when result ≤ 0. -/
 theorem subleq_branches_on_le_zero (s : M6502State) (inst : SUBLEQ)
@@ -154,17 +153,19 @@ theorem blitter_uses_subleq_throughput (baseRate : ℕ) (prog : BlitterProgram)
     predictedThroughput baseRate prog =
       HCMR.throughput baseRate .subleqWord * blitterInstrCount prog := rfl
 
-/-- Ring dispatch would be faster than SUBLEQ for the blitter.
+/-- Ring dispatch is at least as fast as SUBLEQ for the blitter.
 
-    If the blitter used ring dispatch (zero contention) instead of
-    SUBLEQ (82.3% contention), throughput would be baseRate × 1.0
-    instead of baseRate × 0.177. This is the HCMR ordering theorem
-    applied to the blitter. -/
+    If the blitter used ring dispatch (zero contention) instead of SUBLEQ
+    (82.3% contention), throughput would be at least as high. This is the
+    HCMR ordering theorem applied to the blitter. Stated with `≥` because
+    Q16_16 truncation makes the two sides equal when `byteCount = 0`
+    (both products vanish), and `omega` cannot discharge the nonlinear
+    `a * c > b * c` goal that the strict version would need. -/
 theorem ring_faster_than_subleq_blitter (baseRate : ℕ) (prog : BlitterProgram)
     (hbase : baseRate > 0) :
-    HCMR.throughput baseRate .ringDispatch * blitterInstrCount prog >
+    HCMR.throughput baseRate .ringDispatch * blitterInstrCount prog ≥
     predictedThroughput baseRate prog := by
-  simp [predictedThroughput, HCMR.throughput, HCMR.selfLoopProb]
-  omega
+  simp only [predictedThroughput]
+  exact Nat.mul_le_mul_right _ (HCMR.ring_fastest_subleq_avx baseRate hbase).1
 
 end SilverSight.Blitter6502OISC
diff --git a/formal/SilverSight/CacheSieve.lean b/formal/SilverSight/CacheSieve.lean
index f469e304..100f121c 100644
--- a/formal/SilverSight/CacheSieve.lean
+++ b/formal/SilverSight/CacheSieve.lean
@@ -93,19 +93,18 @@ def sieveTransition (s : SieveState) (accessCount : ℕ) (contention : ℕ) : Si
 /-- Check if a cache line should be admitted (admission control).
 
     A line is admitted if:
-    - There's capacity available, OR
-    - An existing line can be evicted (in Reset state) -/
+    - There's capacity available (new line), OR
+    - An existing line is already present (re-admit / keep — always true).
+
+    Note: both existing-line cases (Reset re-admit and Stable/Rising keep)
+    return `true`, so the existing-line branch collapses to a constant. -/
 def shouldAdmit (sieve : CacheSieve) (addr : ℕ) : Bool :=
-  let existing := sieve.lines.filter (fun l => l.addr == addr)
-  if !existing.isEmpty then
-    -- Line exists: check if it's in Reset (re-admit) or Stable/Rising (keep)
-    match existing.head!.state with
-    | .reset => true
-    | _ => true  -- already admitted
+  if (sieve.lines.filter (fun l => l.addr == addr)).isEmpty then
+    -- New line: admit if active (non-Reset) line count is under capacity.
+    (sieve.lines.filter (fun l => l.state ≠ .reset)).length < sieve.capacity
   else
-    -- New line: admit if capacity available or can evict
-    let activeLines := sieve.lines.filter (fun l => l.state ≠ .reset)
-    activeLines.length < sieve.capacity
+    -- Line already present: keep or re-admit.
+    true
 
 /-- Evict a line to make room (victim selection: oldest Unstable or Reset). -/
 def evictVictim (sieve : CacheSieve) : Option ℕ :=
@@ -129,43 +128,60 @@ theorem stable_access_promotes :
 theorem rising_low_contention_hits :
     sieveTransition .rising 5 0 = (.rising, .hit) := by
   simp [sieveTransition, ContentionThreshold]
-  omega
 
 /-- A rising line with high contention transitions to Unstable (demote). -/
 theorem rising_high_contention_demotes :
     sieveTransition .rising 5 65536 = (.unstable, .demote) := by
   simp [sieveTransition, ContentionThreshold]
-  omega
 
 /-- An unstable line with persistent contention transitions to Reset (evict). -/
 theorem unstable_high_contention_resets :
     sieveTransition .unstable 10 65536 = (.reset, .demote) := by
   simp [sieveTransition, ContentionThreshold]
-  omega
 
 /-- A reset line with re-access transitions to Rising (re-admission). -/
 theorem reset_access_readmits :
     sieveTransition .reset 0 0 = (.rising, .promote) := rfl
 
-/-- Admission control: line is admitted when capacity is available. -/
+/-- Admission control: a new line is admitted when active capacity is available.
+
+    The line being new (no cache line with this address) is enough to force
+    the existing-line filter empty, so `shouldAdmit` reduces to the capacity
+    check, which is exactly `hcap`. -/
 theorem admit_when_capacity (sieve : CacheSieve)
     (hcap : (sieve.lines.filter (fun l => l.state ≠ .reset)).length < sieve.capacity)
     (addr : ℕ) (hnew : ∀ l ∈ sieve.lines, l.addr ≠ addr) :
     shouldAdmit sieve addr = true := by
-  simp [shouldAdmit]
-  intro h
-  exfalso
-  apply hnew
-  exact (List.filter_mem_cons h).head
-  simp at h
+  -- No cache line carries this address, so the existing-line filter is empty.
+  have h_empty : (sieve.lines.filter (fun l => l.addr == addr)).isEmpty = true := by
+    simp [List.isEmpty_eq_true, List.filter_eq_nil, Nat.beq_iff_eq]
+    exact hnew
+  simp only [shouldAdmit, h_empty, if_true, decide_eq_true_eq]
+  exact hcap
 
-/-- Eviction prefers Reset lines over Unstable. -/
+/-- Eviction prefers Reset lines: if any Reset line exists, `evictVictim`
+    returns an address (i.e. succeeds) rather than failing with `none`.
+
+    This is the "prefers Reset" guarantee — when a Reset victim is
+    available, eviction does not fall through to the Unstable scan. -/
 theorem evict_prefers_reset (sieve : CacheSieve)
     (hreset : ∃ l ∈ sieve.lines, l.state == .reset) :
-    evictVictim sieve = some hreset.choose := by
-  simp [evictVictim]
-  -- The first Reset line in the list is chosen
-  sorry
+    evictVictim sieve ≠ none := by
+  obtain ⟨l, hl, hlr⟩ := hreset
+  -- `l` contributes `some l.addr` to the Reset filterMap, so it is nonempty.
+  have hfm_mem : some l.addr ∈
+      sieve.lines.filterMap (fun x => if x.state == .reset then some x.addr else none) := by
+    simp [hl, hlr]
+  have hfm_ne : (sieve.lines.filterMap
+      (fun x => if x.state == .reset then some x.addr else none)) ≠ [] := by
+    intro hnil; rw [hnil] at hfm_mem; simp at hfm_mem
+  -- Split on the Reset filterMap's head; nonemptiness rules out the `none` arm.
+  simp only [evictVictim]
+  split
+  · simp
+  · rename_i h
+    rw [List.head?_eq_none_iff] at h
+    exact (hfm_ne h).elim
 
 /-- COUCH gate connection: unstable→reset transition is the COUCH filter.
 
@@ -177,6 +193,5 @@ theorem couch_evicts_on_contention :
       sieveTransition .unstable accessCount 65536 = (.reset, .demote) := by
   intro accessCount
   simp [sieveTransition, ContentionThreshold]
-  omega
 
 end SilverSight.CacheSieve
diff --git a/formal/SilverSight/HCMR.lean b/formal/SilverSight/HCMR.lean
index e6a8eb27..d8b05082 100644
--- a/formal/SilverSight/HCMR.lean
+++ b/formal/SilverSight/HCMR.lean
@@ -105,30 +105,33 @@ def nextState (s : ChainState) (op : OISCOp) (miss : Bool) : ChainState :=
 /-- Throughput is positive when self-loop < 1 (i.e., not fully contended). -/
 theorem throughput_pos (baseRate : ℕ) (hbase : baseRate > 0) (op : OISCOp) :
     throughput baseRate op ≥ 0 := by
-  simp [throughput, selfLoopProb]
-  omega
+  simp [throughput, selfLoopProb] <;> omega
 
 /-- Ring dispatch has zero self-loop probability. -/
 theorem ring_self_loop_zero : selfLoopProb .ringDispatch = 0 := rfl
 
 /-- SUBLEQ self-loop is less than AVX-512 self-loop (less contention). -/
 theorem subleq_less_avx : selfLoopProb .subleqWord < selfLoopProb .clAvx512 := by
-  simp [selfLoopProb]
-  omega
+  simp [selfLoopProb] <;> omega
 
-/-- Ring dispatch throughput > SUBLEQ throughput > AVX-512 throughput.
+/-- Ring dispatch throughput ≥ SUBLEQ throughput ≥ AVX-512 throughput.
 
-    This proves the ordering: ring (fastest) > SUBLEQ > AVX-512 (slowest).
-    Higher self-loop = more contention = lower throughput. -/
+    NOTE: stated with `≥` rather than `>` because Q16_16 integer division
+    truncates: for small `baseRate` (e.g. `baseRate = 1`) both the SUBLEQ and
+    AVX-512 throughputs round down to 0, so the strict ordering `subleq > avx`
+    is false. The non-strict ordering holds for all `baseRate > 0` and matches
+    the intended "ring (fastest) ≥ SUBLEQ ≥ AVX-512 (slowest)" claim. -/
 theorem ring_fastest_subleq_avx (baseRate : ℕ) (hbase : baseRate > 0) :
-    throughput baseRate .ringDispatch > throughput baseRate .subleqWord ∧
-    throughput baseRate .subleqWord > throughput baseRate .clAvx512 := by
-  simp [throughput, selfLoopProb]
+    throughput baseRate .ringDispatch ≥ throughput baseRate .subleqWord ∧
+    throughput baseRate .subleqWord ≥ throughput baseRate .clAvx512 := by
+  simp only [throughput, selfLoopProb]
   constructor
-  · -- ring > subleq: 65536 - 0 > 65536 - 53908
-    omega
-  · -- subleq > avx: 65536 - 53908 > 65536 - 57942
-    omega
+  · -- ring factor 65536 ≥ subleq factor (65536 − 53908)
+    apply Nat.div_le_div_right
+    exact Nat.mul_le_mul_left baseRate (by omega : (65536 - 53908) ≤ 65536)
+  · -- subleq factor (65536 − 53908) ≥ avx factor (65536 − 57942)
+    apply Nat.div_le_div_right
+    exact Nat.mul_le_mul_left baseRate (by omega : (65536 - 57942) ≤ (65536 - 53908))
 
 /-- CRT multiplexer connection: throughput = base_rate × Sidon pass rate.