Recursive counting-sparsification tree

The decision sparsification tree (BranchingRule in Complexity/Logics/Propositional/ClauseSet/Sparsification/Tree.lean) fixes its step to child, whose branches cover the parent's satisfying assignments but may overlap. For exact model counting (Counting.lean), countingChild refines the petal branch (true) by adjoining the unit clauses negatedHeartUnits H requiring every literal of H to be false, matching equation (A.2) in Appendix A.1 of OpenAI, The Exponential Time Hypothesis is False (pp. 44–45).

Adding negatedHeartUnits H contributes up to 2 |H| to the clause-width potential ∑_{C ∈ ψ} 2 ^ |C|. A single width-two clause (z = 1, c = 2, |H| = 1) can therefore be replaced by one petal unit and one negated-heart unit of equal total potential 2 + 2 = 4. Whenever the selected flower has at least two clauses (2 ≤ (flower ψ c H).card), however, removing the flower subtracts z · 2 ^ c while the petals and negated-heart units add at most z · 2 ^ (c - |H|) + 2 |H| < z · 2 ^ c (potential_countingChild_lt_of_two_le_card_flower). Any threshold schedule satisfying 2 ≤ θ j for 1 ≤ j—in particular the geometric schedule θ j = M ^ j with 2 ≤ M in Appendix A.1—guarantees 2 ≤ (flower ψ c H).card at every heavy heart (potential_countingChild_lt, potential_countingChild_lt_pow).

Using this strict potential decrease, countingLeaves recursively enumerates the finite list of leaves obtained from chooseBranch and countingChild. Along the recursion we establish:

• leaf sparsity (sparse_of_mem_countingLeaves) whenever 2 ≤ θ j for 1 ≤ j;
• preservation of declared variable support (support_of_mem_countingLeaves), clause width (card_le_of_mem_countingLeaves), and reducedness (reduced_of_mem_countingLeaves);
• exact assignment partition: every satisfying assignment of the root satisfies a unique leaf occurrence (countP_sat_countingLeaves, sat_iff_existsUnique_fin_countingLeaves, sat_iff_existsUnique_mem_countingLeaves), while unsatisfying assignments satisfy none;
• exact additive conservation of CNF.modelCountOn on a single common declared variable set (sum_modelCountOn_countingLeaves, sum_modelCountOn_countingLeaves_toClauseSet), including unused declared variables, empty formulas, unit clauses, and contradictory formulas.

Quantitative insertion, path-length, and 2 ^ (σ n) leaf-count bounds (Appendix A.2–A.3, Lemmas A.1–A.3) are separate results not claimed in this module.

Main definitions

• Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves: well-founded recursive leaf enumeration for disjoint counting sparsification.

Main results

• Cslib.Logic.PL.ClauseSet.Sparsification.potential_countingChild_lt_of_two_le_card_flower: strict potential decrease when the flower has at least two clauses.
• Cslib.Logic.PL.ClauseSet.Sparsification.potential_countingChild_lt: strict potential decrease under 2 ≤ θ j for 1 ≤ j.
• Cslib.Logic.PL.ClauseSet.Sparsification.potential_countingChild_lt_pow: strict potential decrease for the geometric schedule θ j = M ^ j with 2 ≤ M.
• Cslib.Logic.PL.ClauseSet.Sparsification.sparse_of_mem_countingLeaves: every leaf is sparse when 2 ≤ θ j for 1 ≤ j.
• Cslib.Logic.PL.ClauseSet.Sparsification.support_of_mem_countingLeaves: declared-variable support is preserved at every leaf.
• Cslib.Logic.PL.ClauseSet.Sparsification.countP_sat_countingLeaves: exact 0/1 leaf-occurrence multiplicity for every assignment.
• Cslib.Logic.PL.ClauseSet.Sparsification.sum_modelCountOn_countingLeaves: additive conservation of CNF.modelCountOn across all leaves on a common declared variable set.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix A.1, pp. 44–45
• C. Calabro, R. Impagliazzo, R. Paturi, A duality between clause width and clause density for SAT

Negated-heart units and counting-child potential

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_of_mem_negatedHeartUnits {V : Type u_1} [DecidableEq V] {H C : Finset (Literal V)} (hC : C ∈ negatedHeartUnits H) : C.card = 1

Each singleton clause in negatedHeartUnits H has cardinality 1.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.potential_countingChild_lt_of_two_le_card_flower {V : Type u_1} [DecidableEq V] {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h1 : 1 ≤ H.card) (hlt : H.card < c) (hz : 2 ≤ Finset.card (flower ψ c H)) (b : Bool) : potential (countingChild ψ c H b) < potential ψ

Strict potential decrease for countingChild. When 1 ≤ |H| < c and flower ψ c H has at least two clauses, both counting branches strictly decrease potential. On the petal branch (true), removing z ≥ 2 clauses of width c subtracts z · 2 ^ c while adding at most z petals of width c - |H| and |H| negated units of width 1, and z · 2 ^ (c - |H|) + 2 |H| < z · 2 ^ c.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.two_le_card_flower_of_heavy {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) : 2 ≤ Finset.card (flower ψ c H)

Any threshold schedule satisfying 2 ≤ θ j for 1 ≤ j guarantees at least two clauses in the flower of every heavy heart.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.potential_countingChild_lt {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy θ ψ c H) (b : Bool) : potential (countingChild ψ c H b) < potential ψ

Termination under 2 ≤ θ j (1 ≤ j). Every heavy heart has a flower of size at least 2, so both counting children strictly decrease potential.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.potential_countingChild_lt_pow {V : Type u_1} [DecidableEq V] {M : ℕ} (hM : 2 ≤ M) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (h : Heavy (fun (x : ℕ) => M ^ x) ψ c H) (b : Bool) : potential (countingChild ψ c H b) < potential ψ

Termination for geometric thresholds θ j = M ^ j (2 ≤ M) (Appendix A.1, p. 44).

Finite characterization of sparsity and unique choices

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sparse_iff_forall_mem_powerset {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 1 ≤ θ j) (ψ : ClauseSet V) : Sparse θ ψ ↔ ∀ C ∈ ψ, ∀ H ∈ C.powerset, ¬Heavy θ ψ C.card H

When 1 ≤ θ j for 1 ≤ j, sparsity depends only on nonempty proper subsets of clauses present in ψ, giving a finite criterion on any variable type with decidable equality.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.chooseBranch_eq_of_choice_unique {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hch : Choice θ ψ c H) (huniq : ∀ (H' : Finset (Literal V)), Heavy θ ψ c H' → H.card ≤ H'.card → H' = H) : chooseBranch θ ψ = (c, H)

If (c, H) is a valid Choice and no other heavy heart at width c has size at least |H|, chooseBranch must select (c, H).

Recursive leaf enumeration

@[irreducible]

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

Recursively enumerate the leaves of the disjoint counting-sparsification tree of ψ using chooseBranch θ and countingChild. At any non-sparse state whose chosen flower has at least two clauses (which holds automatically whenever 2 ≤ θ j for 1 ≤ j), potential strictly decreases in both children.

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

At a sparse clause set, countingLeaves terminates immediately with [ψ].

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_of_not_sparse {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {ψ : ClauseSet V} (h : ¬Sparse θ ψ) : countingLeaves θ ψ = countingLeaves θ (countingChild ψ (chooseBranch θ ψ).1 (chooseBranch θ ψ).2 false) ++ countingLeaves θ (countingChild ψ (chooseBranch θ ψ).1 (chooseBranch θ ψ).2 true)

When 2 ≤ θ j for 1 ≤ j and ψ is not sparse, countingLeaves branches into the heart (false) and petal-plus-negated-units (true) subtrees for chooseBranch θ ψ.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_of_choice_unique {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hch : Choice θ ψ c H) (hz : 2 ≤ Finset.card (flower ψ c H)) (huniq : ∀ (H' : Finset (Literal V)), Heavy θ ψ c H' → H.card ≤ H'.card → H' = H) : countingLeaves θ ψ = countingLeaves θ (countingChild ψ c H false) ++ countingLeaves θ (countingChild ψ c H true)

Unfolding countingLeaves when the valid Choice at ψ is uniquely (c, H) and flower ψ c H has at least two clauses.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_of_mem_powerset_unique {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 1 ≤ θ j) {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hheavy : Heavy θ ψ c H) (hz : 2 ≤ Finset.card (flower ψ c H)) (hmin : ∀ C ∈ ψ, C.card < c → ∀ H' ∈ C.powerset, ¬Heavy θ ψ C.card H') (huniq : ∀ C ∈ ψ, C.card = c → ∀ H' ∈ C.powerset, Heavy θ ψ c H' → H.card ≤ H'.card → H' = H) : countingLeaves θ ψ = countingLeaves θ (countingChild ψ c H false) ++ countingLeaves θ (countingChild ψ c H true)

Finite criterion for unfolding countingLeaves at a unique valid choice (c, H) when 1 ≤ θ j for 1 ≤ j, inspecting only clauses C ∈ ψ and subsets H' ∈ C.powerset.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countingLeaves_ne_nil {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) : countingLeaves θ ψ ≠ []

countingLeaves never returns the empty list.

Structural invariants along the recursion

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sparse_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} (hθ : ∀ (j : ℕ), 1 ≤ j → 2 ≤ θ j) {ψ L : ClauseSet V} (hL : L ∈ countingLeaves θ ψ) : Sparse θ L

Leaf sparsity. Whenever 2 ≤ θ j for 1 ≤ j, every clause set in countingLeaves θ ψ is θ-sparse.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sparse_of_mem_countingLeaves_pow {V : Type u_1} [DecidableEq V] {M : ℕ} (hM : 2 ≤ M) {ψ L : ClauseSet V} (hL : L ∈ countingLeaves (fun (x : ℕ) => M ^ x) ψ) : Sparse (fun (x : ℕ) => M ^ x) L

Leaf sparsity for geometric thresholds θ j = M ^ j (2 ≤ M).

theorem Cslib.Logic.PL.ClauseSet.Sparsification.support_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ L : ClauseSet V} {declared : Finset V} (hψ : ∀ C ∈ ψ, ∀ l ∈ C, l.1 ∈ declared) (hL : L ∈ countingLeaves θ ψ) (C : Finset (Literal V)) : C ∈ L → ∀ l ∈ C, l.1 ∈ declared

Variable-support preservation. If all variables occurring in ψ belong to declared, then all variables occurring in every leaf L ∈ countingLeaves θ ψ belong to declared.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.card_le_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ L : ClauseSet V} {k : ℕ} (hk : ∀ C ∈ ψ, C.card ≤ k) (hL : L ∈ countingLeaves θ ψ) (C : Finset (Literal V)) : C ∈ L → C.card ≤ k

Clause-width preservation. If every clause of ψ has width at most k, then every clause of every leaf L ∈ countingLeaves θ ψ has width at most k.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.reduced_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {ψ L : ClauseSet V} (hred : Reduced ψ) (hL : L ∈ countingLeaves θ ψ) : Reduced L

Reducedness preservation. From a reduced root ψ, every leaf in countingLeaves θ ψ is reduced.

Exact assignment partition and model-count conservation

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countP_sat_countingLeaves {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) (x : V → Bool) : List.countP (fun (L : ClauseSet V) => decide (L.Sat x)) (countingLeaves θ ψ) = if ψ.Sat x then 1 else 0

Exact assignment partition (multiplicity form). For every assignment x : V → Bool, the number of leaf occurrences in countingLeaves θ ψ satisfied by x is 1 when ψ.Sat x holds and 0 otherwise.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_iff_existsUnique_fin_countingLeaves {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) (x : V → Bool) : ψ.Sat x ↔ ∃! i : Fin (countingLeaves θ ψ).length, (countingLeaves θ ψ)[i].Sat x

Exact assignment partition (indexed leaf occurrence form). An assignment x satisfies ψ if and only if there is a unique index i into countingLeaves θ ψ whose leaf is satisfied by x.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.sat_iff_existsUnique_mem_countingLeaves {V : Type u_1} [DecidableEq V] (θ : ℕ → ℕ) (ψ : ClauseSet V) (x : V → Bool) : ψ.Sat x ↔ ∃! L : ClauseSet V, L ∈ countingLeaves θ ψ ∧ L.Sat x

Exact assignment partition (leaf membership form). Because any satisfiable leaf occurs at most once in countingLeaves θ ψ, x satisfies ψ if and only if there is a unique clause set L satisfying L ∈ countingLeaves θ ψ ∧ L.Sat x.

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

Additive model-count conservation. Summing CNF.modelCountOn declared over all leaves in countingLeaves θ ψ recovers ψ.toCNF.modelCountOn declared on the same declared variable set, preserving free choices for unused declared variables and handling empty or contradictory clause sets without extra premises.

Bridges to CNF formulas and CNF.modelCountOn

@[simp]

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

Clause-set reduction reduce preserves modelCountOn on any declared variable set.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.countP_eval_toCNF_countingLeaves {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 θ φ.toClauseSet)) = if CNF.eval x φ = true then 1 else 0

CNF assignment partition. Evaluating L.toCNF across countingLeaves θ φ.toClauseSet accepts each assignment x at 1 leaf occurrence when φ.eval x = true and 0 otherwise.

theorem Cslib.Logic.PL.ClauseSet.Sparsification.vars_toCNF_subset_of_mem_countingLeaves {V : Type u_1} [DecidableEq V] {θ : ℕ → ℕ} {φ : CNF V} {declared : Finset V} (hvars : φ.vars.toFinset ⊆ declared) {L : ClauseSet V} (hL : L ∈ countingLeaves θ φ.toClauseSet) : L.toCNF.vars.toFinset ⊆ declared

CNF declared-variable support preservation. If φ.vars.toFinset ⊆ declared, then every leaf formula L.toCNF produced from φ.toClauseSet has its occurring variables contained in declared.

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

CNF additive model-count conservation. Summing modelCountOn declared over the leaf formulas of countingLeaves θ φ.toClauseSet recovers φ.modelCountOn declared.

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

Reduced CNF additive model-count conservation. Normalizing the root clause set with reduce before enumerating countingLeaves likewise preserves φ.modelCountOn declared.