Representation Bridge and Leaf Bounds for CountingTree.countingLeaves

This module provides the representation bridge between the recursive leaf list CountingTree.countingLeaves (CountingTree.lean) and the generic CountingBranchingRule interface (CountingSearch.lean), and applies the leaf-word cardinality bounds of CountingBounds.lean (Appendix A.2–A.3 of OpenAI, The Exponential Time Hypothesis is False, pp. 45–47) to bound (countingLeaves θ ψ).length.

Mathematical overview

1. Nontautological clause filtering (nontautological). The higher-width survival and insertion balance along counting paths (CountingSurvival.lean, CountingInsertions.lean, CountingPathBounds.lean) require that no root clause contains complementary literals l and Std.Sat.Literal.negate l. Because any clause containing complementary literals is satisfied by every assignment, filtering out such clauses via nontautological ψ before applying reduce preserves ClauseSet.Sat (sat_nontautological_iff) and CNF.modelCountOn (modelCountOn_toCNF_nontautological, modelCountOn_toCNF_reduce_nontautological), while ensuring that reduce (nontautological ψ) is both Reduced and nontautological (nontautological_of_mem_reduce_nontautological).

2. Branch-word representation bridge (countingTreeRule, countingLeafWords). Instantiates CountingBranchingRule with CountingTree's deterministic chooser chooseBranch θ (countingTreeRule), enumerates the duplicate-free list of branch-word addresses (countingLeafWords, nodup_countingLeafWords), proves that those addresses are exactly the leaf words of countingTreeRule (mem_countingLeafWords_iff_isLeafWord, isLeafWord_of_mem_countingLeafWords), and shows that walking countingTreeRule along countingLeafWords θ ψ reproduces countingLeaves θ ψ as a list preserving multiplicity (countingLeaves_eq_map_walk_countingLeafWords).

3. Leaf-count and leaf-sparsity corollaries for countingLeaves. Applies CountingBranchingRule.card_le_of_isLeafWord, CountingBranchingRule.card_le_two_pow_of_isLeafWord, and CountingBranchingRule.card_le_two_pow_thresholdBase from CountingBounds.lean to the address finset (countingLeafWords θ ψ).toFinset to bound (countingLeaves θ ψ).length (counting duplicate or unsatisfiable leaf formulas with multiplicity), and packages the resulting Lemma 6.3 / Appendix A.3 leaf-count, occurrence, and model-count conservation bounds for reduce (nontautological φ.toClauseSet).

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.nontautological: filter removing clauses that contain a literal together with its negation.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingTreeRule: the CountingBranchingRule on ClauseSet V driven by chooseBranch θ and countingChild.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingLeafWords: the duplicate-free list of branch-word addresses of the leaves of countingLeaves θ ψ.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.sat_nontautological_iff, Cslib.Logic.PL.ClauseSet.Sparsification.modelCountOn_toCNF_nontautological: removing tautological clauses preserves satisfying assignments and CNF.modelCountOn.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_eq_map_walk_countingLeafWords: countingLeaves θ ψ = (countingLeafWords θ ψ).map ((countingTreeRule θ).walk ψ).
• Cslib.Logic.PL.ClauseSet.Sparsification.mem_countingLeafWords_iff_isLeafWord: under ∀ j, 1 ≤ j → 2 ≤ θ j, w ∈ countingLeafWords θ ψ ↔ (countingTreeRule θ).IsLeafWord ψ w.
• Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_pow_le: binomial-sum leaf-count bound for countingLeaves (M ^ ·) ψ.
• Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_countingThresholdBase_le: exponential 2 ^ (n / B + 1) leaf-count bound at countingThresholdBase k B.
• Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_nontautological_thresholdBase_spec: combined Lemma 6.3 model-count partition, leaf occurrence/clause bounds, and 2 ^ (n / B + 1) leaf-count bound for an arbitrary k-CNF φ : CNF V.

References

• OpenAI, The Exponential Time Hypothesis is False, Section 6.4 (Lemma 6.3) and Appendix A.1–A.3, pp. 43–47

Nontautological clause filtering

def Cslib.Logic.PL.ClauseSet.Sparsification.nontautological {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) : ClauseSet V

Filter a clause set to retain only clauses containing no complementary literal pair l and Std.Sat.Literal.negate l.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {C : Finset (Literal V)} : C ∈ nontautological ψ ↔ C ∈ ψ ∧ ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C

Membership in nontautological ψ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_subset {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) : nontautological ψ ⊆ ψ

nontautological ψ is a subset of ψ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_of_mem_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {C : Finset (Literal V)} (hC : C ∈ nontautological ψ) (l : Literal V) : l ∈ C → Std.Sat.Literal.negate l ∉ C

Every clause in nontautological ψ is free of complementary literals.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_of_mem_reduce_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {C : Finset (Literal V)} (hC : C ∈ reduce (nontautological ψ)) (l : Literal V) : l ∈ C → Std.Sat.Literal.negate l ∉ C

Every clause in reduce (nontautological ψ) is free of complementary literals.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_mem_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {C : Finset (Literal V)} (hC : C ∈ nontautological ψ) : C.card ≤ k

nontautological preserves clause width bounds.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_mem_reduce_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {C : Finset (Literal V)} (hC : C ∈ reduce (nontautological ψ)) : C.card ≤ k

reduce (nontautological ψ) preserves clause width bounds.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.support_of_mem_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {declared : Finset V} (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) {C : Finset (Literal V)} (hC : C ∈ nontautological ψ) (l : Literal V) : l ∈ C → l.1 ∈ declared

nontautological preserves declared-variable support bounds.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.support_of_mem_reduce_nontautological {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {declared : Finset V} (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) {C : Finset (Literal V)} (hC : C ∈ reduce (nontautological ψ)) (l : Literal V) : l ∈ C → l.1 ∈ declared

reduce (nontautological ψ) preserves declared-variable support bounds.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_nontautological_iff {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (x : V → Bool) : (nontautological ψ).Sat x ↔ ψ.Sat x

Removing tautological clauses does not change the satisfying assignments of ψ, because any clause containing both l and Std.Sat.Literal.negate l is satisfied by every assignment.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_reduce_nontautological_iff {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (x : V → Bool) : (reduce (nontautological ψ)).Sat x ↔ ψ.Sat x

Combined nontautological filtering and subsumption reduction preserve ClauseSet.Sat.

@[simp]

theorem Cslib.Logic.PL.ClauseSet.Sparsification.modelCountOn_toCNF_nontautological {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (declared : Finset V) : (nontautological ψ).toCNF.modelCountOn declared = ψ.toCNF.modelCountOn declared

Removing tautological clauses preserves CNF.modelCountOn on any declared variable set.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.modelCountOn_toCNF_reduce_nontautological {V : Type u_1} [DecidableEq V] (ψ : ClauseSet V) (declared : Finset V) : (reduce (nontautological ψ)).toCNF.modelCountOn declared = ψ.toCNF.modelCountOn declared

Normalizing a clause set with reduce (nontautological ψ) preserves CNF.modelCountOn on any declared variable set.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (r : ℕ), 1 ≤ θ r) {ψ L : ClauseSet V} (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hL : L ∈ countingLeaves θ ψ) (C : Finset (Literal V)) : C ∈ L → ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C

Nontautology preservation at leaves. When 1 ≤ θ r for all r and the root ψ has no clause with complementary literals, every leaf L ∈ countingLeaves θ ψ is likewise free of complementary literals within each clause.

Branch-word representation bridge between countingLeaves and CountingBranchingRule

noncomputable def Cslib.Logic.PL.ClauseSet.Sparsification.countingTreeRule {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) : CountingBranchingRule θ V (ClauseSet V)

The CountingBranchingRule on ClauseSet V instantiated with CountingTree's deterministic chooser chooseBranch θ and step countingChild.

@[irreducible]

noncomputable def Cslib.Logic.PL.ClauseSet.Sparsification.countingLeafWords {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : List (List Bool)

Branch-direction words (false for the heart child, true for the petal-plus-negated-units child) corresponding 1-to-1 with the leaf occurrences in countingLeaves θ ψ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_eq_map_walk_countingLeafWords {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : countingLeaves θ ψ = List.map ((countingTreeRule θ).walk ψ) (countingLeafWords θ ψ)

Walking countingTreeRule θ from ψ along the branch-word addresses in countingLeafWords θ ψ reproduces countingLeaves θ ψ in exact list order, preserving multiplicity across equal or unsatisfiable leaf clause sets.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_eq_length_countingLeafWords {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : (countingLeaves θ ψ).length = (countingLeafWords θ ψ).length

The number of leaves in countingLeaves θ ψ (counted with list multiplicity) equals the number of branch-word addresses in countingLeafWords θ ψ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.nodup_countingLeafWords {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : (countingLeafWords θ ψ).Nodup

The branch-word addresses in countingLeafWords θ ψ are pairwise distinct.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_eq_card_toFinset_countingLeafWords {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : (countingLeaves θ ψ).length = (countingLeafWords θ ψ).toFinset.card

Because countingLeafWords θ ψ is duplicate-free, the list length (countingLeaves θ ψ).length equals the cardinality of the address finset (countingLeafWords θ ψ).toFinset.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.mem_countingLeafWords_iff_isLeafWord {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) (ψ : ClauseSet V) (w : List Bool) : w ∈ countingLeafWords θ ψ ↔ (countingTreeRule θ).IsLeafWord ψ w

When ∀ j, 1 ≤ j → 2 ≤ θ j, countingLeafWords θ ψ enumerates data-exact the leaf words of countingTreeRule θ starting from ψ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.isLeafWord_of_mem_countingLeafWords {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {ψ : ClauseSet V} {w : List Bool} (hw : w ∈ countingLeafWords θ ψ) : (countingTreeRule θ).IsLeafWord ψ w

When ∀ j, 1 ≤ j → 2 ≤ θ j, every address w ∈ countingLeafWords θ ψ is a leaf word of countingTreeRule θ starting from ψ.

Leaf-count bounds for countingLeaves via CountingBounds

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_pow_le {V : Type u_1} [DecidableEq V] {k M : ℕ} (hM : 2 ≤ M) {ψ : ClauseSet V} (hred : Reduced ψ) (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ ψ, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) : (countingLeaves (fun (x : ℕ) => M ^ x) ψ).length ≤ ∑ j ∈ Finset.range (countingBChoiceCoeff k * declared.card / M + 1), (countingDepthCoeff k M * declared.card).choose j

Appendix A.3 binomial-sum leaf-count bound for countingLeaves. For any geometric threshold base M ≥ 2 and any reduced, nontautological clause set ψ of width at most k whose occurring variables lie in declared, the number of leaves in countingLeaves (M ^ ·) ψ (counted with list multiplicity) is at most ∑_{j ≤ Γ |declared| / M} (C |declared| choose j), where C = countingDepthCoeff k M and Γ = countingBChoiceCoeff k.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_pow_le_two_pow_of_budget {V : Type u_1} [DecidableEq V] {k M B : ℕ} (hM : 2 ≤ M) (hB : 1 ≤ B) (hbudget : 2 ≤ k → countingBChoiceCoeff k ≤ M ∧ B * countingBChoiceCoeff k * Nat.clog 2 (4 * countingDepthCoeff k M * M) ≤ M) {ψ : ClauseSet V} (hred : Reduced ψ) (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ ψ, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) {n : ℕ} (hn : declared.card ≤ n) : (countingLeaves (fun (x : ℕ) => M ^ x) ψ).length ≤ 2 ^ (n / B + 1)

Leaf-count bound under explicit Appendix A.3 parameter-test hypotheses. When 2 ≤ M, 1 ≤ B, and (for 2 ≤ k) M passes the integer budget test of Appendix A.3, countingLeaves over declared (declared.card ≤ n) produces at most 2 ^ (n / B + 1) leaves.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_countingThresholdBase_le {V : Type u_1} [DecidableEq V] {k B : ℕ} (hB : 1 ≤ B) {ψ : ClauseSet V} (hred : Reduced ψ) (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) (hk : ∀ C ∈ ψ, C.card ≤ k) (declared : Finset V) (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) {n : ℕ} (hn : declared.card ≤ n) : (countingLeaves (fun (j : ℕ) => countingThresholdBase k B ^ j) ψ).length ≤ 2 ^ (n / B + 1)

Appendix A.3 2 ^ (n / B + 1) leaf-count bound at countingThresholdBase k B. For any width k : ℕ, inverse error budget 1 ≤ B, and reduced, nontautological clause set ψ of width at most k over declared (declared.card ≤ n), countingLeaves with threshold base countingThresholdBase k B produces at most 2 ^ (n / B + 1) leaves.

Leaf occurrence and clause-count bounds for countingLeaves

theorem Cslib.Logic.PL.ClauseSet.Sparsification.occurrences_le_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) (hθ0 : 1 ≤ θ 0) {ψ L : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) (hL : L ∈ countingLeaves θ ψ) (v : V) : L.occurrences v ≤ 2 * ∑ c ∈ Finset.range k, θ c

Every leaf L ∈ countingLeaves θ ψ of a width-≤ k root has variable occurrence degree at most 2 * ∑ c ∈ range k, θ c whenever 1 ≤ θ 0 and 2 ≤ θ j for 1 ≤ j.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_mem_countingLeaves_of_support {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) (hθ0 : 1 ≤ θ 0) {ψ L : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {declared : Finset V} (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (hL : L ∈ countingLeaves θ ψ) : Finset.card L ≤ (2 * ∑ c ∈ Finset.range k, θ c) * declared.card + 1

Every leaf L ∈ countingLeaves θ ψ of a width-≤ k root supported on declared has at most 2 * (∑ c ∈ range k, θ c) * declared.card + 1 clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_toCNF_le_of_mem_countingLeaves_of_support {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) (hθ0 : 1 ≤ θ 0) {ψ L : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) {declared : Finset V} (hsupport : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (hL : L ∈ countingLeaves θ ψ) : List.length L.toCNF ≤ (2 * ∑ c ∈ Finset.range k, θ c) * declared.card + 1

Every leaf CNF L.toCNF (L ∈ countingLeaves θ ψ) of a width-≤ k root supported on declared has length at most 2 * (∑ c ∈ range k, θ c) * declared.card + 1.

Unconditional CNF counting-sparsification corollaries

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countP_eval_toCNF_countingLeaves_nontautological {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (φ : CNF V) (x : V → Bool) : List.countP (fun (F : CNF V) => CNF.eval x F) (List.map toCNF (countingLeaves θ (reduce (nontautological φ.toClauseSet)))) = if CNF.eval x φ = true then 1 else 0

Normalized CNF assignment partition. Evaluating L.toCNF across the leaves of reduce (nontautological φ.toClauseSet) accepts each assignment x at 1 leaf occurrence when φ.eval x = true and 0 otherwise.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sum_modelCountOn_countingLeaves_nontautological {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (φ : CNF V) (declared : Finset V) : (List.map (fun (L : ClauseSet V) => L.toCNF.modelCountOn declared) (countingLeaves θ (reduce (nontautological φ.toClauseSet)))).sum = φ.modelCountOn declared

Normalized CNF model-count conservation. Summing L.toCNF.modelCountOn declared across the leaves of reduce (nontautological φ.toClauseSet) equals φ.modelCountOn declared without any nontautology precondition on φ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_nontautological_pow_le {V : Type u_1} [DecidableEq V] {k M : ℕ} (hM : 2 ≤ M) (φ : CNF V) (hk : ∀ c ∈ φ, List.length c ≤ k) (declared : Finset V) (hvars : φ.vars.toFinset ⊆ declared) : (countingLeaves (fun (x : ℕ) => M ^ x) (reduce (nontautological φ.toClauseSet))).length ≤ ∑ j ∈ Finset.range (countingBChoiceCoeff k * declared.card / M + 1), (countingDepthCoeff k M * declared.card).choose j

CNF binomial-sum leaf-count bound. For any 2 ≤ M and any width-≤ k formula φ : CNF V with φ.vars.toFinset ⊆ declared, countingLeaves (M ^ ·) (reduce (nontautological φ.toClauseSet)) has length at most ∑_{j ≤ Γ |declared| / M} (C |declared| choose j).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.length_countingLeaves_nontautological_thresholdBase_le {V : Type u_1} [DecidableEq V] {k B : ℕ} (hB : 1 ≤ B) (φ : CNF V) (hk : ∀ c ∈ φ, List.length c ≤ k) (declared : Finset V) (hvars : φ.vars.toFinset ⊆ declared) {n : ℕ} (hn : declared.card ≤ n) : (countingLeaves (fun (j : ℕ) => countingThresholdBase k B ^ j) (reduce (nontautological φ.toClauseSet))).length ≤ 2 ^ (n / B + 1)

CNF 2 ^ (n / B + 1) leaf-count bound at countingThresholdBase k B. For any width k : ℕ, inverse error budget 1 ≤ B, and width-≤ k formula φ : CNF V with φ.vars.toFinset ⊆ declared and declared.card ≤ n, countingLeaves (fun j => (countingThresholdBase k B) ^ j) (reduce (nontautological φ.toClauseSet)) has length at most 2 ^ (n / B + 1).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_nontautological_thresholdBase_spec {V : Type u_1} [DecidableEq V] {k B : ℕ} (hB : 1 ≤ B) (φ : CNF V) (hk : ∀ c ∈ φ, List.length c ≤ k) (declared : Finset V) (hvars : φ.vars.toFinset ⊆ declared) {n : ℕ} (hn : declared.card ≤ n) : have θ := fun (j : ℕ) => countingThresholdBase k B ^ j; have ψ₀ := reduce (nontautological φ.toClauseSet); (List.map (fun (L : ClauseSet V) => L.toCNF.modelCountOn declared) (countingLeaves θ ψ₀)).sum = φ.modelCountOn declared ∧ (∀ (x : V → Bool), List.countP (fun (F : CNF V) => CNF.eval x F) (List.map toCNF (countingLeaves θ ψ₀)) = if CNF.eval x φ = true then 1 else 0) ∧ (countingLeaves θ ψ₀).length ≤ 2 ^ (n / B + 1) ∧ ∀ L ∈ countingLeaves θ ψ₀, Sparse θ L ∧ Reduced L ∧ (∀ C ∈ L, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) ∧ (∀ C ∈ L, C.card ≤ k) ∧ (∀ C ∈ L, ∀ l ∈ C, l.1 ∈ declared) ∧ (∀ (v : V), L.occurrences v ≤ 2 * ∑ c ∈ Finset.range k, θ c) ∧ Finset.card L ≤ (2 * ∑ c ∈ Finset.range k, θ c) * declared.card + 1

Combined Lemma 6.3 / Appendix A counting-sparsification leaf decomposition for CNFs. For any width k : ℕ, inverse error budget 1 ≤ B, and width-≤ k formula φ : CNF V with occurring variables in declared (declared.card ≤ n), the leaf list countingLeaves (fun j => (countingThresholdBase k B) ^ j) (reduce (nontautological φ.toClauseSet)) satisfies:

1. exact additive modelCountOn declared conservation,
2. exact 0/1 assignment partition across map ClauseSet.toCNF,
3. leaf count at most 2 ^ (n / B + 1), and
4. at every leaf L: sparsity, reducedness, nontautology, clause width ≤ k, support in declared, variable occurrence degree at most 2 * ∑ c ∈ range k, M ^ c, and clause count at most 2 * (∑ c ∈ range k, M ^ c) * declared.card + 1 where M = countingThresholdBase k B.