From bd90d17c43149277e4b2054e4b2e702a3b8d6af1 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Mon, 26 Oct 2026 23:15:50 -0400 Subject: [PATCH] feat(sparsification): bound cumulative counting insertions --- Complexity.lean | 1 + .../Sparsification/CountingInsertions.lean | 288 ++++++++++++++++++ .../SparsificationCountingInsertions.lean | 173 +++++++++++ 3 files changed, 462 insertions(+) create mode 100644 Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingInsertions.lean create mode 100644 ComplexityTests/SparsificationCountingInsertions.lean diff --git a/Complexity.lean b/Complexity.lean index 548da5734..37aff738f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2208,6 +2208,7 @@ 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.CountingDeletion +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingInsertions public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingOccurrences public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSurvival public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTree diff --git a/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingInsertions.lean b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingInsertions.lean new file mode 100644 index 000000000..b5f481443 --- /dev/null +++ b/Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingInsertions.lean @@ -0,0 +1,288 @@ +/- +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.Logics.Propositional.ClauseSet.Sparsification.CountingSurvival +import Mathlib.Algebra.Group.Action.Defs +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Algebra.Ring.GeomSum +import Mathlib.Tactic.Ring + +/-! +# Cumulative counting-sparsification insertions + +Appendix A.2, Lemma A.3 and equation (A.3) [OpenAI2026ETH] bound actual insertion events along +every path prefix. `countingInsertionCount` sums the new payload at each step, excluding clauses +already in the current node or the root. It does not deduplicate events across steps or discard +insertions whose clauses are later deleted. + +For widths at least two, immediate survival gives the exact balance between cumulative insertions, +present marked clauses and cumulative deletions. Summing the marked-occurrence bound over the two +literals per declared variable bounds present clauses. Summing the one-step deletion charge then +gives (A.3). Units are handled by the existing unit-event budget, including B-negated-heart units. +No tree, potential, search algorithm, depth, leaf-count or native-resource result is asserted. + +## Main definitions + +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount`: cumulative insertion events. + +## Main results + +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_eq_present_add_deleted`: + exact higher-width event balance. +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_one_le`: unit-event budget. +* `Cslib.Logic.PL.ClauseSet.Sparsification.card_counting_marked_le`: present-clause bound. +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_rec`: recurrence (A.3). +* `Cslib.Logic.PL.ClauseSet.Sparsification.countingInsertionCount_le_pow`: Lemma A.3's closed bound. + +## References + +* [OpenAI, *The Exponential Time Hypothesis is False*, Appendix A.2, Lemma A.3][OpenAI2026ETH] +-/ + +@[expose] public section + +namespace Cslib.Logic.PL.ClauseSet.Sparsification + +open Finset + +variable {V : Type*} [DecidableEq V] + +/-- The number of width-`j` insertion events in the first `N` steps. Each summand excludes both +the current node and the initial root; a later deletion does not erase the earlier event. -/ +def countingInsertionCount (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) + (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) (j : ℕ) : ℕ := + ∑ m ∈ range N, ((countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0)).filter + fun C => C.card = j).card + +/-- The empty path prefix has no insertion events, regardless of its root. -/ +@[simp] +theorem countingInsertionCount_zero (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) + (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) (j : ℕ) : + countingInsertionCount 0 ψ c H b j = 0 := by simp [countingInsertionCount] + +/-- Along actual heavy-heart counting steps, every literal remains on a declared root variable. +This does not require a finite ambient variable type, reducedness or nontautology. -/ +theorem support_counting_node {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (declared : Finset V) + (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {t : ℕ} (ht : t ≤ N) : + ∀ C ∈ ψ t, ∀ l ∈ C, l.1 ∈ declared := by + induction t with + | zero => exact hsupport + | succ t ih => + have hprev := ih (by omega) + obtain ⟨D, hD⟩ := (hheavy t (by omega)).flower_nonempty hθ + have hH : ∀ l ∈ H t, l.1 ∈ declared := + fun l hl => hprev D (flower_subset _ _ _ hD) l ((mem_flower.mp hD).2.2 hl) + rw [hstep t (by omega)] + exact support_countingChild (ψ t) (c t) (H t) declared hprev hH (b t) + +/-- Unit events, including the negated-heart units, have total at most two per declared variable. +The root-excluding count is bounded by the existing current-excluding unit-event API. -/ +theorem countingInsertionCount_one_le {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) + (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) : + countingInsertionCount N ψ c H b 1 ≤ 2 * declared.card := by + refine le_trans ?_ (sum_countingUnitInsertions_le hθ N ψ c H b hstep hheavy + hred declared hsupport) + unfold countingInsertionCount + refine sum_le_sum fun m hm => card_le_card fun C hC => ?_ + obtain ⟨hCI, hC1⟩ := mem_filter.mp hC + obtain ⟨hCI, hCold⟩ := mem_sdiff.mp hCI + exact mem_filter.mpr ⟨mem_sdiff.mpr ⟨hCI, fun h => hCold (mem_union_left _ h)⟩, hC1⟩ + +/-- At any counting node, the present marked width-`j ≥ 2` clauses number at most +`4 * declared.card * θ (j - 1)`. Both `Choice` priorities are used by the occurrence supplier. -/ +theorem card_counting_marked_le {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hchoice : ∀ i < N, Choice θ (ψ i) (c i) (H i)) (declared : Finset V) + (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) {t j : ℕ} (ht : t ≤ N) + (hj : 2 ≤ j) : + ((ψ t).filter fun C => C ∉ ψ 0 ∧ C.card = j).card ≤ + 4 * declared.card * θ (j - 1) := by + let literals := declared ×ˢ (univ : Finset Bool) + have hs := support_counting_node hθ N ψ c H b hstep (fun i hi => (hchoice i hi).1) + declared hsupport ht + have hcover : (ψ t).filter (fun C => C ∉ ψ 0 ∧ C.card = j) ⊆ + literals.biUnion fun l => (ψ t).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ {l} ⊆ C := by + intro C hC + obtain ⟨hCψ, hCroot, hCj⟩ := mem_filter.mp hC + obtain ⟨l, hl⟩ : C.Nonempty := card_pos.mp (by omega) + exact mem_biUnion.mpr ⟨l, mem_product.mpr ⟨hs C hCψ l hl, mem_univ _⟩, + mem_filter.mpr ⟨hCψ, hCroot, hCj, singleton_subset_iff.mpr hl⟩⟩ + calc + _ ≤ (literals.biUnion fun l => + (ψ t).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ {l} ⊆ C).card := card_le_card hcover + _ ≤ ∑ l ∈ literals, + ((ψ t).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ {l} ⊆ C).card := card_biUnion_le + _ ≤ ∑ _l ∈ literals, 2 * θ (j - 1) := by + refine sum_le_sum fun l hl => ?_ + have hbound := card_counting_newContaining_lt hθ N ψ c H b hstep hchoice (j := j) ht + (S := {l}) (by simp) (by simp only [card_singleton]; omega) + simpa only [card_singleton] using hbound.le + _ = 4 * declared.card * θ (j - 1) := by + simp only [sum_const, smul_eq_mul, literals, card_product, card_univ, Fintype.card_bool] + ring + +/-- For widths at least two, insertion events telescope exactly into currently present marked +clauses plus deletion events. Events are counted at their steps, without a no-reinsertion premise. +Immediate survival and root exclusion are derived from the actual counting path. -/ +theorem countingInsertionCount_eq_present_add_deleted {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hheavy : ∀ i < N, Heavy θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) + (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) {j : ℕ} (hj : 2 ≤ j) : + countingInsertionCount N ψ c H b j = + ((ψ N).filter fun C => C ∉ ψ 0 ∧ C.card = j).card + + ∑ m ∈ range N, ((ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)).card := by + let S (m : ℕ) := (ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j + let I (m : ℕ) := (countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0)).filter + fun C => C.card = j + let D (m : ℕ) := (ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1) + have hinc (m : ℕ) (hm : m < N) : (I m).card + (S m).card = + (D m).card + (S (m + 1)).card := by + have hsurv := countingIntro_filter_eq_node_sdiff hθ N ψ c H b hstep hheavy hred hnt hm hj + have hI : I m = S (m + 1) \ S m := by + ext C + have hsurvC := congrArg (C ∈ ·) hsurv + simp only [mem_filter, mem_sdiff, mem_union] at hsurvC + simp only [I, S, mem_filter, mem_sdiff, mem_union] + tauto + have hD : D m = S m \ S (m + 1) := by + ext C + simp only [D, S, mem_filter, mem_sdiff] + tauto + rw [hI, hD, card_sdiff_add_card, card_sdiff_add_card, union_comm] + suffices ∀ n, n ≤ N → (∑ m ∈ range n, (I m).card) = + (S n).card + ∑ m ∈ range n, (D m).card from this N le_rfl + intro n + induction n with + | zero => + have hS0 : S 0 = ∅ := by + apply filter_eq_empty_iff.mpr + intro C hC h + exact h.1 hC + simp [hS0] + | succ n ih => + intro hn + have hprev := ih (by omega) + have hstep := hinc n (by omega) + rw [sum_range_succ, sum_range_succ] + omega + +/-- Summing the actual one-step deletion charges gives the deletion term of (A.3). +This part requires both `Choice` priorities and reducedness, but not nontautology. -/ +theorem sum_counting_deleted_marked_le {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hchoice : ∀ i < N, Choice θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) (j : ℕ) : + (∑ m ∈ range N, ((ψ m).filter fun C => C ∉ ψ 0 ∧ C.card = j ∧ C ∉ ψ (m + 1)).card) ≤ + 2 * ∑ i ∈ Ico 1 j, θ (j - i) * countingInsertionCount N ψ c H b i := by + calc + _ ≤ ∑ m ∈ range N, ∑ i ∈ Ico 1 j, 2 * θ (j - i) * + ((countingIntro (ψ m) (c m) (H m) (b m) \ (ψ m ∪ ψ 0)).filter + fun C => C.card = i).card := by + refine sum_le_sum fun m hm => ?_ + exact card_counting_deleted_marked_le hθ N ψ c H b hstep hchoice hred (mem_range.mp hm) j + _ = 2 * ∑ i ∈ Ico 1 j, θ (j - i) * countingInsertionCount N ψ c H b i := by + rw [sum_comm] + simp only [countingInsertionCount, mul_sum, mul_assoc] + +/-- Equation (A.3) for actual cumulative insertion events along any legal counting-path prefix. +The hypotheses assert actual steps, choices and root invariants; neither the balance nor its +target bounds are assumptions. Units have the sharper bound `countingInsertionCount_one_le`. +-/ +theorem countingInsertionCount_le_rec {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hchoice : ∀ i < N, Choice θ (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) + (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) + (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) + {j : ℕ} (hj : 2 ≤ j) : + countingInsertionCount N ψ c H b j ≤ 4 * declared.card * θ (j - 1) + + 2 * ∑ i ∈ Ico 1 j, θ (j - i) * countingInsertionCount N ψ c H b i := by + rw [countingInsertionCount_eq_present_add_deleted hθ N ψ c H b hstep + (fun i hi => (hchoice i hi).1) hred hnt hj] + exact add_le_add (card_counting_marked_le hθ N ψ c H b hstep hchoice declared hsupport le_rfl hj) + (sum_counting_deleted_marked_le hθ N ψ c H b hstep hchoice hred j) + +/-- Lemma A.3: for thresholds `θ r = M ^ r`, every path prefix has at most +`4 * (3 * M) ^ (j - 1) * declared.card` width-`j` insertion events. This holds for all `j ≥ 1`, +in particular the manuscript's range `1 ≤ j < k` for width-`k` roots. The proof does not divide +by the declared-variable count, so it includes zero variables and zero-length prefixes. -/ +theorem countingInsertionCount_le_pow {M : ℕ} (hM : 2 ≤ M) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hchoice : ∀ i < N, Choice (fun r => M ^ r) (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) + (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) + (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) + {j : ℕ} (hj : 1 ≤ j) : + countingInsertionCount N ψ c H b j ≤ 4 * (3 * M) ^ (j - 1) * declared.card := by + have hθ : ∀ r, 1 ≤ M ^ r := fun r => Nat.one_le_pow r M (by omega) + induction j using Nat.strong_induction_on with + | _ j ih => + by_cases hj1 : j = 1 + · subst j + have hunit := countingInsertionCount_one_le hθ N ψ c H b hstep + (fun i hi => (hchoice i hi).1) hred declared hsupport + simp only [Nat.sub_self, pow_zero, mul_one] + omega + have hj2 : 2 ≤ j := by omega + have hrec := countingInsertionCount_le_rec hθ N ψ c H b hstep hchoice hred hnt + declared hsupport hj2 + have hterm (i : ℕ) (hi : i ∈ Ico 1 j) : + M ^ (j - i) * countingInsertionCount N ψ c H b i ≤ + (4 * declared.card * M ^ (j - 1)) * 3 ^ (i - 1) := by + obtain ⟨hi1, hij⟩ := mem_Ico.mp hi + have hpow : M ^ (j - i) * M ^ (i - 1) = M ^ (j - 1) := by + rw [← pow_add] + congr 1 + omega + calc + _ ≤ M ^ (j - i) * (4 * (3 * M) ^ (i - 1) * declared.card) := + Nat.mul_le_mul_left _ (ih i hij hi1) + _ = (4 * declared.card * (M ^ (j - i) * M ^ (i - 1))) * 3 ^ (i - 1) := by + rw [mul_pow] + ring + _ = _ := by rw [hpow] + have hgeom : 1 + 2 * (∑ i ∈ Ico 1 j, (3 : ℕ) ^ (i - 1)) = 3 ^ (j - 1) := by + rw [sum_Ico_eq_sum_range] + simpa only [Nat.add_sub_cancel_left, Nat.add_sub_cancel, Nat.reduceAdd, mul_comm, add_comm] + using geom_sum_mul_add (2 : ℕ) (j - 1) + calc + _ ≤ 4 * declared.card * M ^ (j - 1) + + 2 * ∑ i ∈ Ico 1 j, M ^ (j - i) * countingInsertionCount N ψ c H b i := hrec + _ ≤ 4 * declared.card * M ^ (j - 1) + + 2 * ∑ i ∈ Ico 1 j, (4 * declared.card * M ^ (j - 1)) * 3 ^ (i - 1) := + Nat.add_le_add_left (Nat.mul_le_mul_left 2 (sum_le_sum hterm)) _ + _ = (4 * declared.card * M ^ (j - 1)) * + (1 + 2 * ∑ i ∈ Ico 1 j, 3 ^ (i - 1)) := by + rw [← mul_sum] + ring + _ = (4 * declared.card * M ^ (j - 1)) * 3 ^ (j - 1) := by rw [hgeom] + _ = _ := by rw [mul_pow]; ring + +/-- The closed insertion bound also holds for any declared-variable budget above the finite +support's cardinality. No inhabitance or positivity of that budget is required. -/ +theorem countingInsertionCount_le_pow_of_card_le {M : ℕ} (hM : 2 ≤ M) + (N : ℕ) (ψ : ℕ → ClauseSet V) (c : ℕ → ℕ) (H : ℕ → Finset (Literal V)) (b : ℕ → Bool) + (hstep : ∀ i < N, ψ (i + 1) = countingChild (ψ i) (c i) (H i) (b i)) + (hchoice : ∀ i < N, Choice (fun r => M ^ r) (ψ i) (c i) (H i)) (hred : Reduced (ψ 0)) + (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C) + (declared : Finset V) (hsupport : ∀ C ∈ ψ 0, ∀ l ∈ C, l.1 ∈ declared) + {n : ℕ} (hn : declared.card ≤ n) {j : ℕ} (hj : 1 ≤ j) : + countingInsertionCount N ψ c H b j ≤ 4 * (3 * M) ^ (j - 1) * n := + (countingInsertionCount_le_pow hM N ψ c H b hstep hchoice hred hnt declared hsupport hj).trans + (Nat.mul_le_mul_left _ hn) + +end Cslib.Logic.PL.ClauseSet.Sparsification diff --git a/ComplexityTests/SparsificationCountingInsertions.lean b/ComplexityTests/SparsificationCountingInsertions.lean new file mode 100644 index 000000000..14177b7f3 --- /dev/null +++ b/ComplexityTests/SparsificationCountingInsertions.lean @@ -0,0 +1,173 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module + +public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingInsertions + +public section + +open Cslib.Logic.PL +open ClauseSet.Sparsification Finset + +namespace ComplexityTests.SparsificationCountingInsertions + +/-- A two-petal B-step counts both petal units and the negated-heart unit. -/ +theorem binary_flower_inserts_three_units : + let root : ClauseSet (Fin 3) := {{(0, true), (1, true)}, {(0, true), (2, true)}} + countingInsertionCount 1 + (fun i => if i = 0 then root else countingChild root 2 {(0, true)} true) + (fun _ => 2) (fun _ => {(0, true)}) (fun _ => true) 1 = 3 := by decide + +private def θ (j : ℕ) := 2 ^ j +private theorem θpos (j : ℕ) : 1 ≤ θ j := Nat.one_le_pow j 2 (by decide) + +private theorem θtwo {j : ℕ} (hj : 1 ≤ j) : 2 ≤ θ j := by + change 2 ^ 1 ≤ 2 ^ j + exact Nat.pow_le_pow_right (by decide) hj + +-- The first B-step inserts four pairs. The second B-step deletes two marked pairs, including +-- an unselected pair killed by the negated-heart unit. The root pair is deleted but unmarked. +private def root : ClauseSet (Fin 9) := + {{(1, true), (2, true)}, {(0, true), (1, false), (3, true)}, + {(0, true), (1, true), (4, true)}, {(0, true), (5, true), (6, true)}, + {(0, true), (7, true), (8, true)}} + +private def first := countingChild root 3 {(0, true)} true +private def nodes (tail : Bool) (i : ℕ) := + if i = 0 then root else if i = 1 then first else countingChild first 2 {(1, true)} tail +private def sizes (i : ℕ) := if i = 0 then 3 else 2 +private def hearts (i : ℕ) : Finset (Literal (Fin 9)) := + if i = 0 then {(0, true)} else {(1, true)} +private def dirs (tail : Bool) (i : ℕ) := if i = 0 then true else tail + +private theorem firstChoice : Choice θ root 3 {(0, true)} := by + have hpairs : ∀ C ∈ root, ∀ D ∈ root, C ≠ D → C.card = D.card → C.card = 3 := by decide + have hinter : ∀ C ∈ root, ∀ D ∈ root, C ≠ D → (C ∩ D).card ≤ 1 := by decide + refine ⟨by unfold Heavy; decide, ?_, ?_⟩ + · intro c H hh + have htwo : 2 ≤ (flower root c H).card := + (θtwo (by have := hh.2.1; omega)).trans hh.2.2 + obtain ⟨C, hC, D, hD, hCD⟩ := one_lt_card.mp (by omega : 1 < (flower root c H).card) + have hCc := (mem_flower.mp hC).2.1 + have hDc := (mem_flower.mp hD).2.1 + have := hpairs C (flower_subset _ _ _ hC) D (flower_subset _ _ _ hD) hCD (by omega) + omega + · intro H hh + have htwo : 2 ≤ (flower root 3 H).card := + (θtwo (by have := hh.2.1; omega)).trans hh.2.2 + obtain ⟨C, hC, D, hD, hCD⟩ := one_lt_card.mp (by omega : 1 < (flower root 3 H).card) + have hH : H ⊆ C ∩ D := subset_inter (mem_flower.mp hC).2.2 (mem_flower.mp hD).2.2 + exact (card_le_card hH).trans (hinter C (flower_subset _ _ _ hC) D (flower_subset _ _ _ hD) hCD) + +private theorem secondChoice : Choice θ first 2 {(1, true)} := by + refine ⟨by unfold Heavy; decide, ?_, ?_⟩ + · intro c H hh + have := hh.1 + have := hh.2.1 + omega + · intro H hh + have := hh.2.1 + change H.card ≤ 1 + omega + +private theorem steps (tail : Bool) : ∀ i < 2, + nodes tail (i + 1) = countingChild (nodes tail i) (sizes i) (hearts i) (dirs tail i) := by + intro i hi + have : i = 0 ∨ i = 1 := by omega + rcases this with rfl | rfl <;> rfl + +private theorem choices (tail : Bool) : ∀ i < 2, + Choice θ (nodes tail i) (sizes i) (hearts i) := by + intro i hi + have : i = 0 ∨ i = 1 := by omega + rcases this with rfl | rfl + · exact firstChoice + · exact secondChoice + +private theorem rootReduced : Reduced root := by unfold Reduced; decide +private theorem rootNontautological : + ∀ C ∈ root, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by decide + +-- Compute the event count THROUGH the proved balance, with both a nonzero final population and +-- nonzero deletions. Looking only at the final node would lose half of the insertions. +private theorem four_pair_insertion_events : + countingInsertionCount 2 (nodes true) sizes hearts (dirs true) 2 = 4 := by + have hbalance := countingInsertionCount_eq_present_add_deleted θpos 2 (nodes true) + sizes hearts (dirs true) (steps true) (fun i hi => (choices true i hi).1) + rootReduced rootNontautological (j := 2) (by decide) + have hfinal : ((nodes true 2).filter fun C => C ∉ nodes true 0 ∧ C.card = 2).card = 2 := by decide + have hdeleted : (∑ m ∈ range 2, ((nodes true m).filter fun C => + C ∉ nodes true 0 ∧ C.card = 2 ∧ C ∉ nodes true (m + 1)).card) = 2 := by decide + rw [hfinal, hdeleted] at hbalance + exact hbalance + +example : countingInsertionCount 2 (nodes true) sizes hearts (dirs true) 2 ≠ + ((nodes true 2).filter fun C => C ∉ root ∧ C.card = 2).card := by + rw [four_pair_insertion_events] + decide + +example : countingInsertionCount 2 (nodes true) sizes hearts (dirs true) 1 = 4 := by decide +example : countingInsertionCount 1 (nodes true) sizes hearts (dirs true) 1 = 1 := by decide + +-- The A-tail deletes one marked pair; the B-tail deletes two. Both prefixes still count the +-- same four earlier pair insertions, and root clauses never enter the event count. +example : countingInsertionCount 2 (nodes false) sizes hearts (dirs false) 2 = 4 := by decide +example : ((nodes false 2).filter fun C => C ∉ root ∧ C.card = 2).card = 3 := by decide +example : ((nodes true 1).filter fun C => C.card = 2 ∧ C ∉ nodes true 2).card = 3 := by decide + +-- Actual full-Choice clients of the recurrence and the source's unchanged closed constant. +example : countingInsertionCount 2 (nodes true) sizes hearts (dirs true) 2 ≤ 88 := by + exact countingInsertionCount_le_rec θpos 2 (nodes true) sizes hearts (dirs true) + (steps true) (choices true) rootReduced rootNontautological univ + (by intro C hC l hl; exact mem_univ _) (by decide) + +example : countingInsertionCount 2 (nodes true) sizes hearts (dirs true) 2 ≤ 216 := by + exact countingInsertionCount_le_pow (M := 2) (by decide) 2 (nodes true) sizes hearts (dirs true) + (steps true) (choices true) rootReduced rootNontautological univ + (by intro C hC l hl; exact mem_univ _) (by decide) + +example : countingInsertionCount 2 (nodes true) sizes hearts (dirs true) 2 ≤ 240 := by + exact countingInsertionCount_le_pow_of_card_le (M := 2) (by decide) 2 (nodes true) + sizes hearts (dirs true) (steps true) (choices true) rootReduced rootNontautological univ + (by intro C hC l hl; exact mem_univ _) (n := 10) (by decide) (by decide) + +-- Empty variables with an empty root clause do not require division by n or an inhabited type. +example : countingInsertionCount 0 (fun _ => ({∅} : ClauseSet Empty)) (fun _ => 0) + (fun _ => ∅) (fun _ => false) 2 ≤ 0 := by + exact countingInsertionCount_le_pow_of_card_le (M := 2) (by decide) 0 + (fun _ => ({∅} : ClauseSet Empty)) (fun _ => 0) (fun _ => ∅) (fun _ => false) + (by intro i hi; omega) (by intro i hi; omega) (by unfold Reduced; decide) + (by simp) ∅ (by simp) (n := 0) (by simp) (by decide) + +-- Contradictory root units on one variable are individually nontautological. Neither is an +-- insertion, and no unit propagation is assumed by the bound. +private def oneVariable : ClauseSet Unit := {{((), true)}, {((), false)}} + +example : countingInsertionCount 0 (fun _ => oneVariable) (fun _ => 0) + (fun _ => ∅) (fun _ => false) 1 = 0 := by decide +example : countingInsertionCount 0 (fun _ => oneVariable) (fun _ => 0) + (fun _ => ∅) (fun _ => false) 1 ≤ 4 := by + exact countingInsertionCount_le_pow (M := 2) (by decide) 0 (fun _ => oneVariable) + (fun _ => 0) (fun _ => ∅) (fun _ => false) (by intro i hi; omega) + (by intro i hi; omega) (by unfold Reduced; decide) (by decide) {()} + (by intro C hC l hl; exact mem_singleton.mpr (Subsingleton.elim _ _)) (by decide) + +-- Without nontautology, even the one-step event balance can fail before any OLD marked clause +-- is deleted. This is the full-Choice counterexample retained in SparsificationCountingDeletion. +private def tautRoot : ClauseSet (Fin 8) := + {{(0, true), (0, false), (1, true)}, {(0, true), (2, true), (3, true)}, + {(0, true), (4, true), (5, true)}, {(0, true), (6, true), (7, true)}} +private def tautNodes (i : ℕ) := + if i = 0 then tautRoot else countingChild tautRoot 3 {(0, true)} true + +example : countingInsertionCount 1 tautNodes (fun _ => 3) (fun _ => {(0, true)}) + (fun _ => true) 2 = 4 := by decide +example : ((tautNodes 1).filter fun C => C ∉ tautNodes 0 ∧ C.card = 2).card = 3 := by decide +example : (∑ m ∈ range 1, ((tautNodes m).filter fun C => + C ∉ tautNodes 0 ∧ C.card = 2 ∧ C ∉ tautNodes (m + 1)).card) = 0 := by decide + +end ComplexityTests.SparsificationCountingInsertions