SETH ⇒ OVC sparsification bundle 13: concrete word-RAM formalization

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_12

set_option autoImplicit true

/-! Bounds on clauses subsumed by additions, and witnesses for clauses removed
by normalization. These are local accounting lemmas, not the total path bound. -/
namespace WordRAM.Conjectures.Sparsification.Deletion

def subsumed (formula : CNF n) (small : Clause n) (layer : Nat) : CNF n :=
  formula.filter (fun clause => decide (clause.length = layer ∧ small ⊆ clause))

theorem filter_length_mono (items : List α) (p q : α → Bool)
    (implies : ∀ item ∈ items, p item = true → q item = true) :
    (items.filter p).length ≤ (items.filter q).length := by
  induction items with
  | nil => simp
  | cons item rest ih =>
    have tail := ih (fun a ha => implies a (by simp [ha]))
    have head := implies item (by simp)
    cases hp : p item <;> cases hq : q item <;> simp_all
    omega

/-- Pick any literal of the smaller clause: every subsumed clause contains it. -/
theorem subsumed_le_degree (formula : CNF n) (small : Clause n) (layer : Nat)
    (literal : Literal n) (member : literal ∈ small) :
    (subsumed formula small layer).length ≤ Counting.layerDegree formula literal layer := by
  unfold subsumed Counting.layerDegree
  rw [List.filter_filter]
  apply filter_length_mono
  intro clause _ selected
  have selected : clause.length = layer ∧ small ⊆ clause := of_decide_eq_true selected
  simp [selected.1, selected.2 member]

theorem subsumed_bound (formula : CNF n) (small : Clause n) (layer : Nat)
    (nonempty : small ≠ []) (controlled : Path.Controlled threshold formula layer) :
    (subsumed formula small layer).length ≤ 2 * threshold (layer - 1) - 1 := by
  cases small with
  | nil => exact False.elim (nonempty rfl)
  | cons literal rest =>
    exact Nat.le_trans (subsumed_le_degree formula _ layer literal (by simp)) (controlled literal)

/-- Comparable members of an antichain must be the same list representation. -/
theorem comparable_eq (formula : CNF n) (chain : Normalize.Antichain formula)
    (aMember : a ∈ formula) (bMember : b ∈ formula) (subset : a ⊆ b) : a = b := by
  induction formula with
  | nil => simp at aMember
  | cons head rest ih =>
    obtain ⟨apart, restChain⟩ := List.pairwise_cons.mp chain
    rcases List.mem_cons.mp aMember with eqA | tailA
    · rcases List.mem_cons.mp bMember with eqB | tailB
      · exact eqA.trans eqB.symm
      · rw [eqA] at subset
        exact False.elim ((apart b tailB).1 subset)
    · rcases List.mem_cons.mp bMember with eqB | tailB
      · rw [eqB] at subset
        exact False.elim ((apart a tailA).2 subset)
      · exact ih restChain tailA tailB

/-- An old clause removed during normalization has a subset among the additions.
Existing clauses cannot remove one another because the original is an antichain. -/
theorem removed_witness (formula retained added : CNF n)
    (chain : Normalize.Antichain formula) (retainedSub : retained ⊆ formula)
    (nodup : ∀ clause ∈ retained ++ added, clause.Nodup)
    (old : clause ∈ retained) (removed : clause ∉ Normalize.normalize (retained ++ added)) :
    ∃ small ∈ added, small ⊆ clause := by
  obtain ⟨small, kept, subset⟩ := Normalize.normalize_cover (retained ++ added) clause
    (List.mem_append_left _ old)
  have original := (ChildBounds.normalize_sublist _ nodup).subset kept
  rcases List.mem_append.mp original with member | member
  · have same := comparable_eq formula chain (retainedSub member) (retainedSub old) subset
    subst small
    exact False.elim (removed kept)
  · exact ⟨small, member, subset⟩

/-- A union bound for filters, retaining multiplicity in the input list. -/
theorem filter_or_le (items : List α) (p q : α → Bool) :
    (items.filter (fun item => p item || q item)).length ≤
      (items.filter p).length + (items.filter q).length := by
  induction items with
  | nil => simp
  | cons item rest ih =>
    cases hp : p item <;> cases hq : q item <;> simp [hp, hq] <;> omega

/-- Clauses covered by several additions satisfy the sum of the individual
bounds. Counting overlaps more than once only weakens this upper bound. -/
theorem covered_bound (formula added : CNF n) (layer cap : Nat)
    (individual : ∀ small ∈ added, (subsumed formula small layer).length ≤ cap) :
    (formula.filter (fun clause => decide (clause.length = layer ∧ ∃ small ∈ added, small ⊆ clause))).length ≤
      added.length * cap := by
  induction added with
  | nil => simp
  | cons small rest ih =>
    have first := individual small (by simp)
    have later := ih (fun c hc => individual c (by simp [hc]))
    have union := filter_or_le formula
      (fun clause => decide (clause.length = layer ∧ small ⊆ clause))
      (fun clause => decide (clause.length = layer ∧ ∃ c ∈ rest, c ⊆ clause))
    have eq : (fun clause : Clause n => decide (clause.length = layer ∧ ∃ c ∈ small :: rest, c ⊆ clause)) =
        (fun clause => decide (clause.length = layer ∧ small ⊆ clause) ||
          decide (clause.length = layer ∧ ∃ c ∈ rest, c ⊆ clause)) := by
      funext clause
      simp [and_or_left]
    rw [eq]
    simp only [List.length_cons, Nat.add_mul, Nat.one_mul]
    dsimp only [subsumed] at first
    omega

theorem removed_bound (formula child added : CNF n) (layer : Nat)
    (controlled : Path.Controlled threshold formula layer)
    (nonempty : ∀ small ∈ added, small ≠ [])
    (witness : ∀ clause ∈ formula, clause ∉ child → ∃ small ∈ added, small ⊆ clause) :
    (formula.filter (fun clause => decide (clause.length = layer ∧ clause ∉ child))).length ≤
      added.length * (2 * threshold (layer - 1) - 1) := by
  have covered := covered_bound formula added layer (2 * threshold (layer - 1) - 1)
    (fun small member => subsumed_bound formula small layer (nonempty small member) controlled)
  apply Nat.le_trans _ covered
  apply filter_length_mono
  intro clause member removed
  have removed := of_decide_eq_true removed
  exact decide_eq_true ⟨removed.1, witness clause member removed.2⟩

theorem left_witness (formula : CNF n) (core : Clause n) (size : Nat)
    (normalized : Path.Normalized formula) (coreNodup : core.Nodup)
    (old : clause ∈ formula) (removed : clause ∉ Branch.left formula core size) : core ⊆ clause := by
  by_cases selected : clause.length = size ∧ core ⊆ clause
  · exact selected.2
  · have retained : clause ∈ Branch.remaining formula core size :=
      List.mem_filter.mpr ⟨old, by simp only [decide_eq_false selected, Bool.not_false]⟩
    have clean : ∀ c ∈ Branch.remaining formula core size ++ [core], c.Nodup := by
      intro c member
      rcases List.mem_append.mp member with member | member
      · exact normalized.2 c (List.mem_filter.mp member).1
      · simpa only [List.mem_singleton.mp member] using coreNodup
    obtain ⟨small, member, subset⟩ := removed_witness formula (Branch.remaining formula core size) [core]
      normalized.1 (fun _ h => (List.mem_filter.mp h).1) clean retained removed
    simpa only [List.mem_singleton.mp member] using subset

theorem right_witness (formula : CNF n) (core : Clause n) (size : Nat)
    (normalized : Path.Normalized formula)
    (old : clause ∈ formula) (removed : clause ∉ Branch.right formula core size) :
    ∃ small ∈ (Flowers.family formula core size).map (Branch.petal core), small ⊆ clause := by
  by_cases selected : clause.length = size ∧ core ⊆ clause
  · refine ⟨Branch.petal core clause, ?_, ?_⟩
    · exact List.mem_map.mpr ⟨clause, List.mem_filter.mpr ⟨old, decide_eq_true selected⟩, rfl⟩
    · intro literal member
      exact (List.mem_filter.mp member).1
  · have retained : clause ∈ Branch.remaining formula core size :=
      List.mem_filter.mpr ⟨old, by simp only [decide_eq_false selected, Bool.not_false]⟩
    apply removed_witness formula (Branch.remaining formula core size)
      ((Flowers.family formula core size).map (Branch.petal core)) normalized.1
      (fun _ h => (List.mem_filter.mp h).1) _ retained removed
    intro c member
    rcases List.mem_append.mp member with member | member
    · exact normalized.2 c (List.mem_filter.mp member).1
    · obtain ⟨original, familyMember, rfl⟩ := List.mem_map.mp member
      exact (normalized.2 original (List.mem_filter.mp familyMember).1).filter _

/-- Number of old layer clauses removed by one core branch. -/
theorem left_removed (formula : CNF n) (threshold : Nat → Nat) (k layer : Nat)
    (normalized : Path.Normalized formula) (controlled : Path.Controlled threshold formula layer)
    (found : Selection.select formula threshold k = some (size, core)) :
    (formula.filter (fun clause => decide (clause.length = layer ∧ clause ∉ Branch.left formula core size))).length ≤
      2 * threshold (layer - 1) - 1 := by
  have candidate := (Selection.select_sound formula threshold k found).1
  have bound := removed_bound formula (Branch.left formula core size) [core] layer controlled
    (by
      intro c member empty
      have same := List.mem_singleton.mp member
      have coreEmpty : core = [] := same.symm.trans empty
      have positive := candidate.2.1
      simp [coreEmpty] at positive)
    (fun clause old removed => ⟨core, by simp, left_witness formula core size normalized candidate.1 old removed⟩)
  simpa using bound

/-- Number of old layer clauses removed by one petal branch. -/
theorem right_removed (formula : CNF n) (threshold : Nat → Nat) (k layer : Nat)
    (normalized : Path.Normalized formula) (controlled : Path.Controlled threshold formula layer)
    (found : Selection.select formula threshold k = some (size, core)) :
    (formula.filter (fun clause => decide (clause.length = layer ∧ clause ∉ Branch.right formula core size))).length ≤
      (Flowers.family formula core size).length * (2 * threshold (layer - 1) - 1) := by
  have candidate := (Selection.select_sound formula threshold k found).1
  have bound := removed_bound formula (Branch.right formula core size)
    ((Flowers.family formula core size).map (Branch.petal core)) layer controlled
    (by
      intro small member empty
      obtain ⟨original, familyMember, rfl⟩ := List.mem_map.mp member
      obtain ⟨present, properties⟩ := List.mem_filter.mp familyMember
      have properties := of_decide_eq_true properties
      have length := Branch.petal_length core original candidate.1 (normalized.2 original present) properties.2
      rw [empty] at length
      have proper := candidate.2.2.1
      simp only [List.length_nil, Nat.add_zero] at length
      omega)
    (fun clause old removed => right_witness formula core size normalized old removed)
  simpa only [List.length_map] using bound

/-- A proper subset of an existing clause cannot already be implied by a
smaller existing clause in an antichain. This ensures additions are new. -/
theorem proper_subset_fresh (formula : CNF n) (normalized : Path.Normalized formula)
    (selectedMember : selected ∈ formula) (subset : small ⊆ selected)
    (shorter : small.length < selected.length) (oldMember : old ∈ formula) : ¬ old ⊆ small := by
  intro covered
  have same := comparable_eq formula normalized.1 oldMember selectedMember (List.Subset.trans covered subset)
  rw [same] at covered
  have impossible := (normalized.2 selected selectedMember).length_le_of_subset covered
  omega

theorem core_fresh (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (normalized : Path.Normalized formula) (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select formula threshold k = some (size, core))
    (oldMember : old ∈ formula) : ¬ old ⊆ core := by
  have candidate := (Selection.select_sound formula threshold k found).1
  have nonempty : Flowers.family formula core size ≠ [] := by
    intro empty
    have enough := candidate.2.2.2
    rw [empty] at enough
    have lower := large (size - core.length)
    simp only [List.length_nil] at enough
    omega
  obtain ⟨selected, member⟩ := List.exists_mem_of_ne_nil _ nonempty
  obtain ⟨selectedMember, properties⟩ := List.mem_filter.mp member
  have properties := of_decide_eq_true properties
  apply proper_subset_fresh formula normalized selectedMember properties.2 _ oldMember
  rw [properties.1]
  exact candidate.2.2.1

theorem petal_fresh (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (normalized : Path.Normalized formula)
    (found : Selection.select formula threshold k = some (size, core))
    (newMember : small ∈ (Flowers.family formula core size).map (Branch.petal core))
    (oldMember : old ∈ formula) : ¬ old ⊆ small := by
  have candidate := (Selection.select_sound formula threshold k found).1
  obtain ⟨original, member, rfl⟩ := List.mem_map.mp newMember
  obtain ⟨originalMember, properties⟩ := List.mem_filter.mp member
  have properties := of_decide_eq_true properties
  have length := Branch.petal_length core original candidate.1 (normalized.2 original originalMember) properties.2
  have positive := candidate.2.1
  apply proper_subset_fresh formula normalized originalMember _ (by omega) oldMember
  intro literal member
  exact (List.mem_filter.mp member).1

end WordRAM.Conjectures.Sparsification.Deletion

/-! Added clauses survive normalization, and their actual number can be counted. -/
namespace WordRAM.Conjectures.Sparsification.Additions

theorem petal_subset_lift (core a b : Clause n) (coreInB : core ⊆ b)
    (subset : Branch.petal core a ⊆ Branch.petal core b) : a ⊆ b := by
  intro literal member
  by_cases inCore : literal ∈ core
  · exact coreInB inCore
  · have inPetal : literal ∈ Branch.petal core a := by simp [Branch.petal, member, inCore]
    exact (List.mem_filter.mp (subset inPetal)).1

theorem petals_antichain (formula : CNF n) (core : Clause n) (size : Nat)
    (chain : Normalize.Antichain formula) :
    Normalize.Antichain ((Flowers.family formula core size).map (Branch.petal core)) := by
  apply List.pairwise_map.mpr
  have selected : Normalize.Antichain (Flowers.family formula core size) := chain.filter _
  apply selected.imp_of_mem
  intro a b ha hb apart
  have pa := of_decide_eq_true (List.mem_filter.mp ha).2
  have pb := of_decide_eq_true (List.mem_filter.mp hb).2
  exact ⟨fun subset => apart.1 (petal_subset_lift core a b pb.2 subset),
    fun subset => apart.2 (petal_subset_lift core b a pa.2 subset)⟩

theorem antichain_nodup (formula : CNF n) (chain : Normalize.Antichain formula) : formula.Nodup := by
  apply chain.imp
  intro a b apart eq
  subst b
  exact apart.1 (List.Subset.refl _)

/-- A family of mutually incomparable additions, not subsumed by old clauses,
remains present after normalization. -/
theorem additions_retained (old added : CNF n)
    (chain : Normalize.Antichain added)
    (nodup : ∀ clause ∈ old ++ added, clause.Nodup)
    (fresh : ∀ a ∈ old, ∀ b ∈ added, ¬ a ⊆ b) :
    added ⊆ Normalize.normalize (old ++ added) := by
  intro clause member
  obtain ⟨small, kept, subset⟩ := Normalize.normalize_cover (old ++ added) clause (List.mem_append_right _ member)
  have original := (ChildBounds.normalize_sublist _ nodup).subset kept
  rcases List.mem_append.mp original with original | original
  · exact False.elim (fresh small original clause member subset)
  · have eq := Deletion.comparable_eq added chain original member subset
    simpa only [eq] using kept

def newClauses (old child : CNF n) : CNF n := child.filter (fun clause => !decide (clause ∈ old))

/-- Counts actual newly retained clauses, rather than attempted insertions. -/
theorem new_count (formula retained added : CNF n)
    (retainedSub : retained ⊆ formula) (chain : Normalize.Antichain added)
    (nodup : ∀ clause ∈ retained ++ added, clause.Nodup)
    (fresh : ∀ a ∈ formula, ∀ b ∈ added, ¬ a ⊆ b) :
    (newClauses formula (Normalize.normalize (retained ++ added))).length = added.length := by
  have survives := additions_retained retained added chain nodup
    (fun a ha b hb => fresh a (retainedSub ha) b hb)
  apply Nat.le_antisymm
  · apply List.Nodup.length_le_of_subset
      ((antichain_nodup _ (Normalize.normalize_antichain _)).filter _)
    intro clause member
    obtain ⟨present, absent⟩ := List.mem_filter.mp member
    have absent : clause ∉ formula := by simpa using absent
    have original := (ChildBounds.normalize_sublist _ nodup).subset present
    rcases List.mem_append.mp original with original | original
    · exact False.elim (absent (retainedSub original))
    · exact original
  · apply (antichain_nodup added chain).length_le_of_subset
    intro clause member
    have absent : clause ∉ formula := fun present => fresh clause present clause member (List.Subset.refl _)
    exact List.mem_filter.mpr ⟨survives member, by simp [absent]⟩

theorem core_count (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (normalized : Path.Normalized formula) (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select formula threshold k = some (size, core)) :
    (newClauses formula (Branch.left formula core size)).length = 1 := by
  have candidate := (Selection.select_sound formula threshold k found).1
  apply new_count formula (Branch.remaining formula core size) [core]
    (fun _ h => (List.mem_filter.mp h).1) (by exact List.pairwise_singleton _ _)
  · intro clause member
    rcases List.mem_append.mp member with member | member
    · exact normalized.2 clause (List.mem_filter.mp member).1
    · simpa only [List.mem_singleton.mp member] using candidate.1
  · intro a ha b hb
    have eq := List.mem_singleton.mp hb
    rw [eq]
    exact Deletion.core_fresh formula threshold k normalized large found ha

theorem petal_count (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (normalized : Path.Normalized formula)
    (found : Selection.select formula threshold k = some (size, core)) :
    (newClauses formula (Branch.right formula core size)).length = (Flowers.family formula core size).length := by
  have result := new_count formula (Branch.remaining formula core size)
    ((Flowers.family formula core size).map (Branch.petal core))
    (fun _ h => (List.mem_filter.mp h).1) (petals_antichain formula core size normalized.1)
    (by
      intro clause member
      rcases List.mem_append.mp member with member | member
      · exact normalized.2 clause (List.mem_filter.mp member).1
      · obtain ⟨original, present, rfl⟩ := List.mem_map.mp member
        exact (normalized.2 original (List.mem_filter.mp present).1).filter _)
    (fun a ha b hb => Deletion.petal_fresh formula threshold k normalized found hb ha)
  simpa only [Branch.right, List.length_map] using result

/-- A fresh addition can remove only strictly larger old clauses. -/
theorem removal_strict (small old : Clause n) (nodup : small.Nodup)
    (subset : small ⊆ old) (fresh : ¬ old ⊆ small) : small.length < old.length := by
  apply Nat.lt_of_not_ge
  intro opposite
  exact fresh (Occurrences.subset_reverse small old nodup subset opposite)

theorem core_removal_size (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (normalized : Path.Normalized formula) (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select formula threshold k = some (size, core))
    (old : clause ∈ formula) (removed : clause ∉ Branch.left formula core size) :
    core.length < clause.length := by
  have candidate := (Selection.select_sound formula threshold k found).1
  exact removal_strict core clause candidate.1
    (Deletion.left_witness formula core size normalized candidate.1 old removed)
    (Deletion.core_fresh formula threshold k normalized large found old)

theorem petal_removal_size (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (normalized : Path.Normalized formula)
    (found : Selection.select formula threshold k = some (size, core))
    (old : clause ∈ formula) (removed : clause ∉ Branch.right formula core size) :
    size - core.length < clause.length := by
  have candidate := (Selection.select_sound formula threshold k found).1
  obtain ⟨small, member, subset⟩ := Deletion.right_witness formula core size normalized old removed
  have fresh := Deletion.petal_fresh formula threshold k normalized found member old
  obtain ⟨original, present, eq⟩ := List.mem_map.mp member
  obtain ⟨originalMember, properties⟩ := List.mem_filter.mp present
  have properties := of_decide_eq_true properties
  have nodup : small.Nodup := by rw [← eq]; exact (normalized.2 original originalMember).filter _
  have strict := removal_strict small clause nodup subset fresh
  have length := Branch.petal_length core original candidate.1 (normalized.2 original originalMember) properties.2
  rw [eq] at length
  omega

end WordRAM.Conjectures.Sparsification.Additions