diff --git a/Complexity.lean b/Complexity.lean
index e7fc4266a..e61d3017d 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -765,6 +765,7 @@ public import Complexity.Computability.Complexity.FineGrained.BruteForce
 public import Complexity.Computability.Complexity.FineGrained.CountingEndpoint
 public import Complexity.Computability.Complexity.FineGrained.CountingScale
 public import Complexity.Computability.Complexity.FineGrained.CountingSparsification
+public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound
 public import Complexity.Computability.Complexity.FineGrained.ExhaustiveSearch
 public import Complexity.Computability.Complexity.FineGrained.Exponents
 public import Complexity.Computability.Complexity.FineGrained.GraphProblems
@@ -2234,6 +2235,7 @@ public import Complexity.Logics.Propositional.ClauseSet.Basic
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Bounds
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.Counting
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingBounds
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingDeletion
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingInsertions
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingList
diff --git a/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean b/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean
new file mode 100644
index 000000000..ffa957035
--- /dev/null
+++ b/Complexity/Computability/Complexity/FineGrained/CountingTreeBound.lean
@@ -0,0 +1,277 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Complexity.Computability.Complexity.FineGrained.CountingSparsification
+public import Complexity.Computability.Complexity.FineGrained.ThreeOccurrenceReduction
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingBounds
+
+/-!
+# Discharging `CountingTreeBound` for Counting Sparsification
+
+We discharge the quantitative depth and leaf-count hypothesis `CountingSparsify.CountingTreeBound`
+of `CountingSparsification` from the actual path budgets and the leaf-only binomial-sum adaptation
+in `CountingBounds` and the first-success threshold base `countingThresholdBase` in
+`CountingParameters` (adapting Appendix A.2, Lemma A.3 on p. 46 and Appendix A.3 on pp. 46–47 of
+[OpenAI2026ETH]).
+
+Specifically:
+* For any parameters `M, K, B : ℕ` with `2 ≤ M`, `1 ≤ K`, and `1 ≤ B` satisfying the integer
+  parameter budget `countingBChoiceCoeff K ≤ M` and
+  `B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M` whenever `2 ≤ K`,
+  `CountingSparsify.countingTreeBound_of_budget` proves
+  `CountingSparsify.CountingTreeBound M K B (countingDepthCoeff K M) hM hK`.
+* Instantiating `M = countingThresholdBase K B` via `countingThresholdBase_spec`,
+  `CountingSparsify.countingTreeBound_countingThresholdBase` proves `CountingTreeBound`
+  unconditionally for every `1 ≤ K` and `1 ≤ B`.
+
+We then specialize the correctness and native `ComputableInO` transfer theorems of
+`CountingSparsification` and `ThreeOccurrenceReduction` both for any budget-satisfying `M` and
+unconditionally at `M = countingThresholdBase K B`.
+
+## Main results
+
+* `Cslib.Complexity.CountingSparsify.countingTreeBound_of_budget`,
+  `Cslib.Complexity.CountingSparsify.countingTreeBound_countingThresholdBase`: discharge
+  `CountingTreeBound` with linear depth coefficient `countingDepthCoeff K M` from the integer
+  parameter budget and unconditionally at `M = countingThresholdBase K B`.
+* `Cslib.Complexity.CountingSparsify.search_eq_ite_modelCount_of_budget`,
+  `Cslib.Complexity.CountingSparsify.search_eq_modelCount_of_budget`,
+  `Cslib.Complexity.CountingSparsify.search_eq_modelCount_countingThresholdBase`: model-count
+  correctness of `CountingSparsify.search` without an external `CountingTreeBound` witness.
+* `Cslib.Complexity.CountingSparsify.exists_computableInO_search_of_budget`,
+  `Cslib.Complexity.CountingSparsify.exists_computableInO_search_countingThresholdBase`: native
+  `ComputableInO ... T T` time-and-space transfer certificates for `CountingSparsify.search`.
+* `Cslib.Complexity.CountingSparsify.exists_computableInO_search_threeOccurrence_promise_of_budget`,
+  `Cslib.Complexity.CountingSparsify.exists_computableInO_search_threeOccurrence_of_budget`,
+  `Cslib.Complexity.CountingSparsify.exists_computableInO_search_threeOccurrence_thresholdBase`:
+  end-to-end counting-sparsification reduction from a dense occurrence-`≤ 3` model counter.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*, Section 6.4 (pp. 43–44),
+  Appendix A.2 (Lemma A.3, p. 46), and Appendix A.3 (pp. 46–47)][OpenAI2026ETH]
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Cslib.Logic.PL.ClauseSet.Sparsification
+open Turing.MultiTapeTM
+
+namespace CountingSparsify
+
+variable {M K : ℕ} (hM : 1 ≤ M) (hK : 1 ≤ K)
+
+include hM hK in
+/-- **Discharging `CountingTreeBound` from the integer parameter budget.**
+For `2 ≤ M`, `1 ≤ K`, and `1 ≤ B`, if `2 ≤ K` implies `countingBChoiceCoeff K ≤ M` and
+`B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M`, then
+`CountingTreeBound M K B (countingDepthCoeff K M) hM hK` holds (adapting the §A.3 node bound on
+printed pp. 46–47 of [OpenAI2026ETH] via the leaf-only B-position injection of
+`CountingBounds`). -/
+theorem countingTreeBound_of_budget (hM2 : 2 ≤ M) {B : ℕ} (hB : 1 ≤ B)
+    (hbudget : 2 ≤ K → countingBChoiceCoeff K ≤ M ∧
+      B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M) :
+    CountingTreeBound M K B (countingDepthCoeff K M) hM hK := by
+  intro ψ declared hsupport
+  have hnt : ∀ C ∈ ψ.1.toClauseSet, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by
+    intro C' hC' l hl hneg
+    obtain ⟨C, hC, rfl⟩ := mem_toClauseSet.mp hC'
+    exact ψ.2.nontautological C hC l (List.mem_toFinset.mp hl) (List.mem_toFinset.mp hneg)
+  have hsup : ∀ C ∈ ψ.1.toClauseSet, ∀ l ∈ C, l.1 ∈ declared := by
+    intro C' hC' l hl
+    obtain ⟨C, hC, rfl⟩ := mem_toClauseSet.mp hC'
+    exact hsupport C hC l (List.mem_toFinset.mp hl)
+  refine ⟨fun w hw => ?_, fun W hW => ?_⟩
+  · exact CountingBranchingRule.IsLeafWord.length_le (R := rule hM hK) hM2 ψ.2.reduced
+      hnt ψ.2.card_le declared hsup hw
+  · exact CountingBranchingRule.card_le_two_pow_of_isLeafWord (R := rule hM hK) hM2
+      ψ.2.reduced hnt ψ.2.card_le declared hsup hB hbudget W hW
+
+include hK in
+/-- **Unconditional `CountingTreeBound` at `countingThresholdBase K B`.**
+For any `1 ≤ K` and `1 ≤ B`, the first-success dyadic base `countingThresholdBase K B` satisfies
+`CountingTreeBound` with linear depth coefficient
+`countingDepthCoeff K (countingThresholdBase K B)`. -/
+theorem countingTreeBound_countingThresholdBase {B : ℕ} (hB : 1 ≤ B) :
+    CountingTreeBound (countingThresholdBase K B) K B
+      (countingDepthCoeff K (countingThresholdBase K B))
+      ((by decide : 1 ≤ 2).trans (two_le_countingThresholdBase K B)) hK :=
+  countingTreeBound_of_budget _ hK (two_le_countingThresholdBase K B) hB
+    fun hk2 => countingThresholdBase_spec hk2 hB
+
+include hM hK in
+/-- **Model-count correctness of `search` under the integer parameter budget.**
+If `g` computes `ψ.modelCount` on sparse formulas `ψ` of width at most `k`, then
+`search M K k B g φ` returns `φ.modelCount` on formulas of width at most `k` and `0` otherwise. -/
+theorem search_eq_ite_modelCount_of_budget (hM2 : 2 ≤ M) {k B : ℕ} (hkK : k ≤ K) (hB : 1 ≤ B)
+    (hbudget : 2 ≤ K → countingBChoiceCoeff K ≤ M ∧
+      B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M)
+    {g : CNF ℕ → ℕ}
+    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold M) K ψ = true → g ψ = ψ.modelCount)
+    (φ : CNF ℕ) :
+    search M K k B g φ =
+      if (φ.all fun c => decide (c.length ≤ k)) then φ.modelCount else 0 :=
+  search_eq_ite_modelCount hM hK hM2 hkK (countingTreeBound_of_budget hM hK hM2 hB hbudget) hg φ
+
+include hM hK in
+/-- **Model-count correctness of `search` on width-`≤ k` formulas under the integer parameter
+budget.** -/
+theorem search_eq_modelCount_of_budget (hM2 : 2 ≤ M) {k B : ℕ} (hkK : k ≤ K) (hB : 1 ≤ B)
+    (hbudget : 2 ≤ K → countingBChoiceCoeff K ≤ M ∧
+      B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M)
+    {g : CNF ℕ → ℕ}
+    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold M) K ψ = true → g ψ = ψ.modelCount)
+    {φ : CNF ℕ} (hφ : ∀ c ∈ φ, c.length ≤ k) :
+    search M K k B g φ = φ.modelCount :=
+  search_eq_modelCount hM hK hM2 hkK (countingTreeBound_of_budget hM hK hM2 hB hbudget) hg hφ
+
+include hK in
+/-- **Unconditional model-count correctness of `search` at `countingThresholdBase K B`.** -/
+theorem search_eq_modelCount_countingThresholdBase {k B : ℕ} (hkK : k ≤ K) (hB : 1 ≤ B)
+    {g : CNF ℕ → ℕ}
+    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold (countingThresholdBase K B)) K ψ = true → g ψ = ψ.modelCount)
+    {φ : CNF ℕ} (hφ : ∀ c ∈ φ, c.length ≤ k) :
+    search (countingThresholdBase K B) K k B g φ = φ.modelCount :=
+  search_eq_modelCount _ hK (two_le_countingThresholdBase K B) hkK
+    (countingTreeBound_countingThresholdBase hK hB) hg hφ
+
+include hM hK in
+/-- **Time and space of `search` under the integer parameter budget.**
+Given a total leaf routine `g` with `hg : ComputableInO g encCNF encNat t t` satisfying the global
+bound `ht` (`O(2 ^ (δ * ψ.length) * (|encCNF ψ| + 1) ^ e)`) for every `ψ : CNF ℕ` and bounded by
+`2 ^ ψ.numVars` on sparse width-`≤ k` formulas, `search M K k B g` has a combined time-and-space
+certificate `ComputableInO (search M K k B g) encCNF encNat T T` with fixed-parameter transfer
+bound `T φ ≤ C₀ * (2 ^ ((1 / B + occBound K M * δ) * φ.numVars) * (|encCNF φ| + 1) ^ E) + C₀`. -/
+theorem exists_computableInO_search_of_budget (hM2 : 2 ≤ M) {k B : ℕ} (hkK : k ≤ K) (hB : 1 ≤ B)
+    (hbudget : 2 ≤ K → countingBChoiceCoeff K ≤ M ∧
+      B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M)
+    {g : CNF ℕ → ℕ} {t : CNF ℕ → ℕ} (hg : ComputableInO g encCNF encNat t t)
+    (hg_le : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold M) K ψ = true → g ψ ≤ 2 ^ ψ.numVars)
+    {δ : ℝ} (hδ : 0 ≤ δ) {c e : ℕ}
+    (ht : ∀ ψ : CNF ℕ, (t ψ : ℝ) ≤ c * (2 ^ (δ * ψ.length) * ((encCNF ψ).length + 1) ^ e) + c) :
+    ∃ T : CNF ℕ → ℕ, ∃ C₀ E : ℕ,
+      ComputableInO (search M K k B g) encCNF encNat T T ∧
+      ∀ φ : CNF ℕ, (T φ : ℝ) ≤
+        C₀ * ((2 : ℝ) ^ ((1 / B + occBound K M * δ) * φ.numVars) *
+          (((encCNF φ).length : ℝ) + 1) ^ E) + C₀ :=
+  exists_computableInO_search hM hK hM2 hkK (countingTreeBound_of_budget hM hK hM2 hB hbudget)
+    hg hg_le hδ ht
+
+include hK in
+/-- **Unconditional time and space of `search` at `countingThresholdBase K B`.** -/
+theorem exists_computableInO_search_countingThresholdBase {k B : ℕ} (hkK : k ≤ K) (hB : 1 ≤ B)
+    {g : CNF ℕ → ℕ} {t : CNF ℕ → ℕ} (hg : ComputableInO g encCNF encNat t t)
+    (hg_le : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ k) →
+      isSparse (countingThreshold (countingThresholdBase K B)) K ψ = true → g ψ ≤ 2 ^ ψ.numVars)
+    {δ : ℝ} (hδ : 0 ≤ δ) {c e : ℕ}
+    (ht : ∀ ψ : CNF ℕ, (t ψ : ℝ) ≤ c * (2 ^ (δ * ψ.length) * ((encCNF ψ).length + 1) ^ e) + c) :
+    ∃ T : CNF ℕ → ℕ, ∃ C₀ E : ℕ,
+      ComputableInO (search (countingThresholdBase K B) K k B g) encCNF encNat T T ∧
+      ∀ φ : CNF ℕ, (T φ : ℝ) ≤
+        C₀ * ((2 : ℝ) ^ ((1 / B + occBound K (countingThresholdBase K B) * δ) * φ.numVars) *
+          (((encCNF φ).length : ℝ) + 1) ^ E) + C₀ :=
+  exists_computableInO_search _ hK (two_le_countingThresholdBase K B) hkK
+    (countingTreeBound_countingThresholdBase hK hB) hg hg_le hδ ht
+
+include hM hK in
+/-- **End-to-end counting sparsification from a dense 3-occurrence model counter under the integer
+parameter budget (promised runtime).**
+Given `2 ≤ k ≤ K` and a total model counter `f : CNF ℕ → ℕ` with a combined time-and-space
+certificate `ComputableInO f encCNF encNat tf tf` that on every dense formula `χ` of width `≤ k`
+and variable occurrence `≤ 3` computes `χ.modelCount` and satisfies
+`(tf χ : ℝ) ≤ c * (2 ^ (δ * χ.numVars) * (|encCNF χ| + 1) ^ e) + c`, the search
+`search M K k B (guardOccurrenceCounter k f)` computes `φ.modelCount` on every formula `φ` of width
+`≤ k` and has a combined time-and-space certificate with fixed-parameter transfer bound
+`O(2 ^ ((1 / B + occBound K M * (k * δ)) * φ.numVars) * (|encCNF φ| + 1) ^ E)`. -/
+theorem exists_computableInO_search_threeOccurrence_promise_of_budget
+    (hM2 : 2 ≤ M) {k B : ℕ} (hk2 : 2 ≤ k) (hkK : k ≤ K) (hB : 1 ≤ B)
+    (hbudget : 2 ≤ K → countingBChoiceCoeff K ≤ M ∧
+      B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M)
+    {f : CNF ℕ → ℕ} {tf : CNF ℕ → ℕ} (hf : ComputableInO f encCNF encNat tf tf)
+    (hf_eq : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars → f χ = χ.modelCount)
+    {δ : ℝ} (hδ : 0 ≤ δ) {c e : ℕ}
+    (ht : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars →
+      (tf χ : ℝ) ≤ c * (2 ^ (δ * χ.numVars) * ((encCNF χ).length + 1) ^ e) + c) :
+    (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) →
+      search M K k B (guardOccurrenceCounter k f) φ = φ.modelCount) ∧
+    ∃ T : CNF ℕ → ℕ, ∃ C₀ E : ℕ,
+      ComputableInO (search M K k B (guardOccurrenceCounter k f)) encCNF encNat T T ∧
+      ∀ φ : CNF ℕ, (T φ : ℝ) ≤
+        C₀ * ((2 : ℝ) ^ ((1 / B + occBound K M * (k * δ)) * φ.numVars) *
+          (((encCNF φ).length : ℝ) + 1) ^ E) + C₀ :=
+  exists_computableInO_search_threeOccurrence_of_promise hM hK hM2 hk2 hkK
+    (countingTreeBound_of_budget hM hK hM2 hB hbudget) hf hf_eq hδ ht
+
+include hM hK in
+/-- **End-to-end counting sparsification from a dense 3-occurrence model counter under the integer
+parameter budget.**
+Given `2 ≤ k ≤ K` and a total model counter `f : CNF ℕ → ℕ` that computes `χ.modelCount` on every
+dense formula `χ` of width `≤ k` and variable occurrence `≤ 3` and has a combined time-and-space
+certificate `ComputableInO f encCNF encNat tf tf` with global bound
+`(tf χ : ℝ) ≤ c * (2 ^ (δ * χ.numVars) * (|encCNF χ| + 1) ^ e) + c`, the search
+`search M K k B (guardOccurrenceCounter k f)` computes `φ.modelCount` on every formula `φ` of width
+`≤ k` and has a combined time-and-space certificate with fixed-parameter transfer bound
+`O(2 ^ ((1 / B + occBound K M * (k * δ)) * φ.numVars) * (|encCNF φ| + 1) ^ E)`. -/
+theorem exists_computableInO_search_threeOccurrence_of_budget
+    (hM2 : 2 ≤ M) {k B : ℕ} (hk2 : 2 ≤ k) (hkK : k ≤ K) (hB : 1 ≤ B)
+    (hbudget : 2 ≤ K → countingBChoiceCoeff K ≤ M ∧
+      B * countingBChoiceCoeff K * Nat.clog 2 (4 * countingDepthCoeff K M * M) ≤ M)
+    {f : CNF ℕ → ℕ} {tf : CNF ℕ → ℕ} (hf : ComputableInO f encCNF encNat tf tf)
+    (hf_eq : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars → f χ = χ.modelCount)
+    {δ : ℝ} (hδ : 0 ≤ δ) {c e : ℕ}
+    (ht : ∀ χ : CNF ℕ, (tf χ : ℝ) ≤ c * (2 ^ (δ * χ.numVars) * ((encCNF χ).length + 1) ^ e) + c) :
+    (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) →
+      search M K k B (guardOccurrenceCounter k f) φ = φ.modelCount) ∧
+    ∃ T : CNF ℕ → ℕ, ∃ C₀ E : ℕ,
+      ComputableInO (search M K k B (guardOccurrenceCounter k f)) encCNF encNat T T ∧
+      ∀ φ : CNF ℕ, (T φ : ℝ) ≤
+        C₀ * ((2 : ℝ) ^ ((1 / B + occBound K M * (k * δ)) * φ.numVars) *
+          (((encCNF φ).length : ℝ) + 1) ^ E) + C₀ :=
+  exists_computableInO_search_threeOccurrence_promise_of_budget hM hK hM2 hk2 hkK hB hbudget
+    hf hf_eq hδ fun χ _ _ _ => ht χ
+
+include hK in
+/-- **Unconditional end-to-end counting sparsification from a dense 3-occurrence model counter at
+`countingThresholdBase K B` (promised runtime).** -/
+theorem exists_computableInO_search_threeOccurrence_thresholdBase
+    {k B : ℕ} (hk2 : 2 ≤ k) (hkK : k ≤ K) (hB : 1 ≤ B)
+    {f : CNF ℕ → ℕ} {tf : CNF ℕ → ℕ} (hf : ComputableInO f encCNF encNat tf tf)
+    (hf_eq : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars → f χ = χ.modelCount)
+    {δ : ℝ} (hδ : 0 ≤ δ) {c e : ℕ}
+    (ht : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars →
+      (tf χ : ℝ) ≤ c * (2 ^ (δ * χ.numVars) * ((encCNF χ).length + 1) ^ e) + c) :
+    (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) →
+      search (countingThresholdBase K B) K k B (guardOccurrenceCounter k f) φ = φ.modelCount) ∧
+    ∃ T : CNF ℕ → ℕ, ∃ C₀ E : ℕ,
+      ComputableInO
+        (search (countingThresholdBase K B) K k B (guardOccurrenceCounter k f)) encCNF encNat T T ∧
+      ∀ φ : CNF ℕ, (T φ : ℝ) ≤
+        C₀ * ((2 : ℝ) ^
+            ((1 / B + occBound K (countingThresholdBase K B) * (k * δ)) * φ.numVars) *
+          (((encCNF φ).length : ℝ) + 1) ^ E) + C₀ :=
+  exists_computableInO_search_threeOccurrence_promise_of_budget
+    ((by decide : 1 ≤ 2).trans (two_le_countingThresholdBase K B)) hK
+    (two_le_countingThresholdBase K B) hk2 hkK hB (fun hk2' => countingThresholdBase_spec hk2' hB)
+    hf hf_eq hδ ht
+
+end CountingSparsify
+
+end Cslib.Complexity
diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingBounds.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingBounds.lean
new file mode 100644
index 000000000..3de949a42
--- /dev/null
+++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingBounds.lean
@@ -0,0 +1,292 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingParameters
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingPathBounds
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSearch
+
+/-!
+# Depth and Leaf-Count Bounds for Counting Sparsification
+
+We connect the actual counting-path insertion and petal-step bounds of `CountingPathBounds`
+(Appendix A.2, Lemma A.3 on p. 46 and the path budgets of Appendix A.3 on p. 46 of
+[OpenAI2026ETH]) to the prefix words of a `CountingBranchingRule`, and combine a leaf-only
+petal-step injection (a library adaptation of §A.3's depth-and-B-positions node encoding on p. 46)
+with the geometric binomial-tail bound `Cslib.sum_choose_le_two_pow_div_add_one` and the
+first-success threshold base `countingThresholdBase` of `CountingParameters` (pp. 46–47) to bound
+the number of leaf words of any counting-sparsification tree.
+
+For a `CountingBranchingRule (fun r => M ^ r) V σ` starting from a state `s` whose clause set
+`R.toClauseSet s` is `Reduced`, nontautological, of width at most `k`, and supported on a finite
+variable set `declared` of size `N = declared.card`:
+* every node word `w` has length at most `countingDepthCoeff k M * N`, where
+  `countingDepthCoeff k M = 4 * ∑ r < k - 1, (3 * M) ^ r`;
+* every node word `w` has `M * #{i < w.length | w[i] = true} ≤ countingBChoiceCoeff k * N`, where
+  `countingBChoiceCoeff k = 4 * ∑ r < k - 1, 3 ^ r`;
+* as a library adaptation of §A.3's `(Cn + 1) * ∑ choose` node bound (p. 46), leafhood rules out
+  trailing-`false` ambiguity so two leaf words with `true` steps at the same positions are equal
+  (`CountingBranchingRule.IsLeafWord.eq_of_getD_eq`); any finset `W` of leaf words therefore
+  injects into the subsets of `range (countingDepthCoeff k M * N)` of cardinality at most
+  `countingBChoiceCoeff k * N / M` without a separate depth factor, giving the pure binomial-sum
+  leaf bound `W.card ≤ ∑ j ≤ countingBChoiceCoeff k * N / M, (countingDepthCoeff k M * N).choose j`
+  (`CountingBranchingRule.card_le_of_isLeafWord`);
+* under the integer parameter budget `countingBChoiceCoeff k ≤ M` and
+  `B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M` (for `2 ≤ k`, with
+  `1 ≤ B`), and in particular unconditionally at `M = countingThresholdBase k B`,
+  `W.card ≤ 2 ^ (N / B + 1)` (`CountingBranchingRule.card_le_two_pow_of_isLeafWord`,
+  `CountingBranchingRule.card_le_two_pow_thresholdBase`).
+
+## Main results
+
+* `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.eq_of_getD_eq`: two
+  leaf words with `true` steps at the same positions are equal.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.length_le`,
+  `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.length_le`: linear depth
+  bound along node and leaf words.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsNodeWord.mul_card_le`,
+  `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.IsLeafWord.mul_card_le`: `M`-scaled
+  petal-step budget along node and leaf words.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_of_isLeafWord`:
+  binomial-sum bound on any finset of leaf words.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_two_pow_of_isLeafWord`,
+  `Cslib.Logic.PL.ClauseSet.Sparsification.CountingBranchingRule.card_le_two_pow_thresholdBase`:
+  exponential bound `2 ^ (declared.card / B + 1)` on any finset of leaf words under the integer
+  parameter budget and at `countingThresholdBase k B`.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*, Appendix A.2 (Lemma A.3, p. 46) and
+  Appendix A.3 (pp. 46–47)][OpenAI2026ETH]
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.ClauseSet.Sparsification
+
+open Finset
+
+variable {V : Type*} [DecidableEq V]
+
+theorem countingDepthCoeff_eq_zero {k : ℕ} (hk : k ≤ 1) (M : ℕ) :
+    countingDepthCoeff k M = 0 := by
+  have hk0 : k - 1 = 0 := by omega
+  simp [countingDepthCoeff, hk0]
+
+theorem countingBChoiceCoeff_eq_zero {k : ℕ} (hk : k ≤ 1) :
+    countingBChoiceCoeff k = 0 := by
+  have hk0 : k - 1 = 0 := by omega
+  simp [countingBChoiceCoeff, hk0]
+
+/-! ### Prefix paths and leaf-count bounds for a counting branching rule -/
+
+namespace CountingBranchingRule
+
+variable {θ : ℕ → ℕ} {σ : Type*} (R : CountingBranchingRule θ V σ)
+
+private theorem walk_append (s : σ) (u v : List Bool) :
+    R.walk s (u ++ v) = R.walk (R.walk s u) v := by
+  induction u generalizing s with
+  | nil => rfl
+  | cons a u ih => exact ih (R.next s a)
+
+private theorem walk_take_succ (s : σ) (w : List Bool) {i : ℕ} (hi : i < w.length) :
+    R.walk s (w.take (i + 1)) = R.next (R.walk s (w.take i)) (w.getD i false) := by
+  rw [List.take_add_one, List.getElem?_eq_getElem hi, Option.toList_some, walk_append,
+    List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hi, Option.getD_some]
+  rfl
+
+variable {R}
+
+private theorem IsNodeWord.not_sparse_take {s : σ} {w : List Bool} (h : R.IsNodeWord s w) :
+    ∀ i < w.length, ¬ Sparse θ (R.toClauseSet (R.walk s (w.take i))) := by
+  induction w generalizing s with
+  | nil => intro i hi; simp at hi
+  | cons b w ih =>
+    intro i hi
+    cases i with
+    | zero => exact h.1
+    | succ i =>
+      rw [List.take_succ_cons, walk]
+      exact ih h.2 i (by simpa using hi)
+
+/-- **Leaf words are determined by their petal steps.** Two leaf words with `true` steps at the
+same positions are equal. -/
+theorem IsLeafWord.eq_of_getD_eq {s : σ} {w w' : List Bool} (hw : R.IsLeafWord s w)
+    (hw' : R.IsLeafWord s w') (h : ∀ i, w.getD i false = w'.getD i false) : w = w' := by
+  induction w generalizing s w' with
+  | nil =>
+    cases w' with
+    | nil => rfl
+    | cons b' w' => exact absurd hw hw'.1
+  | cons b w ih =>
+    cases w' with
+    | nil => exact absurd hw' hw.1
+    | cons b' w' =>
+      have hb : b = b' := by simpa using h 0
+      subst hb
+      rw [ih hw.2 hw'.2 fun i => by simpa using h (i + 1)]
+
+/-- Every node word `w` of a counting branching rule induces a sequence of valid choices
+`(c i, H i)` along its prefixes `w.take i`. -/
+theorem exists_choice_seq_of_isNodeWord (s : σ) {w : List Bool} (hw : R.IsNodeWord s w) :
+    ∃ (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)),
+      (∀ i < w.length,
+        R.toClauseSet (R.walk s (w.take (i + 1))) =
+          countingChild (R.toClauseSet (R.walk s (w.take i))) (c i) (H i) (w.getD i false)) ∧
+      (∀ i < w.length, Choice θ (R.toClauseSet (R.walk s (w.take i))) (c i) (H i)) := by
+  classical
+  have hns := hw.not_sparse_take
+  have hch (i : ℕ) (hi : i < w.length) := R.exists_choice_next _ (hns i hi)
+  let c (i : ℕ) : ℕ := if hi : i < w.length then (hch i hi).choose else 0
+  let H (i : ℕ) : Finset (Literal V) :=
+    if hi : i < w.length then (hch i hi).choose_spec.choose else ∅
+  have hspec (i : ℕ) (hi : i < w.length) :
+      Choice θ (R.toClauseSet (R.walk s (w.take i))) (c i) (H i) ∧
+        ∀ b, R.toClauseSet (R.next (R.walk s (w.take i)) b) =
+          countingChild (R.toClauseSet (R.walk s (w.take i))) (c i) (H i) b := by
+    simp only [c, H, dite_eq_left hi]
+    exact (hch i hi).choose_spec.choose_spec
+  refine ⟨c, H, fun i hi => ?_, fun i hi => (hspec i hi).1⟩
+  rw [walk_take_succ R s w hi]
+  exact (hspec i hi).2 _
+
+section PathBounds
+
+variable {M k : ℕ} (hM : 2 ≤ M)
+  {R : CountingBranchingRule (fun r => M ^ r) V σ} {s : σ}
+  (hred : Reduced (R.toClauseSet s))
+  (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C)
+  (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k)
+  (declared : Finset V)
+  (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared)
+include hM hred hnt hk hsupport
+
+/-- **Node words are short.** From a reduced, nontautological clause set of width `≤ k` over
+`declared`, every node word has length at most `countingDepthCoeff k M * declared.card`. -/
+theorem IsNodeWord.length_le {w : List Bool} (hw : R.IsNodeWord s w) :
+    w.length ≤ countingDepthCoeff k M * declared.card := by
+  obtain ⟨c, H, hstep, hchoice⟩ := exists_choice_seq_of_isNodeWord s hw
+  exact counting_length_le hM w.length (fun i => R.toClauseSet (R.walk s (w.take i)))
+    c H (fun i => w.getD i false) hstep hchoice hred hnt hk declared hsupport
+
+/-- **Node words have few petal steps.** From a reduced, nontautological clause set of width `≤ k`
+over `declared`, every node word satisfies
+`M * #{i < w.length | w.getD i false = true} ≤ countingBChoiceCoeff k * declared.card`. -/
+theorem IsNodeWord.mul_card_le {w : List Bool} (hw : R.IsNodeWord s w) :
+    M * ((range w.length).filter fun i => w.getD i false = true).card ≤
+      countingBChoiceCoeff k * declared.card := by
+  obtain ⟨c, H, hstep, hchoice⟩ := exists_choice_seq_of_isNodeWord s hw
+  exact mul_card_counting_B_le hM w.length (fun i => R.toClauseSet (R.walk s (w.take i)))
+    c H (fun i => w.getD i false) hstep hchoice hred hnt hk declared hsupport
+
+/-- **Leaf words are short.** From a reduced, nontautological clause set of width `≤ k` over
+`declared`, every leaf word has length at most `countingDepthCoeff k M * declared.card`. -/
+theorem IsLeafWord.length_le {w : List Bool} (hw : R.IsLeafWord s w) :
+    w.length ≤ countingDepthCoeff k M * declared.card :=
+  hw.isNodeWord.length_le hM hred hnt hk declared hsupport
+
+/-- **Leaf words have few petal steps.** From a reduced, nontautological clause set of width `≤ k`
+over `declared`, every leaf word satisfies
+`M * #{i < w.length | w.getD i false = true} ≤ countingBChoiceCoeff k * declared.card`. -/
+theorem IsLeafWord.mul_card_le {w : List Bool} (hw : R.IsLeafWord s w) :
+    M * ((range w.length).filter fun i => w.getD i false = true).card ≤
+      countingBChoiceCoeff k * declared.card :=
+  hw.isNodeWord.mul_card_le hM hred hnt hk declared hsupport
+
+/-- **Binomial-sum leaf-word bound.** From a reduced, nontautological clause set of width `≤ k` over
+`declared`, any finset `W` of leaf words has cardinality at most
+`∑_{j ≤ countingBChoiceCoeff k * declared.card / M}
+  (countingDepthCoeff k M * declared.card).choose j`. -/
+theorem card_le_of_isLeafWord (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) :
+    W.card ≤ ∑ j ∈ range (countingBChoiceCoeff k * declared.card / M + 1),
+      (countingDepthCoeff k M * declared.card).choose j := by
+  classical
+  set Λ := countingDepthCoeff k M * declared.card
+  set ρ := countingBChoiceCoeff k * declared.card / M
+  let pos (w : List Bool) : Finset ℕ := (range Λ).filter fun i => w.getD i false = true
+  have hpos : ∀ w ∈ W, pos w ∈ (range Λ).powerset.filter (·.card ≤ ρ) := by
+    intro w hw
+    have hlen := (hW w hw).length_le hM hred hnt hk declared hsupport
+    refine mem_filter.mpr ⟨mem_powerset.mpr (filter_subset _ _), ?_⟩
+    refine (Nat.le_div_iff_mul_le (by omega)).mpr ((Nat.mul_comm _ _).trans_le
+      ((Nat.mul_le_mul_left M (card_le_card fun i hi => ?_)).trans
+        ((hW w hw).mul_card_le hM hred hnt hk declared hsupport)))
+    obtain ⟨-, hi⟩ := mem_filter.mp hi
+    refine mem_filter.mpr ⟨mem_range.mpr ?_, hi⟩
+    by_contra hge
+    rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)] at hi
+    exact Bool.false_ne_true hi
+  have hinj : Set.InjOn pos W := by
+    intro w hw w' hw' h
+    refine (hW w hw).eq_of_getD_eq (hW w' hw') fun i => ?_
+    by_cases hi : i < Λ
+    · have := congrArg (i ∈ ·) h
+      simp only [pos, mem_filter, mem_range, hi, true_and, eq_iff_iff] at this
+      cases hwi : w.getD i false <;> cases hw'i : w'.getD i false <;> simp_all
+    · have hl := (hW w hw).length_le hM hred hnt hk declared hsupport
+      have hl' := (hW w' hw').length_le hM hred hnt hk declared hsupport
+      rw [List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega),
+        List.getD_eq_getElem?_getD, List.getElem?_eq_none (by omega)]
+  calc W.card = (W.image pos).card := (card_image_of_injOn hinj).symm
+    _ ≤ ((range Λ).powerset.filter (·.card ≤ ρ)).card :=
+        card_le_card fun t ht => by
+          obtain ⟨w, hw, rfl⟩ := mem_image.mp ht
+          exact hpos w hw
+    _ ≤ ((range (ρ + 1)).biUnion fun j => (range Λ).powersetCard j).card := by
+        refine card_le_card fun t ht => ?_
+        obtain ⟨htΛ, htρ⟩ := mem_filter.mp ht
+        exact mem_biUnion.mpr ⟨t.card, mem_range.mpr (by omega),
+          mem_powersetCard.mpr ⟨mem_powerset.mp htΛ, rfl⟩⟩
+    _ ≤ ∑ j ∈ range (ρ + 1), ((range Λ).powersetCard j).card := card_biUnion_le
+    _ = ∑ j ∈ range (ρ + 1), Λ.choose j := by
+        refine sum_congr rfl fun j _ => ?_
+        rw [card_powersetCard, card_range]
+
+/-- **Exponential leaf-word bound.** Under the integer parameter budget `countingBChoiceCoeff k ≤ M`
+and `B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M` (for `2 ≤ k`,
+with `1 ≤ B`), any finset `W` of leaf words has cardinality at most `2 ^ (declared.card / B + 1)`.
+-/
+theorem card_le_two_pow_of_isLeafWord {B : ℕ} (hB : 1 ≤ B)
+    (hbudget : 2 ≤ k → countingBChoiceCoeff k ≤ M ∧
+      B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M)
+    (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) :
+    W.card ≤ 2 ^ (declared.card / B + 1) := by
+  refine (card_le_of_isLeafWord hM hred hnt hk declared hsupport W hW).trans ?_
+  by_cases hk2 : 2 ≤ k
+  · obtain ⟨hΓM, hbud⟩ := hbudget hk2
+    exact Cslib.sum_choose_le_two_pow_div_add_one
+      (four_le_countingDepthCoeff hk2) (four_le_countingBChoiceCoeff hk2)
+      hΓM hB hbud declared.card
+  · have hk1 : k ≤ 1 := by omega
+    rw [countingDepthCoeff_eq_zero hk1 M, countingBChoiceCoeff_eq_zero hk1]
+    simp only [zero_mul, Nat.zero_div, zero_add, range_one, sum_singleton, Nat.choose_zero_right]
+    exact Nat.one_le_two_pow
+
+end PathBounds
+
+/-- **Unconditional exponential leaf-word bound at `countingThresholdBase k B`.**
+For any `1 ≤ B` and any counting branching rule `R` at `M = countingThresholdBase k B`, any finset
+`W` of leaf words from a reduced, nontautological clause set of width `≤ k` over `declared` has
+cardinality at most `2 ^ (declared.card / B + 1)`. -/
+theorem card_le_two_pow_thresholdBase {k B : ℕ} (hB : 1 ≤ B)
+    {R : CountingBranchingRule (fun r => (countingThresholdBase k B) ^ r) V σ} {s : σ}
+    (hred : Reduced (R.toClauseSet s))
+    (hnt : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C)
+    (hk : ∀ C ∈ R.toClauseSet s, C.card ≤ k)
+    (declared : Finset V)
+    (hsupport : ∀ C ∈ R.toClauseSet s, ∀ l ∈ C, l.1 ∈ declared)
+    (W : Finset (List Bool)) (hW : ∀ w ∈ W, R.IsLeafWord s w) :
+    W.card ≤ 2 ^ (declared.card / B + 1) :=
+  card_le_two_pow_of_isLeafWord (two_le_countingThresholdBase k B) hred hnt hk declared hsupport hB
+    (fun hk2 => countingThresholdBase_spec hk2 hB) W hW
+
+end CountingBranchingRule
+
+end Cslib.Logic.PL.ClauseSet.Sparsification
diff --git a/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean b/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean
new file mode 100644
index 000000000..27b9383c5
--- /dev/null
+++ b/ComplexityTests/Computability/Complexity/FineGrained/CountingTreeBound.lean
@@ -0,0 +1,90 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Complexity.Computability.Complexity.FineGrained.CountingTreeBound
+
+/-!
+# Tests for `CountingBounds` and `CountingTreeBound`
+-/
+
+@[expose] public section
+
+namespace Cslib.Complexity.CountingTreeBoundTests
+
+open Cslib.Logic.PL Cslib.Logic.PL.CNF.Sparsification Cslib.Logic.PL.ClauseSet.Sparsification
+open Cslib.Complexity.CountingSparsify Turing.MultiTapeTM
+
+example : countingDepthCoeff 1 2 = 0 := by decide
+
+example : countingBChoiceCoeff 1 = 0 := by decide
+
+example : countingDepthCoeff 2 2 = 4 := by decide
+
+example : countingBChoiceCoeff 2 = 4 := by decide
+
+example : countingDepthCoeff 3 2 = 28 := by decide
+
+example : countingBChoiceCoeff 3 = 16 := by decide
+
+/-- Unconditional `CountingTreeBound` witness for `K = 1, B = 1, M = 2`. -/
+example : CountingTreeBound 2 1 1 (countingDepthCoeff 1 2) (by decide) (by decide) :=
+  countingTreeBound_of_budget (by decide) (by decide) (by decide) (by decide) (by decide)
+
+/-- Unconditional `CountingTreeBound` witness for 2-CNF (`K = 2, B = 1, M = 64`), verified by
+`decide` on the integer parameter budget `4 * Nat.clog 2 (4 * 4 * 64) = 40 ≤ 64`. -/
+example : CountingTreeBound 64 2 1 (countingDepthCoeff 2 64) (by decide) (by decide) :=
+  countingTreeBound_of_budget (by decide) (by decide) (by decide) (by decide) (by decide)
+
+/-- Unconditional `CountingTreeBound` witness for 3-CNF (`K = 3, B = 1, M = 512`), verified by
+`decide` on the integer parameter budget `16 * Nat.clog 2 (4 * 6148 * 512) = 384 ≤ 512`. -/
+example : CountingTreeBound 512 3 1 (countingDepthCoeff 3 512) (by decide) (by decide) :=
+  countingTreeBound_of_budget (by decide) (by decide) (by decide) (by decide) (by decide)
+
+/-- Unconditional `CountingTreeBound` witness for arbitrary `1 ≤ K` and `1 ≤ B` at
+`countingThresholdBase K B`. -/
+example {K B : ℕ} (hK : 1 ≤ K) (hB : 1 ≤ B) :
+    CountingTreeBound (countingThresholdBase K B) K B
+      (countingDepthCoeff K (countingThresholdBase K B))
+      ((by decide : 1 ≤ 2).trans (two_le_countingThresholdBase K B)) hK :=
+  countingTreeBound_countingThresholdBase hK hB
+
+/-- Model-count correctness of `CountingSparsify.search` on 3-CNF at `(M, K, k, B) = (512, 3, 3, 1)`
+without an external `CountingTreeBound` hypothesis. -/
+example {g : CNF ℕ → ℕ}
+    (hg : ∀ ψ : CNF ℕ, (∀ c ∈ ψ, c.length ≤ 3) →
+      isSparse (countingThreshold 512) 3 ψ = true → g ψ = ψ.modelCount)
+    {φ : CNF ℕ} (hφ : ∀ c ∈ φ, c.length ≤ 3) :
+    search 512 3 3 1 g φ = φ.modelCount :=
+  search_eq_modelCount_of_budget (by decide) (by decide) (by decide) (by decide) (by decide)
+    (by decide) hg hφ
+
+/-- Unconditional end-to-end counting-sparsification reduction from a dense 3-occurrence model
+counter for arbitrary `2 ≤ k ≤ K` and `1 ≤ B` at `countingThresholdBase K B`. -/
+example {K k B : ℕ} (hK : 1 ≤ K) (hk2 : 2 ≤ k) (hkK : k ≤ K) (hB : 1 ≤ B)
+    {f : CNF ℕ → ℕ} {tf : CNF ℕ → ℕ} (hf : ComputableInO f encCNF encNat tf tf)
+    (hf_eq : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars → f χ = χ.modelCount)
+    {δ : ℝ} (hδ : 0 ≤ δ) {c e : ℕ}
+    (ht : ∀ χ : CNF ℕ, (∀ c ∈ χ, c.length ≤ k) → (∀ v, χ.vars.count v ≤ 3) →
+      χ.vars.toFinset = Finset.range χ.numVars →
+      (tf χ : ℝ) ≤ c * (2 ^ (δ * χ.numVars) * ((encCNF χ).length + 1) ^ e) + c) :
+    (∀ φ : CNF ℕ, (∀ c ∈ φ, c.length ≤ k) →
+      search (countingThresholdBase K B) K k B (guardOccurrenceCounter k f) φ = φ.modelCount) ∧
+    ∃ T : CNF ℕ → ℕ, ∃ C₀ E : ℕ,
+      ComputableInO
+        (search (countingThresholdBase K B) K k B (guardOccurrenceCounter k f)) encCNF encNat T T ∧
+      ∀ φ : CNF ℕ, (T φ : ℝ) ≤
+        C₀ * ((2 : ℝ) ^
+            ((1 / B + occBound K (countingThresholdBase K B) * (k * δ)) * φ.numVars) *
+          (((encCNF φ).length : ℝ) + 1) ^ E) + C₀ :=
+  exists_computableInO_search_threeOccurrence_thresholdBase
+    hK hk2 hkK hB hf hf_eq hδ ht
+
+end Cslib.Complexity.CountingTreeBoundTests