diff --git a/Complexity/Computability/Complexity/FineGrained/SparseCountingScale.lean b/Complexity/Computability/Complexity/FineGrained/SparseCountingScale.lean
index 2e424d559..4ec243d47 100644
--- a/Complexity/Computability/Complexity/FineGrained/SparseCountingScale.lean
+++ b/Complexity/Computability/Complexity/FineGrained/SparseCountingScale.lean
@@ -195,14 +195,6 @@ theorem two_le_numGroups_of_clog_ge {n : ℕ} (h : 640000 ≤ Nat.clog 2 n) :
     rw [hm_eq]
     exact (four_mul_succ_pow_four_le_two_pow (by omega)).trans hpow_lt.le
 
-/-- Symbolic dyadic strict-lower-bound threshold: if `639999 ≤ m` and `2 ^ m < n`, then
-`2 ≤ numGroups n`. -/
-theorem two_le_numGroups_of_pow_lt {m n : ℕ} (hm : 639999 ≤ m) (hn : 2 ^ m < n) :
-    2 ≤ numGroups n := by
-  apply two_le_numGroups_of_clog_ge
-  have hlt : m < Nat.clog 2 n := (Nat.lt_clog_iff_pow_lt one_lt_two).mpr hn
-  omega
-
 /-- Explicit dyadic threshold: for `2 ^ 640000 ≤ n`, `2 ≤ numGroups n`. -/
 theorem two_le_numGroups_of_pow_le {n : ℕ} (hn : 2 ^ 640000 ≤ n) :
     2 ≤ numGroups n :=
@@ -540,16 +532,6 @@ private theorem eventually_two_pow_succ_clog_pow_le (C : ℝ) (d : ℕ) {ε : 
       linarith [mul_le_mul_of_nonneg_left hp hC.le]
     exact (Real.rpow_le_rpow_of_exponent_le one_le_two hexp).trans hpow
 
-/-- Quasi-polynomial natural-exponential overhead `exp (C * ⌈log₂ n⌉ ^ d)` is eventually bounded by
-`(2 : ℝ) ^ (ε * interpolationScale n)` for every `ε > 0`. -/
-theorem eventually_exp_clog_pow_le (C : ℝ) (d : ℕ) {ε : ℝ} (hε : 0 < ε) :
-    ∀ᶠ n : ℕ in atTop, Real.exp (C * (Nat.clog 2 n : ℝ) ^ d) ≤
-      (2 : ℝ) ^ (ε * interpolationScale n) := by
-  filter_upwards [eventually_mul_clog_pow_le_interpolationScale C d
-    (mul_pos hε (Real.log_pos one_lt_two))] with n hn
-  rw [Real.rpow_def_of_pos two_pos, Real.exp_le_exp]
-  linarith
-
 /-- Concrete leaf-factor bound (`A_tree = 17`): for any polynomial degree `d`, eventually
 `(n + numGroups n + 1) ^ d * 2 ^ (n / numGroups n) ≤ 2 ^ (17 * ρ(n))`. -/
 theorem eventually_poly_mul_two_pow_div_numGroups_le (d : ℕ) :
@@ -760,17 +742,6 @@ theorem eventually_leafOccurrenceBound_le (C_k : ℕ) {k : ℕ} (hk : 1 ≤ k) :
   exact (Nat.clog_pow 2 C_k one_lt_two).symm.le.trans
     (Nat.clog_mono_right 2 ((le_max_right 5 (2 ^ C_k)).trans hn))
 
-/-- Unconditional existential form for arbitrary `k : ℕ`: there exists `β : ℕ` (`β = max k 1`)
-such that eventually `leafOccurrenceBound C_k k (numGroups n) ≤ ⌈log₂ n⌉ ^ β`. -/
-theorem exists_eventually_leafOccurrenceBound_le (C_k k : ℕ) :
-    ∃ β : ℕ, ∀ᶠ n : ℕ in atTop, leafOccurrenceBound C_k k (numGroups n) ≤ Nat.clog 2 n ^ β := by
-  rcases Nat.eq_zero_or_pos k with rfl | hk
-  · refine ⟨1, ?_⟩
-    filter_upwards [eventually_ge_atTop (2 ^ C_k)] with n hn
-    simp only [leafOccurrenceBound, Nat.zero_sub, pow_zero, mul_one, pow_one]
-    exact (Nat.clog_pow 2 C_k one_lt_two).symm.le.trans (Nat.clog_mono_right 2 hn)
-  · exact ⟨k, eventually_leafOccurrenceBound_le C_k hk⟩
-
 /-- Direct Lemma 4.8 feasibility bridge: for `1 ≤ k`, the Proposition 6.4 leaf-occurrence cap
 `leafOccurrenceBound C_k k (numGroups n)` eventually discharges the `b ≤ ⌈log₂ n⌉ ^ k` hypothesis
 of `ReplacementParams.exists_feasible`, yielding `ReplacementParams.Feasible k n b w M`. -/
diff --git a/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean b/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean
index d37002b53..2eae5901a 100644
--- a/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean
+++ b/Complexity/Computability/PolyTime/BooleanAnalysis/SparsePolyCounter.lean
@@ -272,9 +272,6 @@ theorem countSystemExhaustive_eq_rootCount (n : ℕ) (sys : List (List (List ℕ
         HeavyBranchFold.extendAssignment, dite_eq_right hv]
   rw [hfun]
 
-theorem scopeWidthOn_le (n : ℕ) (eq : List (List ℕ)) : scopeWidthOn n eq ≤ n :=
-  List.countP_le_length.trans_eq List.length_range
-
 theorem scopeWidthOn_eq_length_equationVars {n : ℕ} {eq : List (List ℕ)}
     (hvars : ∀ m ∈ eq, ∀ v ∈ m, v < n) : scopeWidthOn n eq = (equationVars eq).length := by
   rw [scopeWidthOn, List.countP_eq_length_filter,
@@ -765,14 +762,6 @@ theorem countSparsePolySystem_eq_commonZeroCount
   rw [countSparsePolySystem_eq_rootCount hbranch inp,
     HeavyBranchFold.rootCount_eq_commonZeroCount hcan hvars]
 
-theorem countSparsePolySystem_le_two_pow
-    (hbranch : ∀ n' eqs', checkBranchFeasible N₀_branch (n', eqs') = true →
-      branchEval (prepareBranchEvalInput (n', eqs')) = HeavyBranchFold.rootCount n' eqs')
-    (inp : SparseSystemInput) :
-    countSparsePolySystem N₀_top N₀_branch branchEval inp ≤ 2 ^ inp.1 :=
-  (countSparsePolySystem_eq_rootCount hbranch inp).trans_le
-    (HeavyBranchFold.rootCount_le_two_pow inp.1 inp.2.2)
-
 end SemanticExactness
 
 /-- Markov heavy-variable bound (§5.5, p. 38): `M_eqs * s_div ≤ b₀ * n → |S| ≤ n / s_div`. -/
diff --git a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
index 2949d2035..9972e31ef 100644
--- a/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
+++ b/Complexity/Computability/PolyTime/CNF/BranchedSparseCNFCounter.lean
@@ -147,9 +147,6 @@ theorem leafDensityRatio_eq_prop64LeafClauseRatio {k N : ℕ}
   simp only [leafDensityRatio, leafOccBound_eq_sum, leafThresholdBase, leafSearchDivisor,
     max_eq_right hs, CNF.prop64LeafClauseRatio, CNF.prop64ThresholdBase]
 
-/-- `1 ≤ leafDensityRatio k N` for all `k, N : ℕ`. -/
-theorem one_le_leafDensityRatio (k N : ℕ) : 1 ≤ leafDensityRatio k N := Nat.succ_pos _
-
 /-- For `1 ≤ N`, `leafOccBound k N * N + 1 ≤ leafDensityRatio k N * N`. -/
 theorem leafOccBound_mul_succ_le_leafDensityRatio_mul {k N : ℕ} (hN : 1 ≤ N) :
     leafOccBound k N * N + 1 ≤ leafDensityRatio k N * N :=
diff --git a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
index 796e00a93..8dd14ef1c 100644
--- a/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
+++ b/Complexity/Computability/PolyTime/CNF/GreedyParitySearch.lean
@@ -134,11 +134,6 @@ def encodeTestTuple (m : ℕ) (γ : List (ℕ × Bool)) : ℕ :=
 
 @[simp] theorem decodeTestTuple_zero_right (m j : ℕ) : decodeTestTuple m 0 j = [] := rfl
 
-@[simp] theorem decodeTestTuple_zero_left (P j : ℕ) :
-    decodeTestTuple 0 P j = List.replicate P (0, false) := by
-  simp only [decodeTestTuple, ↓reduceIte, Nat.zero_div, Nat.zero_mod, zero_ne_one, decide_false,
-    List.map_const', List.length_range]
-
 @[simp] theorem length_decodeTestTuple (m P j : ℕ) : (decodeTestTuple m P j).length = P := by
   simp only [decodeTestTuple, List.length_map, List.length_range]
 
@@ -353,12 +348,6 @@ def materializeTestRow (m : ℕ) (γ : List (ℕ × Bool)) : List Bool :=
     (materializeTestRow m γ).length = m := by
   simp only [materializeTestRow, List.length_map, List.length_range]
 
-@[simp] theorem materializeTestRow_zero (γ : List (ℕ × Bool)) : materializeTestRow 0 γ = [] := rfl
-
-@[simp] theorem materializeTestRow_nil (m : ℕ) :
-    materializeTestRow m [] = List.replicate m false := by
-  simp only [materializeTestRow, List.foldl_nil, List.map_const', List.length_range]
-
 private theorem foldl_xor_eq_sum (e : ℕ) (γ : List (ℕ × Bool)) (init : Bool) :
     γ.foldl (fun acc p => if p.1 = e then xor acc p.2 else acc) init =
       init + (γ.map fun p => if p.1 = e then p.2 else 0).sum := by
@@ -378,10 +367,6 @@ theorem materializeTestRow_ofFn {m P : ℕ} (γ : Fin P → Fin m × Bool) :
   exact congrArg (fun fn => (List.ofFn fn).sum)
     (funext fun r => by simp only [Function.comp_apply, Fin.ext_iff])
 
-@[simp] theorem ofList_materializeTestRow_ofFn {m P : ℕ} (γ : Fin P → Fin m × Bool) :
-    ofList m (materializeTestRow m (List.ofFn fun r => ((γ r).1.val, (γ r).2))) = testRow γ := by
-  rw [materializeTestRow_ofFn, ofList_ofFn]
-
 private theorem foldl_xor_eq_false_of_not_mem (e : ℕ) (γ : List (ℕ × Bool))
     (h : e ∉ γ.map Prod.fst) :
     γ.foldl (fun acc p => if p.1 = e then xor acc p.2 else acc) false = false := by
@@ -505,10 +490,6 @@ theorem greedyParityRowsAt_succ (countSys : List (List Bool) → ℕ)
         [selectBestTestRow countSys m P (greedyParityRowsAt countSys m P initRows i)] :=
   Function.iterate_succ_apply' _ _ _
 
-@[simp] theorem greedyParityRows_zero_left (countSys : List (List Bool) → ℕ)
-    (m P : ℕ) (initRows : List (List Bool)) :
-    greedyParityRows countSys 0 m P initRows = initRows := rfl
-
 /-! ### Prefix invariant, tie-breaking, and minimality -/
 
 private theorem run_selectBestStep_params (countSys : List (List Bool) → ℕ)
@@ -639,22 +620,6 @@ private theorem prefix_greedyParityRowsAt (countSys : List (List Bool) → ℕ)
   | zero => exact List.prefix_rfl
   | succ i ih => rw [greedyParityRowsAt_succ]; exact ih.trans (List.prefix_append _ _)
 
-/-- Every row appended after `initRows` has exact length `m` and Hamming weight `≤ P`. -/
-theorem mem_drop_greedyParityRows (countSys : List (List Bool) → ℕ)
-    (n m P : ℕ) (initRows : List (List Bool)) {r : List Bool}
-    (hr : r ∈ (greedyParityRows countSys n m P initRows).drop initRows.length) :
-    r.length = m ∧ r.count true ≤ P := by
-  suffices ∀ i, ∀ r ∈ (greedyParityRowsAt countSys m P initRows i).drop initRows.length,
-      r.length = m ∧ r.count true ≤ P from this (3 * n) r hr
-  intro i; induction i with
-  | zero => intro _ h; simp only [greedyParityRowsAt_zero, List.drop_length, List.not_mem_nil] at h
-  | succ i ih =>
-    intro r h; rw [greedyParityRowsAt_succ, List.drop_append_of_le_length
-      (prefix_greedyParityRowsAt countSys m P initRows i).length_le, List.mem_append,
-      List.mem_singleton] at h
-    exact h.elim (ih r) fun hr =>
-      hr ▸ ⟨length_selectBestTestRow _ _ _ _, count_true_selectBestTestRow_le _ _ _ _⟩
-
 private theorem mem_greedyParityRowsAt (countSys : List (List Bool) → ℕ)
     {m P : ℕ} {initRows : List (List Bool)} {i : ℕ} {r : List Bool}
     (hr : r ∈ greedyParityRowsAt countSys m P initRows i) :
diff --git a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean
index 54c7b3092..35035e29b 100644
--- a/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean
+++ b/Complexity/Computability/PolyTime/CNF/SparsePolyCompile.lean
@@ -752,16 +752,6 @@ def compileParitySystemBounded (k : ℕ) (φ : CNF ℕ) (rows : List (List Bool)
     List (List (List ℕ)) :=
   compileParitySystem (φ.map (List.take k)) rows
 
-theorem compileClauseBounded_eq_compileClause {k : ℕ} {c : Clause ℕ} (hc : c.length ≤ k) :
-    compileClauseBounded k c = compileClause c := by
-  rw [compileClauseBounded, List.take_of_length_le hc]
-
-theorem compileParityRowBounded_eq_compileParityRow {k : ℕ} {φ : CNF ℕ}
-    (hφ : ∀ c ∈ φ, c.length ≤ k) (row : List Bool) :
-    compileParityRowBounded k φ row = compileParityRow φ row := by
-  rw [compileParityRowBounded,
-    (List.map_congr_left fun c hc => List.take_of_length_le (hφ c hc)).trans (List.map_id φ)]
-
 theorem compileParitySystemBounded_eq_compileParitySystem {k : ℕ} {φ : CNF ℕ}
     (hφ : ∀ c ∈ φ, c.length ≤ k) (rows : List (List Bool)) :
     compileParitySystemBounded k φ rows = compileParitySystem φ rows := by
@@ -839,16 +829,6 @@ theorem exists_sublist_of_mem_restrictEquation {v : ℕ} {val : Bool} {eq : List
     obtain ⟨m, hm, rfl⟩ := List.mem_map.mp (mem_of_mem_reduceEquation hm')
     exact ⟨m, hm, List.filter_sublist⟩
 
-theorem isCanonicalEquation_restrictEquation {v : ℕ} {val : Bool} {eq : List (List ℕ)}
-    (heq : IsCanonicalEquation eq) : IsCanonicalEquation (restrictEquation v val eq) := by
-  unfold restrictEquation; cases val
-  · simp only [Bool.false_eq_true, ↓reduceIte]
-    exact ⟨heq.1.filter _, fun m hm => heq.2 m (List.mem_filter.mp hm).1⟩
-  · simp only [↓reduceIte]
-    refine ⟨nodup_reduceEquation _, fun m' hm' => ?_⟩
-    obtain ⟨m, hm, rfl⟩ := List.mem_map.mp (mem_of_mem_reduceEquation hm')
-    exact (heq.2 m hm).filter _
-
 /-- `restrictEquation` preserves any monomial degree bound `≤ k`. -/
 theorem length_mem_restrictEquation_le {k v : ℕ} {val : Bool} {eq : List (List ℕ)}
     (hdeg : ∀ m ∈ eq, m.length ≤ k) {m' : List ℕ} (hm' : m' ∈ restrictEquation v val eq) :
@@ -875,32 +855,6 @@ theorem not_mem_of_mem_restrictEquation {v : ℕ} {val : Bool} {eq : List (List
     obtain ⟨m, -, rfl⟩ := List.mem_map.mp (mem_of_mem_reduceEquation hm')
     exact fun hvm => absurd rfl (of_decide_eq_true (List.mem_filter.mp hvm).2)
 
-theorem varDegree_restrictSystem_self (v : ℕ) (val : Bool) (sys : List (List (List ℕ))) :
-    varDegree v (restrictSystem v val sys) = 0 := by
-  rw [varDegree, List.countP_eq_zero]
-  intro eq' heq'
-  obtain ⟨eq, -, rfl⟩ := List.mem_map.mp heq'
-  simp only [Bool.not_eq_true, decide_eq_false_iff_not, mem_equationVars, not_exists, not_and]
-  exact fun _ hm' => not_mem_of_mem_restrictEquation hm'
-
-theorem varDegree_restrictSystem_le (u v : ℕ) (val : Bool) (sys : List (List (List ℕ))) :
-    varDegree u (restrictSystem v val sys) ≤ varDegree u sys := by
-  unfold varDegree restrictSystem
-  induction sys with
-  | nil => simp only [List.map_nil, le_rfl]
-  | cons eq sys ih =>
-    rw [List.map_cons, List.countP_cons, List.countP_cons]
-    refine Nat.add_le_add ih ?_
-    split_ifs with h1 h2
-    · exact le_rfl
-    · exfalso
-      rw [decide_eq_true_iff, mem_equationVars] at h1 h2
-      obtain ⟨m', hm', hum'⟩ := h1
-      obtain ⟨m, hm, hsub⟩ := exists_sublist_of_mem_restrictEquation hm'
-      exact h2 ⟨m, hm, hsub.subset hum'⟩
-    · exact Nat.zero_le _
-    · exact le_rfl
-
 /-- **Exact variable-restriction semantics (§5.5, p. 38)**: evaluating `restrictEquation v val eq`
 on `σ` agrees with evaluating `eq` on `Function.update σ v val`. -/
 theorem evalMonomialList_restrictEquation (v : ℕ) (val : Bool) (eq : List (List ℕ))
@@ -941,12 +895,6 @@ theorem evalMonomialList_restrictEquation (v : ℕ) (val : Bool) (eq : List (Lis
       · obtain ⟨hum, huv⟩ := List.mem_filter.mp hu
         simpa only [Function.update_of_ne (of_decide_eq_true huv)] using h u hum
 
-theorem evalSystem_restrictSystem (v : ℕ) (val : Bool) (sys : List (List (List ℕ)))
-    (σ : ℕ → Bool) :
-    evalSystem (restrictSystem v val sys) σ = evalSystem sys (Function.update σ v val) := by
-  simp only [evalSystem, restrictSystem, List.all_map, Function.comp_def,
-    evalMonomialList_restrictEquation]
-
 /-! ### 4. Polynomial-Time Complexity Proofs (Plain `ComputableInPolyTime`) -/
 
 section PolyTime
diff --git a/Complexity/Foundations/BooleanAnalysis/SparseBranching.lean b/Complexity/Foundations/BooleanAnalysis/SparseBranching.lean
index 85fcaee65..00b16e892 100644
--- a/Complexity/Foundations/BooleanAnalysis/SparseBranching.lean
+++ b/Complexity/Foundations/BooleanAnalysis/SparseBranching.lean
@@ -131,20 +131,6 @@ def univariateMonomialSumPoly (R : Type*) [CommSemiring R] (q : ι → Polynomia
     (𝓜 : Finset (Finset ι)) : Polynomial R :=
   ∑ M ∈ 𝓜, univariateMonomialPoly R q M
 
-/-- `univariateMonomialPoly R q M` agrees with evaluating `monomialPoly R M` at `q`. -/
-theorem univariateMonomialPoly_eq_eval₂ [CommSemiring R] (q : ι → Polynomial R) (M : Finset ι) :
-    univariateMonomialPoly R q M = (monomialPoly R M).eval₂ Polynomial.C q := by
-  rw [univariateMonomialPoly, monomialPoly, MvPolynomial.eval₂_prod]
-  refine prod_congr rfl fun v _ => ?_
-  rw [MvPolynomial.eval₂_X]
-
-/-- `univariateMonomialSumPoly R q 𝓜` agrees with evaluating `monomialSumPoly R 𝓜` at `q`. -/
-theorem univariateMonomialSumPoly_eq_eval₂ [CommSemiring R] (q : ι → Polynomial R)
-    (𝓜 : Finset (Finset ι)) :
-    univariateMonomialSumPoly R q 𝓜 = (monomialSumPoly R 𝓜).eval₂ Polynomial.C q := by
-  rw [univariateMonomialSumPoly, monomialSumPoly, MvPolynomial.eval₂_sum]
-  exact sum_congr rfl fun M _ => univariateMonomialPoly_eq_eval₂ q M
-
 /-- Pointwise evaluation of `univariateMonomialPoly R q M` at `t : R`. -/
 theorem eval_univariateMonomialPoly [CommSemiring R] (q : ι → Polynomial R) (M : Finset ι)
     (t : R) :
@@ -461,15 +447,6 @@ theorem monomialSum_relabelRestrictedMonomials [Fintype ι] [DecidableEq ι] [De
     (fun x _ => ?_)
   simp only [extendFreeAssignment, x.2, ↓reduceDIte]
 
-/-- Over `ZMod 2`, evaluating `relabelRestrictedMonomials S e b 𝓜` at `y : ι' → Bool` equals
-evaluating the original equation `𝓜` at `patchAssignment S b (extendFreeAssignment S e y)`. -/
-theorem monomialSum_zmod_two_relabelRestrictedMonomials [Fintype ι] [DecidableEq ι]
-    [DecidableEq ι'] (S : Finset ι) (e : ↥(univ \ S) ≃ ι') (b : ι → Bool)
-    (𝓜 : Finset (Finset ι)) (y : ι' → Bool) :
-    monomialSum (ZMod 2) (relabelRestrictedMonomials S e b 𝓜) y =
-      monomialSum (ZMod 2) 𝓜 (patchAssignment S b (extendFreeAssignment S e y)) := by
-  rw [monomialSum_relabelRestrictedMonomials, monomialSum_zmod_two_restrictMonomials]
-
 /-- **§5.5–5.6 (Theorem 2.2 additive branch decomposition on the relabeled free-variable cube
 `ι' → Bool`)**: for any branch variable set `S` and equivalence `e : ↥(univ \ S) ≃ ι'`, the
 common-zero count `commonZeroCount I P` equals the sum over `b ∈ branchAssignments S` of
@@ -710,41 +687,6 @@ unrestricted system on `n` variables and every free-variable branch. -/
 def branchPrecision (n : ℕ) : ℕ :=
   n + 1
 
-/-- The branch precision `branchPrecision n` is always at least `1`. -/
-theorem one_le_branchPrecision (n : ℕ) : 1 ≤ branchPrecision n :=
-  Nat.succ_pos n
-
-/-- Strict inequality `2 ^ n < 2 ^ branchPrecision n`. -/
-theorem two_pow_lt_two_pow_branchPrecision (n : ℕ) :
-    2 ^ n < 2 ^ branchPrecision n :=
-  Nat.pow_lt_pow_right (by decide) (Nat.lt_succ_self n)
-
-/-- **§5.1 ($N(\mathcal{P}) < 2^\ell$)**: the common-zero count on `ι` is strictly smaller than
-`2 ^ branchPrecision (Fintype.card ι)`. -/
-theorem commonZeroCount_lt_two_pow_branchPrecision [Fintype ι] [DecidableEq ι] (I : Finset κ)
-    (P : κ → Finset (Finset ι)) :
-    commonZeroCount I P < 2 ^ branchPrecision (Fintype.card ι) :=
-  lt_of_le_of_lt (commonZeroCount_le_two_pow I P)
-    (two_pow_lt_two_pow_branchPrecision (Fintype.card ι))
-
-/-- **§5.5 (branch count $< 2^\ell$ at original precision $\ell = n + 1$)**: for any subset `S`
-and branch assignment `b : ι → Bool`, the relabeled branch common-zero count on `ι'` is strictly
-smaller than `2 ^ branchPrecision (Fintype.card ι)` whenever `e : ↥(univ \ S) ≃ ι'`. -/
-theorem commonZeroCount_relabelRestrictedMonomials_lt_two_pow_branchPrecision [Fintype ι]
-    [Fintype ι'] [DecidableEq ι] [DecidableEq ι'] (S : Finset ι) (e : ↥(univ \ S) ≃ ι')
-    (I : Finset κ) (P : κ → Finset (Finset ι)) (b : ι → Bool) :
-    commonZeroCount I (fun i => relabelRestrictedMonomials S e b (P i)) <
-      2 ^ branchPrecision (Fintype.card ι) := by
-  have hcard : Fintype.card ι' ≤ Fintype.card ι := by
-    rw [← Fintype.card_congr e, Fintype.card_coe]
-    exact card_le_univ (univ \ S)
-  calc
-    commonZeroCount I (fun i => relabelRestrictedMonomials S e b (P i))
-      ≤ 2 ^ Fintype.card ι' := commonZeroCount_le_two_pow _ _
-    _ ≤ 2 ^ Fintype.card ι := Nat.pow_le_pow_right (by decide) hcard
-    _ < 2 ^ branchPrecision (Fintype.card ι) :=
-      two_pow_lt_two_pow_branchPrecision (Fintype.card ι)
-
 /-- **§5.5 (exact branch recovery at original precision $\ell = n + 1$)**: on any branch `(S, b)`
 relabeled along `e : ↥(univ \ S) ≃ ι'`, evaluating `univariateParityTruncatedSum` at `T = 0` with
 the original precision `branchPrecision (Fintype.card ι) = n + 1` and taking the remainder modulo
diff --git a/Complexity/Foundations/BooleanAnalysis/SparseClearedSpecialization.lean b/Complexity/Foundations/BooleanAnalysis/SparseClearedSpecialization.lean
index 1abdd4fff..639d46ede 100644
--- a/Complexity/Foundations/BooleanAnalysis/SparseClearedSpecialization.lean
+++ b/Complexity/Foundations/BooleanAnalysis/SparseClearedSpecialization.lean
@@ -146,15 +146,6 @@ theorem eval_coeff_prod_parityFactorCleared [CommRing R] (I : Finset κ) (ℓ :
   refine congrArg (fun Q : Polynomial R => Q.coeff s) (prod_congr rfl fun i _ => ?_)
   exact map_parityFactorCleared φ ℓ Δ (A_i i)
 
-/-- Evaluating `sumCoeffsBelow m` of `∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i)` at `t : R` agrees
-with `sumCoeffsBelow m` of `∏ i ∈ I, parityFactorCleared ℓ (Δ.eval t) ((A_i i).eval t)`. -/
-theorem eval_sumCoeffsBelow_prod_parityFactorCleared [CommRing R] (I : Finset κ) (ℓ : ℕ)
-    (Δ : Polynomial R) (A_i : κ → Polynomial R) (m : ℕ) (t : R) :
-    ((∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i)).sumCoeffsBelow m).eval t =
-      (∏ i ∈ I, parityFactorCleared ℓ (Δ.eval t) ((A_i i).eval t)).sumCoeffsBelow m := by
-  rw [Polynomial.sumCoeffsBelow, Polynomial.eval_finsetSum, Polynomial.sumCoeffsBelow]
-  exact sum_congr rfl fun s _ => eval_coeff_prod_parityFactorCleared I ℓ Δ A_i s t
-
 /-- When `Δ` has `natDegree = 0` and `A_i` has `natDegree ≤ d`, `parityBaseDigitCleared ℓ j Δ A_i`
 has `natDegree ≤ d`. -/
 theorem natDegree_parityBaseDigitCleared_le [CommRing R] (ℓ j : ℕ) (Δ A_i : Polynomial R)
@@ -258,20 +249,6 @@ theorem natDegree_coeff_prod_parityFactorCleared_le_of_lt [CommRing R] (I : Fins
   refine (natDegree_coeff_prod_parityFactorCleared_le I ℓ Δ A_i hΔ hA s).trans ?_
   exact Nat.mul_le_mul_left d (by omega)
 
-/-- The truncated sum `sumCoeffsBelow ℓ (∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i))` has
-`natDegree ≤ d * (#I + 2 * (ℓ - 1))`. -/
-theorem natDegree_sumCoeffsBelow_prod_parityFactorCleared_le [CommRing R] (I : Finset κ)
-    (ℓ : ℕ) (Δ : Polynomial R) (A_i : κ → Polynomial R) {d : ℕ} (hΔ : Δ.natDegree = 0)
-    (hA : ∀ i ∈ I, (A_i i).natDegree ≤ d) :
-    ((∏ i ∈ I, parityFactorCleared ℓ Δ (A_i i)).sumCoeffsBelow ℓ).natDegree ≤
-      d * (#I + 2 * (ℓ - 1)) := by
-  rw [Polynomial.sumCoeffsBelow]
-  refine (Polynomial.natDegree_sum_le _ _).trans ?_
-  rw [Finset.fold_max_le]
-  refine ⟨Nat.zero_le _, fun s hs => ?_⟩
-  rw [mem_range] at hs
-  exact natDegree_coeff_prod_parityFactorCleared_le_of_lt I Δ A_i hΔ hA hs
-
 /-! ### 2. Cleared-denominator monomials and equations: $T = 0$ evaluation, ring homogenization,
 and `natDegree` bounds (§5.3–5.4 & Appendix B.2) -/
 
@@ -414,17 +391,6 @@ theorem univariateClearedParityTruncatedSum_eq_sum_coord [Fintype ι] [Decidable
       ∑ s ∈ range ℓ, univariateClearedParityCoord I P d_den k ℓ θ s :=
   rfl
 
-/-- Explicit cube-sum expansion of `univariateClearedParityTruncatedSum`. -/
-theorem univariateClearedParityTruncatedSum_eq_sum [Fintype ι] [DecidableEq ι] (I : Finset κ)
-    (P : κ → Finset (Finset ι)) (d_den : ℤ) (k ℓ : ℕ)
-    (θ : (ι → Bool) → κ → ι → Polynomial ℤ) :
-    univariateClearedParityTruncatedSum I P d_den k ℓ θ =
-      ∑ x : ι → Bool,
-        (∏ i ∈ I,
-          parityFactorCleared ℓ (Polynomial.C (d_den ^ k))
-            (clearedMonomialSumPoly d_den k (θ x i) (P i))).sumCoeffsBelow ℓ := by
-  rw [univariateClearedParityTruncatedSum, univariateClearedParityProduct, sumCoeffsBelow_sum]
-
 /-- **Equation (5.5a) (cleared-denominator coordinate `natDegree` bound)**: for `s < ℓ`, if every
 equation `P i` (`i ∈ I`) has degree at most `k` and every numerator `θ x i v` has
 `natDegree ≤ R_deg`, then `univariateClearedParityCoord I P d_den k ℓ θ s` has
@@ -531,19 +497,6 @@ theorem C_mul_divDenomReplacement {K : Type*} [Field K] {d_den : ℤ} (hd : (d_d
   rw [divDenomReplacement, ← mul_assoc, ← Polynomial.C_mul, mul_inv_cancel₀ hd, Polynomial.C_1,
     one_mul]
 
-/-- At `T = 0`, if `(d_den : K) ≠ 0` and `(θ x i v).eval 0 = d_den * bitVal ℤ (x v)`, then
-`divDenomReplacement K d_den θ x i v` restores `bitVal K (x v)`. -/
-theorem eval_zero_divDenomReplacement {K : Type*} [Field K] {d_den : ℤ} (hd : (d_den : K) ≠ 0)
-    (θ : (ι → Bool) → κ → ι → Polynomial ℤ) {x : ι → Bool} {i : κ} {v : ι}
-    (hθ : (θ x i v).eval 0 = d_den * bitVal ℤ (x v)) :
-    (divDenomReplacement K d_den θ x i v).eval 0 = bitVal K (x v) := by
-  rw [divDenomReplacement, Polynomial.eval_mul, Polynomial.eval_C]
-  have h0 : (0 : K) = Int.castRingHom K 0 := by rw [map_zero]
-  have hbit : (bitVal ℤ (x v) : K) = bitVal K (x v) := by
-    cases x v <;> simp only [bitVal_true, bitVal_false, Int.cast_one, Int.cast_zero]
-  rw [h0, Polynomial.eval_map_apply, eq_intCast, hθ, Int.cast_mul, hbit, ← mul_assoc,
-    inv_mul_cancel₀ hd, one_mul]
-
 /-- **§5.4 & Appendix B.3 ($\tilde{H}_s(T) = \Omega [V^s] H(T)$ over a field $K$)**: when
 `(d_den : K) ≠ 0`, `1 ≤ ℓ`, and `∀ i ∈ I, ∀ M ∈ P i, #M ≤ k`, mapping
 `univariateClearedParityCoord I P d_den k ℓ θ s` into `K[T]` equals
diff --git a/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean b/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean
index 6f1f9bcfa..d9daca94e 100644
--- a/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean
+++ b/Complexity/Foundations/BooleanAnalysis/SparseEquations.lean
@@ -52,8 +52,7 @@ Finally, for any system of equations with variable scopes `scope : κ → Finset
 candidate variable set `V` (`∀ i ∈ F, scope i ⊆ V`) and positive incidence threshold `1 ≤ b₀`,
 the set `Cslib.BitString.heavyVars V F scope b₀` of variables in `V` appearing in more than `b₀`
 scopes has cardinality at most `totalIncidence F scope / b₀`
-(`Cslib.BitString.card_heavyVars_le_div`; and at most `(k_scope * #F) / b₀` when every scope has
-cardinality at most `k_scope`, `Cslib.BitString.card_heavyVars_le_mul_card_div`), while every
+(`Cslib.BitString.card_heavyVars_le_div`), while every
 remaining variable in `V \ heavyVars V F scope b₀` (and in any post-branching restricted equation
 scope when `∀ i ∈ I, equationScope (P i) ⊆ V`) has incidence at most `b₀`. Branching on all
 `2 ^ #S` assignments to a variable subset `S` and simplifying each equation via
@@ -139,29 +138,6 @@ theorem monomialSum_eq_card_filter (R : Type*) [CommRing R] (𝓜 : Finset (Fins
   unfold monomialSum
   simp only [monomial_apply, sum_boole]
 
-/-- If every monomial in `𝓜` has size at most `k`, then `monomialSum R 𝓜` has degree at most `k`
-on the Boolean cube. -/
-theorem monomialSum_mem_lowDegree (R : Type*) [CommRing R] {𝓜 : Finset (Finset ι)} {k : ℕ}
-    (hk : ∀ M ∈ 𝓜, #M ≤ k) :
-    monomialSum R 𝓜 ∈ lowDegree R ι k := by
-  have hEq : monomialSum R 𝓜 = ∑ M ∈ 𝓜, monomial R M := by
-    funext x
-    simp only [monomialSum, Finset.sum_apply]
-  rw [hEq]
-  exact sum_mem_lowDegree 𝓜 fun M hM => monomial_mem_lowDegree (hk M hM)
-
-/-- Over `ℤ`, `monomialSum ℤ 𝓜 x` is nonnegative. -/
-theorem monomialSum_int_nonneg (𝓜 : Finset (Finset ι)) (x : ι → Bool) :
-    0 ≤ monomialSum ℤ 𝓜 x := by
-  rw [monomialSum_eq_card_filter]
-  exact Nat.cast_nonneg _
-
-/-- Over `ℤ`, `monomialSum ℤ 𝓜 x` is at most `#𝓜`. -/
-theorem monomialSum_int_le_card (𝓜 : Finset (Finset ι)) (x : ι → Bool) :
-    monomialSum ℤ 𝓜 x ≤ #𝓜 := by
-  rw [monomialSum_eq_card_filter]
-  exact Nat.cast_le.mpr (card_filter_le _ _)
-
 /-- A monomial sum vanishes in `ZMod 2` at `x` if and only if its integer lift `monomialSum ℤ 𝓜 x`
 is even. -/
 theorem monomialSum_zmod_two_eq_zero_iff_even (𝓜 : Finset (Finset ι)) (x : ι → Bool) :
@@ -273,33 +249,6 @@ theorem eval₂_monomialPoly {S : Type*} [CommSemiring R] [CommSemiring S] (f :
   refine prod_congr rfl fun v _ => ?_
   simp only [coe_eval₂Hom, eval₂_X]
 
-/-- Evaluating `monomialSumPoly R 𝓜` via `eval₂ f q` gives `∑ M ∈ 𝓜, ∏ v ∈ M, q v`. -/
-theorem eval₂_monomialSumPoly {S : Type*} [CommSemiring R] [CommSemiring S] (f : R →+* S)
-    (q : ι → S) (𝓜 : Finset (Finset ι)) :
-    (monomialSumPoly R 𝓜).eval₂ f q = ∑ M ∈ 𝓜, ∏ v ∈ M, q v := by
-  unfold monomialSumPoly
-  rw [← coe_eval₂Hom, map_sum]
-  refine sum_congr rfl fun M _ => ?_
-  rw [coe_eval₂Hom, eval₂_monomialPoly]
-
-/-- `monomialPoly R M` has total degree at most `#M`. -/
-theorem totalDegree_monomialPoly_le (R : Type*) [CommSemiring R] (M : Finset ι) :
-    (monomialPoly R M).totalDegree ≤ #M := by
-  unfold monomialPoly
-  refine (totalDegree_finsetProd M _).trans ?_
-  refine (sum_le_card_nsmul M _ 1 fun v _ => ?_).trans ?_
-  · exact (totalDegree_monomial_le _ _).trans (by simp)
-  · simp only [smul_eq_mul, mul_one, le_rfl]
-
-/-- If every monomial `M ∈ 𝓜` has size at most `k`, then `monomialSumPoly R 𝓜` has total degree
-at most `k`. -/
-theorem totalDegree_monomialSumPoly_le (R : Type*) [CommSemiring R] {𝓜 : Finset (Finset ι)}
-    {k : ℕ} (hk : ∀ M ∈ 𝓜, #M ≤ k) :
-    (monomialSumPoly R 𝓜).totalDegree ≤ k := by
-  unfold monomialSumPoly
-  refine (totalDegree_finsetSum 𝓜 _).trans (Finset.sup_le fun M hM => ?_)
-  exact (totalDegree_monomialPoly_le R M).trans (hk M hM)
-
 /-- Substituting polynomials `q v` of total degree at most `d₀` into `monomialPoly R M` produces a
 polynomial of total degree at most `#M * d₀`. -/
 theorem totalDegree_eval₂_monomialPoly_le [CommSemiring R] (f : R →+* MvPolynomial σ R)
@@ -327,20 +276,6 @@ theorem totalDegree_eval₂_monomialSumPoly_le [CommSemiring R] (f : R →+* MvP
 
 /-! ### 3. Truncated parity-factor degree bound (eq. 5.5) and count recovery (eq. 5.4) -/
 
-/-- **Equation (5.5) (retained coefficient degree bound under variable replacement)**: if every
-equation `P i` (`i ∈ I`) has degree at most `k` and each variable is replaced by a polynomial
-`q i v` of total degree at most `d₀`, then for `s < ℓ` the `V ^ s`-coefficient of the product of
-parity factors has total degree at most `(k * d₀) * (#I + 2 * (ℓ - 1))`. -/
-theorem totalDegree_coeff_prod_parityFactor_eval₂_le_of_lt [CommRing R] (I : Finset κ)
-    {P : κ → Finset (Finset ι)} {ℓ s k d₀ : ℕ} (hs : s < ℓ)
-    (f : R →+* MvPolynomial σ R) (q : κ → ι → MvPolynomial σ R)
-    (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k)
-    (hq : ∀ i ∈ I, ∀ M ∈ P i, ∀ v ∈ M, (q i v).totalDegree ≤ d₀) :
-    ((∏ i ∈ I, Polynomial.parityFactor ℓ ((monomialSumPoly R (P i)).eval₂ f (q i))).coeff
-      s).totalDegree ≤ (k * d₀) * (#I + 2 * (ℓ - 1)) :=
-  Polynomial.totalDegree_coeff_prod_parityFactor_le_of_lt I hs fun i hi =>
-    totalDegree_eval₂_monomialSumPoly_le f (q i) (hk i hi) (hq i hi)
-
 /-- **Equation (5.5) (truncated product degree bound under variable replacement)**: under the same
 hypotheses, the truncated sum `S_ℓ(∏ i ∈ I, B_i(V))` has total degree at most
 `(k * d₀) * (#I + 2 * (ℓ - 1))`. -/
@@ -466,15 +401,6 @@ theorem card_heavyVars_le_div [DecidableEq ι] (U : Finset ι) (F : Finset κ)
     #(heavyVars U F scope b₀) ≤ totalIncidence F scope / b₀ :=
   (Nat.le_div_iff_mul_le hb₀).mpr (card_heavyVars_mul_le_totalIncidence U F scope b₀ hU)
 
-/-- **§5.5 (heavy-variable bound for `k`-bounded scopes)**: if `b₀ > 0` and every scope has size at
-most `k`, then `#(heavyVars U F scope b₀) ≤ (k * #F) / b₀`. -/
-theorem card_heavyVars_le_mul_card_div [DecidableEq ι] (U : Finset ι) (F : Finset κ)
-    (scope : κ → Finset ι) {k b₀ : ℕ} (hb₀ : 0 < b₀) (hU : ∀ i ∈ F, scope i ⊆ U)
-    (hk : ∀ i ∈ F, #(scope i) ≤ k) :
-    #(heavyVars U F scope b₀) ≤ (k * #F) / b₀ :=
-  (card_heavyVars_le_div U F scope hb₀ hU).trans
-    (Nat.div_le_div_right (totalIncidence_le_mul_card F scope hk))
-
 /-- Every variable in `U \ heavyVars U F scope b₀` has incidence at most `b₀`. -/
 theorem varIncidence_le_of_mem_sdiff_heavyVars [DecidableEq ι] {U : Finset ι} {F : Finset κ}
     {scope : κ → Finset ι} {b₀ : ℕ} {v : ι} (hv : v ∈ U \ heavyVars U F scope b₀) :
diff --git a/Complexity/Foundations/BooleanAnalysis/SparseHermiteRecovery.lean b/Complexity/Foundations/BooleanAnalysis/SparseHermiteRecovery.lean
index bfd62dfa3..a342bbe21 100644
--- a/Complexity/Foundations/BooleanAnalysis/SparseHermiteRecovery.lean
+++ b/Complexity/Foundations/BooleanAnalysis/SparseHermiteRecovery.lean
@@ -333,24 +333,6 @@ theorem taylor_clearedMonomialSumPoly (t d_den : ℤ) (k : ℕ) (θ : ι → Pol
   rw [map_sum]
   exact sum_congr rfl fun M _ => taylor_clearedMonomialPoly t d_den k θ M
 
-/-- `Polynomial.taylor t` commutes with `parityBaseDigitCleared` when `Δ` is a scalar constant. -/
-theorem taylor_parityBaseDigitCleared {R : Type*} [CommRing R] (t Δ : R) (ℓ j : ℕ)
-    (A_i : Polynomial R) :
-    Polynomial.taylor t (parityBaseDigitCleared ℓ j (Polynomial.C Δ) A_i) =
-      parityBaseDigitCleared ℓ j (Polynomial.C Δ) (Polynomial.taylor t A_i) := by
-  have hhom :=
-    map_parityBaseDigitCleared (Polynomial.taylorAlgHom t).toRingHom ℓ j (Polynomial.C Δ) A_i
-  simpa only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Polynomial.taylorAlgHom_apply,
-    Polynomial.taylor_C] using hhom
-
-/-- `Polynomial.taylor t` commutes with `hPolyCleared` when `Δ` is a scalar constant. -/
-theorem taylor_hPolyCleared {R : Type*} [CommRing R] (t Δ : R) (A_i : Polynomial R) :
-    Polynomial.taylor t (hPolyCleared (Polynomial.C Δ) A_i) =
-      hPolyCleared (Polynomial.C Δ) (Polynomial.taylor t A_i) := by
-  have hhom := map_hPolyCleared (Polynomial.taylorAlgHom t).toRingHom (Polynomial.C Δ) A_i
-  simpa only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, Polynomial.taylorAlgHom_apply,
-    Polynomial.taylor_C] using hhom
-
 /-- Mapping `parityFactorCleared ℓ (Polynomial.C Δ) A_i` by `(Polynomial.taylorAlgHom t).toRingHom`
 shifts `A_i` by `Polynomial.taylor t`. -/
 theorem map_taylor_parityFactorCleared {R : Type*} [CommRing R] (t Δ : R) (ℓ : ℕ)
diff --git a/Complexity/Foundations/BooleanAnalysis/SparseReplacementDesign.lean b/Complexity/Foundations/BooleanAnalysis/SparseReplacementDesign.lean
index 708e6284a..dccd81847 100644
--- a/Complexity/Foundations/BooleanAnalysis/SparseReplacementDesign.lean
+++ b/Complexity/Foundations/BooleanAnalysis/SparseReplacementDesign.lean
@@ -71,8 +71,7 @@ Appendix B.2–B.3 cleared-denominator parity-polynomial zero-counting pipeline
      `natDegree_univariateClearedParityCoord_design_le`,
      `natDegree_univariateClearedParityTruncatedSum_design_le`),
    - the rational homogenization identity $\tilde{H}_s(T) = \Omega [V^s] H(T)$ over `ℚ[X]`
-     (`map_univariateClearedParityCoord_design`,
-     `map_univariateClearedParityTruncatedSum_design`),
+     (`map_univariateClearedParityCoord_design`),
    - the Appendix B.2 coordinate `ℓ₁`-norm bound
      (`coeffNorm1_univariateClearedParityCoord_design_le`),
    - exact integer division and modulo-`2 ^ ℓ` recovery of `commonZeroCount I P` when `n < ℓ` and
@@ -229,10 +228,6 @@ theorem designRowNormBound_pos (Q R : ℕ) : 0 < designRowNormBound Q R :=
 theorem commonDenom_intCast_ne_zero (Q R : ℕ) : (commonDenom Q R : ℤ) ≠ 0 :=
   Nat.cast_ne_zero.mpr (commonDenom_pos Q R).ne'
 
-/-- `(commonDenom Q R : ℚ) ≠ 0`. -/
-theorem commonDenom_ratCast_ne_zero (Q R : ℕ) : (commonDenom Q R : ℚ) ≠ 0 :=
-  Nat.cast_ne_zero.mpr (commonDenom_pos Q R).ne'
-
 /-- The univariate rational replacement polynomial `⟨P⃗_e(T), x⟩ ∈ ℚ[X]` for incidence
 `e : ScopeIncidence scope` and Boolean assignment `x : Fin n → Bool` (§5.3, p. 37). -/
 noncomputable def evalVarReplacementRowPoly {F : Type*} [Fintype F]
@@ -472,16 +467,6 @@ theorem map_designReplacementScaledIntMap {F : Type*} [Fintype F]
       simp only [bitVal_true, bitVal_false, Int.cast_one, Int.cast_zero, Polynomial.C_1,
         Polynomial.C_0, mul_one, mul_zero]
 
-/-- `divDenomReplacement ℚ (commonDenom Q R : ℤ) (designReplacementScaledIntMap D emb)` agrees
-with `designReplacementMap D emb`. -/
-theorem divDenomReplacement_designReplacementScaledIntMap {F : Type*} [Fintype F]
-    {scope : F → Finset (Fin n)} (D : ReplacementDesign scope Q r A₀ R τ) (emb : κ → F)
-    (x : Fin n → Bool) (i : κ) (v : Fin n) :
-    divDenomReplacement ℚ (commonDenom Q R : ℤ) (designReplacementScaledIntMap D emb) x i v =
-      designReplacementMap D emb x i v := by
-  rw [divDenomReplacement, map_designReplacementScaledIntMap, ← mul_assoc, ← Polynomial.C_mul,
-    Int.cast_natCast, inv_mul_cancel₀ (commonDenom_ratCast_ne_zero Q R), Polynomial.C_1, one_mul]
-
 /-- At `T = 0`, `designReplacementMap D emb x i v` evaluates to `bitVal ℚ (x v)`. -/
 theorem eval_zero_designReplacementMap {F : Type*} [Fintype F]
     {scope : F → Finset (Fin n)} (D : ReplacementDesign scope Q r A₀ R τ) (emb : κ → F)
@@ -610,24 +595,6 @@ theorem map_univariateClearedParityCoord_design {F : Type*} [Fintype F]
     (designReplacementScaledIntMap D emb) (designReplacementMap D emb) hk
     (fun x i _ _ _ v _ => map_designReplacementScaledIntMap D emb x i v) s
 
-/-- **§5.4 & Appendix B.3 ($S_\ell(\tilde{H}(T)) = \Omega S_\ell(H(T))$ over `ℚ[X]` for
-`ReplacementDesign`)**: under the same hypotheses, mapping
-`univariateClearedParityTruncatedSum I P (commonDenom Q R : ℤ) k ℓ
-  (designReplacementScaledIntMap D emb)` into `ℚ[X]` equals
-`C (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I : ℚ)` times
-`univariateParityTruncatedSum I P ℓ (designReplacementMap D emb)`. -/
-theorem map_univariateClearedParityTruncatedSum_design {F : Type*} [Fintype F]
-    {scope : F → Finset (Fin n)} (D : ReplacementDesign scope Q r A₀ R τ) (emb : κ → F)
-    (I : Finset κ) (P : κ → Finset (Finset (Fin n))) {k ℓ : ℕ} (hℓ : 1 ≤ ℓ)
-    (hk : ∀ i ∈ I, ∀ M ∈ P i, #M ≤ k) :
-    (univariateClearedParityTruncatedSum I P (commonDenom Q R : ℤ) k ℓ
-        (designReplacementScaledIntMap D emb)).map (Int.castRingHom ℚ) =
-      Polynomial.C (clearedProductDenom (commonDenom Q R : ℤ) k ℓ #I : ℚ) *
-        univariateParityTruncatedSum I P ℓ (designReplacementMap D emb) :=
-  map_univariateClearedParityTruncatedSum I P (commonDenom Q R : ℤ) hℓ
-    (designReplacementScaledIntMap D emb) (designReplacementMap D emb) hk
-    (fun x i _ _ _ v _ => map_designReplacementScaledIntMap D emb x i v)
-
 /-- **Appendix B.2 coordinate `ℓ₁`-norm bound for `ReplacementDesign`**:
 if `∀ i ∈ I, ∀ M ∈ P i, #M ≤ k`, `∀ i ∈ I, #(P i) ≤ S_mon`, and
 `∀ j < ℓ, (parityBaseDigit ℓ j).coeffNorm1 ≤ E_ℓ`, then every coordinate polynomial
diff --git a/Complexity/Logics/Propositional/CNF/SparseParityCounter.lean b/Complexity/Logics/Propositional/CNF/SparseParityCounter.lean
index 26171cec7..13373d87b 100644
--- a/Complexity/Logics/Propositional/CNF/SparseParityCounter.lean
+++ b/Complexity/Logics/Propositional/CNF/SparseParityCounter.lean
@@ -100,23 +100,6 @@ def CNF.parityRowSystem (φ : CNF V) (rows : List (Fin φ.length → Bool))
     (i : Fin rows.length) : Finset (Finset V) :=
   φ.parityRowMonomials (rows.get i)
 
-/-- Evaluating the `i`-th equation of `φ.parityRowSystem rows` over `ZMod 2` at `σ` equals the
-violation parity `bitVal (ZMod 2) (rows.get i ⬝ᵥ φ.violations σ)`. -/
-theorem CNF.monomialSum_parityRowSystem (φ : CNF V) (rows : List (Fin φ.length → Bool))
-    (i : Fin rows.length) (σ : V → Bool) :
-    monomialSum (ZMod 2) (φ.parityRowSystem rows i) σ =
-      bitVal (ZMod 2) (rows.get i ⬝ᵥ φ.violations σ) := by
-  rw [CNF.parityRowSystem, monomialSum, CNF.sum_parityRowMonomials]
-  rfl
-
-/-- The `i`-th equation of `φ.parityRowSystem rows` vanishes at `σ` over `ZMod 2` if and only if
-`rows.get i ⬝ᵥ φ.violations σ = false`. -/
-theorem CNF.monomialSum_parityRowSystem_eq_zero_iff (φ : CNF V)
-    (rows : List (Fin φ.length → Bool)) (i : Fin rows.length) (σ : V → Bool) :
-    monomialSum (ZMod 2) (φ.parityRowSystem rows i) σ = 0 ↔
-      rows.get i ⬝ᵥ φ.violations σ = false := by
-  rw [CNF.parityRowSystem, monomialSum, CNF.sum_parityRowMonomials_eq_zero_iff_dotProduct]
-
 /-- **§6 (eq. 6.1 common-zero equivalence)**: `σ : V → Bool` is a common zero of
 `φ.parityRowSystem rows` if and only if `PassesTests φ.violations rows σ`. -/
 theorem CNF.isCommonZero_parityRowSystem_iff (φ : CNF V)
@@ -130,23 +113,6 @@ theorem CNF.isCommonZero_parityRowSystem_iff (φ : CNF V)
   · intro h i _
     exact h (rows.get i) (List.get_mem rows i)
 
-/-- Every monomial in `φ.parityRowSystem rows i` is supported on `φ.vars.toFinset`. -/
-theorem CNF.mem_parityRowSystem_subset_vars (φ : CNF V)
-    (rows : List (Fin φ.length → Bool)) (i : Fin rows.length) {M : Finset V}
-    (hM : M ∈ φ.parityRowSystem rows i) :
-    M ⊆ φ.vars.toFinset :=
-  CNF.subset_vars_of_mem_parityRowMonomials hM
-
-/-- The variable scope `equationScope (φ.parityRowSystem rows i)` is contained in
-`φ.vars.toFinset`. -/
-theorem CNF.equationScope_parityRowSystem_subset_vars (φ : CNF V)
-    (rows : List (Fin φ.length → Bool)) (i : Fin rows.length) :
-    equationScope (φ.parityRowSystem rows i) ⊆ φ.vars.toFinset := by
-  intro v hv
-  rw [equationScope, mem_biUnion] at hv
-  rcases hv with ⟨M, hM, hvM⟩
-  exact CNF.mem_parityRowSystem_subset_vars φ rows i hM hvM
-
 /-- If every clause of `φ` has width at most `k`, then every monomial in
 `φ.parityRowSystem rows i` has size at most `k`. -/
 theorem CNF.card_mem_parityRowSystem_le {φ : CNF V} {k : ℕ} (hk : ∀ c ∈ φ, c.length ≤ k)