refactor(ETH): delete unused helper declarations in the sparse counting stack (#1361)

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`. -/

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`. -/

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 :=

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) :

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

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