feat(sparsification): prove immediate counting payload survival

Complexity.lean

@@ -2196,6 +2196,7 @@ 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.CountingOccurrences
+public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingSurvival
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingTree
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.CountingUnits
 public import Complexity.Logics.Propositional.ClauseSet.Sparsification.List

Complexity/Logics/Propositional/ClauseSet/Sparsification/CountingSurvival.lean

@@ -0,0 +1,178 @@
+/-
+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.CountingDeletion
+
+/-!
+# Immediate survival in counting sparsification
+
+Appendix A.1, Lemma A.1 [OpenAI2026ETH] shows that the heart and petals are new and survive
+immediate reduction. For the B-child, nontautology prevents its additional negated-heart units
+from subsuming a petal. This module proves that fact for the actual `countingChild`, and preserves
+the pointwise absence of complementary literals along actual counting paths.
+
+The local result needs only a heavy heart, positive thresholds and a reduced nontautological
+parent; neither priority in `Choice` is needed. At width at least two, the full counting payload
+consists of the heart or petals, so all its clauses survive and are absent from the current node.
+The root-subclause invariant additionally excludes the root along a path. The resulting equality
+identifies these insertion events with new clauses present in the next node. It does not sum
+events or prove the complete Appendix A.2 recurrence, depth, leaf count or native runtime.
+
+## Main results
+
+* `Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_countingChild`: preservation at one step.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.nontautological_counting_node`: path preservation.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.intro_subset_countingChild`: heart and petal survival.
+* `Cslib.Logic.PL.ClauseSet.Sparsification.countingIntro_filter_eq_node_sdiff`: higher-width
+  insertion events are exactly the new marked clauses present in the next node.
+
+## References
+
+* [OpenAI, *The Exponential Time Hypothesis is False*, Appendix A.1, Lemma A.1][OpenAI2026ETH]
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.PL.ClauseSet.Sparsification
+
+open Finset
+
+variable {V : Type*} [DecidableEq V]
+
+/-- A proper heavy-heart step preserves the absence of complementary literals within each
+clause. This concerns clauses individually, not consistency between different unit clauses. -/
+theorem nontautological_countingChild {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r)
+    {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)}
+    (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C)
+    (h : Heavy θ ψ c H) (b : Bool) :
+    ∀ C ∈ countingChild ψ c H b, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by
+  intro C hC l hl hneg
+  rw [countingChild_eq_reduce_union] at hC
+  rcases mem_union.mp (reduce_subset _ hC) with hC | hC
+  · exact hnt C hC l hl hneg
+  · have hcore : C ∈ intro ψ c H b ∨ C ∈ negatedHeartUnits H := by
+      cases b with
+      | false => exact Or.inl hC
+      | true => exact mem_union.mp hC
+    rcases hcore with hcore | hunit
+    · obtain ⟨D, hD, hCD⟩ := exists_flower_ssuperset hθ h hcore
+      exact hnt D (flower_subset _ _ _ hD) l (hCD.subset hl) (hCD.subset hneg)
+    · obtain ⟨a, -, rfl⟩ := mem_image.mp hunit
+      rw [mem_singleton] at hl hneg
+      subst l
+      rcases a with ⟨v, p⟩
+      cases p <;> simp [Std.Sat.Literal.negate] at hneg
+
+/-- Nontautology at the root is preserved along actual counting children. There is no finite
+ambient variable type or satisfiability premise, and heaviness suffices in place of `Choice`. -/
+theorem nontautological_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))
+    (hnt : ∀ C ∈ ψ 0, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C)
+    {t : ℕ} (ht : t ≤ N) :
+    ∀ C ∈ ψ t, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by
+  induction t with
+  | zero => exact hnt
+  | succ t ih =>
+    rw [hstep t (by omega)]
+    exact nontautological_countingChild hθ (ih (by omega)) (hheavy t (by omega)) (b t)
+
+/-- Every heart or petal survives immediate counting reduction. This includes unit petals but
+does not refer to the B-child's additional negated-heart units. Nontautology prevents those units
+from subsuming any petal. -/
+theorem intro_subset_countingChild {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r)
+    {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hred : Reduced ψ)
+    (hnt : ∀ C ∈ ψ, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C)
+    (h : Heavy θ ψ c H) (b : Bool) : intro ψ c H b ⊆ countingChild ψ c H b := by
+  intro a ha
+  rw [countingChild_eq_reduce_union, mem_reduce]
+  have haI : a ∈ countingIntro ψ c H b := by
+    cases b with
+    | false => exact ha
+    | true => exact mem_union_left _ ha
+  refine ⟨mem_union_right _ haI, fun D hD hDa => ?_⟩
+  obtain ⟨C, hC, haC⟩ := exists_flower_ssuperset hθ h ha
+  rcases mem_union.mp hD with hD | hD
+  · exact hred C (flower_subset _ _ _ hC) D hD (hDa.trans haC)
+  · cases b with
+    | false =>
+      have haH : a = H := mem_singleton.mp ha
+      have hDH : D = H := mem_singleton.mp hD
+      exact (ne_of_ssubset hDa) (hDH.trans haH.symm)
+    | true =>
+      rcases mem_union.mp hD with hD | hD
+      · have hlt := card_lt_card hDa
+        rw [card_of_mem_petals hD, card_of_mem_petals ha] at hlt
+        exact lt_irrefl _ hlt
+      · obtain ⟨l, hl, rfl⟩ := mem_image.mp hD
+        exact hnt C (flower_subset _ _ _ hC) l ((mem_flower.mp hC).2.2 hl)
+          (haC.subset (hDa.subset (mem_singleton_self _)))
+
+/-- Every heart or petal is absent from a reduced parent. This newness fact does not require
+nontautology; the strict flower superset already rules out membership in the old antichain. -/
+theorem notMem_of_mem_intro {θ : ℕ → ℕ} (hθ : ∀ r, 1 ≤ θ r)
+    {ψ : ClauseSet V} {c : ℕ} {H : Finset (Literal V)} (hred : Reduced ψ)
+    (h : Heavy θ ψ c H) {b : Bool} {a : Finset (Literal V)}
+    (ha : a ∈ intro ψ c H b) : a ∉ ψ := by
+  obtain ⟨C, hC, haC⟩ := exists_flower_ssuperset hθ h ha
+  exact fun haψ => hred C (flower_subset _ _ _ hC) a haψ haC
+
+/-- At width at least two, the counting payload contains only the heart or petals.
+The B-child's negated-heart units have width one and are excluded by this hypothesis. -/
+theorem mem_intro_of_mem_countingIntro {ψ : ClauseSet V} {c : ℕ}
+    {H : Finset (Literal V)} {b : Bool} {a : Finset (Literal V)}
+    (ha : a ∈ countingIntro ψ c H b) (ha2 : 2 ≤ a.card) : a ∈ intro ψ c H b := by
+  cases b with
+  | false => exact ha
+  | true =>
+    rcases mem_union.mp ha with ha | ha
+    · exact ha
+    · obtain ⟨l, -, rfl⟩ := mem_image.mp ha
+      simp only [card_singleton] at ha2
+      omega
+
+/-- Along an actual counting path, every width-`j ≥ 2` payload clause survives and is absent
+from both the current node and the root. Thus its insertion event is exactly a new marked clause
+present in the next node. No survival or insertion-balance premise is assumed. -/
+theorem countingIntro_filter_eq_node_sdiff {θ : ℕ → ℕ} (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)
+    {m : ℕ} (hm : m < N) {j : ℕ} (hj : 2 ≤ j) :
+    (countingIntro (ψ m) (c m) (H m) (b m)).filter (·.card = j) =
+      (ψ (m + 1) \ (ψ m ∪ ψ 0)).filter (·.card = j) := by
+  have hredm : Reduced (ψ m) := by
+    cases m with
+    | zero => exact hred
+    | succ m =>
+      rw [hstep m (by omega), countingChild_eq_reduce_union]
+      exact reduced_reduce _
+  have hntm := nontautological_counting_node hθ N ψ c H b hstep hheavy hnt hm.le
+  ext a
+  simp only [mem_filter, mem_sdiff, mem_union]
+  constructor
+  · rintro ⟨ha, haj⟩
+    have hai := mem_intro_of_mem_countingIntro ha (haj ▸ hj)
+    have haψ := notMem_of_mem_intro hθ hredm (hheavy m hm) hai
+    have haroot : a ∉ ψ 0 := by
+      intro ha0
+      obtain ⟨D, hD, hDa⟩ := exists_mem_counting_node_subset N ψ c H b hstep hm.le ha0
+      obtain ⟨C, hC, haC⟩ := exists_flower_ssuperset hθ (hheavy m hm) hai
+      exact hredm C (flower_subset _ _ _ hC) D hD
+        (Finset.ssubset_of_subset_of_ssubset hDa haC)
+    refine ⟨⟨?_, fun h => h.elim haψ haroot⟩, haj⟩
+    rw [hstep m hm]
+    exact intro_subset_countingChild hθ hredm hntm (hheavy m hm) (b m) hai
+  · rintro ⟨⟨ha, hnot⟩, haj⟩
+    rw [hstep m hm, countingChild_eq_reduce_union] at ha
+    exact ⟨(mem_union.mp (reduce_subset _ ha)).resolve_left (fun h => hnot (Or.inl h)), haj⟩
+
+end Cslib.Logic.PL.ClauseSet.Sparsification

ComplexityTests/SparsificationCountingSurvival.lean

@@ -0,0 +1,146 @@
+/-
+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.CountingSurvival
+
+public section
+
+open Cslib.Logic.PL
+open ClauseSet.Sparsification Finset
+
+namespace ComplexityTests.SparsificationCountingSurvival
+
+private def θ (j : ℕ) := 2 ^ j
+
+private theorem θpos (j : ℕ) : 1 ≤ θ j := Nat.one_le_pow j 2 (by decide)
+
+-- Mixed polarities, a two-literal heart, and four disjoint two-literal petals. One of the
+-- negated-heart units is already in the root, so payload is not the same as new unit events.
+private def root : ClauseSet (Fin 10) :=
+  {{(0, false)}, {(0, true), (1, false), (2, true), (3, false)},
+    {(0, true), (1, false), (4, true), (5, false)},
+    {(0, true), (1, false), (6, true), (7, false)},
+    {(0, true), (1, false), (8, true), (9, false)}}
+
+private def heart : Finset (Literal (Fin 10)) := {(0, true), (1, false)}
+
+private theorem rootReduced : Reduced root := by unfold Reduced; decide
+
+private theorem rootNontautological :
+    ∀ C ∈ root, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by decide
+
+private theorem rootHeavy : Heavy θ root 4 heart := by unfold Heavy; decide
+
+private def nodes (b : Bool) (i : ℕ) := if i = 0 then root else countingChild root 4 heart b
+
+private theorem steps (b : Bool) : ∀ i < 1,
+    nodes b (i + 1) = countingChild (nodes b i) 4 heart b := by
+  intro i hi
+  have : i = 0 := by omega
+  subst i
+  rfl
+
+private theorem heavies (b : Bool) : ∀ i < 1, Heavy θ (nodes b i) 4 heart := by
+  intro i hi
+  have : i = 0 := by omega
+  subst i
+  exact rootHeavy
+
+-- Apply the path theorem, then count its concrete insertion batch: A inserts one width-two
+-- heart; B inserts four width-two petals. This exercises the equality in both directions.
+example : ((nodes false 1 \ (nodes false 0 ∪ nodes false 0)).filter (·.card = 2)).card = 1 := by
+  rw [← countingIntro_filter_eq_node_sdiff θpos 1 (nodes false) (fun _ => 4)
+    (fun _ => heart) (fun _ => false) (steps false) (heavies false)
+    rootReduced rootNontautological (m := 0) (by decide) (by decide)]
+  decide
+
+example : ((nodes true 1 \ (nodes true 0 ∪ nodes true 0)).filter (·.card = 2)).card = 4 := by
+  rw [← countingIntro_filter_eq_node_sdiff θpos 1 (nodes true) (fun _ => 4)
+    (fun _ => heart) (fun _ => true) (steps true) (heavies true)
+    rootReduced rootNontautological (m := 0) (by decide) (by decide)]
+  decide
+
+-- The property is clausewise: preservation does not require a satisfying assignment.
+example : ∀ C ∈ nodes false 1, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by
+  exact nontautological_counting_node θpos 1 (nodes false) (fun _ => 4)
+    (fun _ => heart) (fun _ => false) (steps false) (heavies false)
+    rootNontautological (t := 1) le_rfl
+
+example : ∀ C ∈ nodes true 1, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by
+  exact nontautological_countingChild θpos rootNontautological rootHeavy true
+
+-- Existing negated units belong to the raw payload but are not new insertions. Extending the
+-- event equality from widths at least two to width one would fail in this same legal example.
+example : ((countingIntro root 4 heart true).filter (·.card = 1)).card = 2 := by decide
+example : ((nodes true 1 \ root).filter (·.card = 1)).card = 1 := by decide
+example : {(0, false)} ∈ nodes true 1 ∧ {(0, false)} ∈ root := by decide
+
+-- A one-literal petal is also covered by core survival, even though the event equality above
+-- deliberately separates width-one accounting.
+theorem unit_petal_survives : {(2, true)} ∈ countingChild
+    ({{(0, true), (2, true)}, {(0, true), (3, false)}} : ClauseSet (Fin 4))
+    2 {(0, true)} true := by
+  apply intro_subset_countingChild θpos (by unfold Reduced; decide)
+    (by decide) (by unfold Heavy; decide) true
+  decide
+
+-- A later step has a current node different from the root. It removes the remaining old
+-- width-three clause and introduces a width-two heart, while the earlier negated unit persists.
+private def chainRoot : ClauseSet ℕ := {{(0, true), (1, true), (2, true), (3, true)}}
+
+private def chainFirst := countingChild chainRoot 4 {(0, true)} true
+
+private def chainNodes (i : ℕ) :=
+  if i = 0 then chainRoot else if i = 1 then chainFirst
+    else countingChild chainFirst 3 {(1, true), (2, true)} false
+
+private def chainSizes (i : ℕ) := if i = 0 then 4 else 3
+private def chainHearts (i : ℕ) : Finset (Literal ℕ) :=
+  if i = 0 then {(0, true)} else {(1, true), (2, true)}
+private def chainDirs (i : ℕ) := i == 0
+
+private theorem chainSteps : ∀ i < 2, chainNodes (i + 1) =
+    countingChild (chainNodes i) (chainSizes i) (chainHearts i) (chainDirs i) := by
+  intro i hi
+  have : i = 0 ∨ i = 1 := by omega
+  rcases this with rfl | rfl <;> rfl
+
+private theorem chainHeavies : ∀ i < 2,
+    Heavy (fun _ => 1) (chainNodes i) (chainSizes i) (chainHearts i) := by
+  intro i hi
+  have : i = 0 ∨ i = 1 := by omega
+  rcases this with rfl | rfl <;> unfold Heavy <;> decide
+
+example : ((chainNodes 2 \ (chainNodes 1 ∪ chainNodes 0)).filter (·.card = 2)).card = 1 := by
+  rw [← countingIntro_filter_eq_node_sdiff (fun _ => le_rfl) 2 chainNodes chainSizes
+    chainHearts chainDirs chainSteps chainHeavies (by unfold Reduced; decide)
+    (by decide) (m := 1) (by decide) (by decide)]
+  decide
+
+example : {(0, false)} ∈ chainNodes 2 ∧ {(1, true), (2, true)} ∈ chainNodes 2 := by decide
+
+-- Reducedness is essential: a pre-existing unit immediately subsumes the new width-two petal.
+private def unreduced : ClauseSet (Fin 3) :=
+  {{(1, true)}, {(0, true), (1, true), (2, true)}}
+
+example : ∀ C ∈ unreduced, ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by decide
+example : Heavy (fun _ => 1) unreduced 3 {(0, true)} := by unfold Heavy; decide
+example : ¬ Reduced unreduced := by unfold Reduced; decide
+example : {(1, true), (2, true)} ∈ intro unreduced 3 {(0, true)} true ∧
+    {(1, true), (2, true)} ∉ countingChild unreduced 3 {(0, true)} true := by decide
+
+-- The independent tautological full-Choice 4-payload/3-survivor counterexample remains in
+-- SparsificationCountingDeletion. It is unchanged and checked alongside this module.
+
+-- No ambient variable or nonempty-formula hypothesis at a zero-length prefix.
+example : ∀ C ∈ ({∅} : ClauseSet Empty), ∀ l ∈ C, Std.Sat.Literal.negate l ∉ C := by
+  exact nontautological_counting_node θpos 0 (fun _ => ({∅} : ClauseSet Empty))
+    (fun _ => 0) (fun _ => ∅) (fun _ => false) (by intro i hi; omega)
+    (by intro i hi; omega) (by simp) (t := 0) le_rfl
+
+end ComplexityTests.SparsificationCountingSurvival