SETH ⇒ OVC sparsification bundle 11: 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_10

set_option autoImplicit true

/-! A terminating, computable sparsification tree. Its quantitative leaf bound
and wordRAM realization remain separate obligations. -/
namespace WordRAM.Conjectures.Sparsification.Tree

theorem selected_smaller (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select (Normalize.normalize formula) threshold k = some (size, core)) :
    weight (Branch.left (Normalize.normalize formula) core size) < weight formula ∧
      weight (Branch.right (Normalize.normalize formula) core size) < weight formula := by
  have candidate := (Selection.select_sound _ threshold k found).1
  have smaller := Branch.smaller (Normalize.normalize formula) core size candidate.1
    (Normalize.normalize_nodup_literals formula) candidate.2.1
    (Nat.le_trans (large _) candidate.2.2.2)
  exact ⟨Nat.lt_of_lt_of_le smaller.1 (Normalize.normalize_weight formula),
    Nat.lt_of_lt_of_le smaller.2 (Normalize.normalize_weight formula)⟩

/-- Normalize, reject an empty clause, then either retain a sparse leaf or branch
on the first eligible weak flower. -/
def leaves (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) : List (CNF n) :=
  let normalized := Normalize.normalize formula
  if [] ∈ normalized then []
  else
    match _found : Selection.select normalized threshold k with
    | none => [normalized]
    | some (size, core) =>
      leaves (Branch.left normalized core size) threshold k large ++
        leaves (Branch.right normalized core size) threshold k large
termination_by weight formula
decreasing_by
  · exact (selected_smaller formula threshold k large _found).1
  · exact (selected_smaller formula threshold k large _found).2

theorem leaves_holds (assignment : Fin n → Bool) (formula : CNF n)
    (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    Holds assignment formula ↔ ∃ leaf ∈ leaves formula threshold k large, Holds assignment leaf := by
  induction formula using leaves.induct threshold k large with
  | case1 formula normalized empty =>
    dsimp only [normalized] at *
    rw [leaves]
    simp only [if_pos empty, List.not_mem_nil, false_and, exists_false, iff_false]
    intro truth
    have normalized := (Normalize.normalize_holds assignment formula).mpr truth
    have impossible := normalized [] empty
    simp [ClauseHolds] at impossible
  | case2 formula normalized nonempty found =>
    dsimp only [normalized] at *
    rw [leaves]
    simp only [if_neg nonempty]
    split
    · simp only [List.mem_singleton, exists_eq_left]
      exact (Normalize.normalize_holds assignment formula).symm
    · rename_i size core selected
      rw [found] at selected
      contradiction
  | case3 formula normalized nonempty size core found leftIH rightIH =>
    dsimp only [normalized] at *
    rw [leaves]
    simp only [if_neg nonempty]
    split
    · rename_i selected
      rw [found] at selected
      contradiction
    · rename_i otherSize otherCore selected
      rw [found] at selected
      have eq := Option.some.inj selected
      have sizeEq := congrArg Prod.fst eq
      have coreEq := congrArg Prod.snd eq
      dsimp only at sizeEq coreEq
      subst otherSize otherCore
      simp only [List.mem_append, or_and_right, exists_or]
      rw [← leftIH, ← rightIH, ← Branch.holds]
      exact (Normalize.normalize_holds assignment formula).symm

theorem leaves_bounds (formula : CNF n) (threshold : Nat → Nat) (k bound : Nat)
    (large : ∀ i, 2 ≤ threshold i) (positive : 1 ≤ bound)
    (thresholdBound : ∀ i, 0 < i → i < k → threshold i ≤ bound)
    (width : ∀ clause ∈ formula, clause.length ≤ k) :
    ∀ leaf ∈ leaves formula threshold k large,
      (∀ clause ∈ leaf, clause.length ≤ k) ∧ leaf.length ≤ (2 * (k * bound)) * n := by
  revert width
  induction formula using leaves.induct threshold k large with
  | case1 formula normalized empty =>
    dsimp only [normalized] at *
    intro _ leaf member
    rw [leaves] at member
    simp only [if_pos empty, List.not_mem_nil] at member
  | case2 formula normalized nonempty found =>
    dsimp only [normalized] at *
    intro width leaf member
    rw [leaves] at member
    simp only [if_neg nonempty] at member
    split at member
    · have eq := List.mem_singleton.mp member
      subst leaf
      have normalizedWidth := Normalize.normalize_kcnf (SATInstance.mk n formula) width
      exact ⟨normalizedWidth, Selection.select_none_sparse _ threshold k bound
        (Normalize.normalize_antichain formula) (Normalize.normalize_nodup_literals formula)
        (fun c hc eq => nonempty (eq ▸ hc)) normalizedWidth (fun i => by have := large i; omega)
        found positive thresholdBound⟩
    · rename_i size core selected
      rw [found] at selected
      contradiction
  | case3 formula normalized nonempty size core found leftIH rightIH =>
    dsimp only [normalized] at *
    intro width leaf member
    have candidate := Selection.select_sound _ threshold k found
    have normalizedWidth := Normalize.normalize_kcnf (SATInstance.mk n formula) width
    have coreBound : core.length ≤ k := Nat.le_trans (Nat.le_of_lt candidate.1.2.2.1) candidate.2
    have childWidths := Branch.width (Normalize.normalize formula) core size k normalizedWidth coreBound
    rw [leaves] at member
    simp only [if_neg nonempty] at member
    split at member
    · rename_i selected
      rw [found] at selected
      contradiction
    · rename_i otherSize otherCore selected
      rw [found] at selected
      have eq := Option.some.inj selected
      have sizeEq := congrArg Prod.fst eq
      have coreEq := congrArg Prod.snd eq
      dsimp only at sizeEq coreEq
      subst otherSize otherCore
      rcases List.mem_append.mp member with member | member
      · exact leftIH childWidths.1 leaf member
      · exact rightIH childWidths.2 leaf member

theorem leaves_satisfiable (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (large : ∀ i, 2 ≤ threshold i) :
    (SATInstance.mk n formula).Satisfiable ↔
      ∃ leaf ∈ leaves formula threshold k large, (SATInstance.mk n leaf).Satisfiable := by
  constructor
  · rintro ⟨assignment, truth⟩
    obtain ⟨leaf, member, leafTrue⟩ := (leaves_holds assignment formula threshold k large).mp truth
    exact ⟨leaf, member, assignment, leafTrue⟩
  · rintro ⟨leaf, member, assignment, leafTrue⟩
    exact ⟨assignment, (leaves_holds assignment formula threshold k large).mpr ⟨leaf, member, leafTrue⟩⟩

end WordRAM.Conjectures.Sparsification.Tree

/-! The selector's priority invariant: smaller clause sizes precede larger ones;
within one size, smaller petals precede larger petals. -/
namespace WordRAM.Conjectures.Sparsification.Priority

/-- Non-strict lexicographic order of clause size and petal size. -/
def Before (a b : Nat × Clause n) : Prop :=
  a.1 < b.1 ∨ (a.1 = b.1 ∧ a.1 - a.2.length ≤ b.1 - b.2.length)

theorem cores_ordered (n size petals : Nat) :
    ((Selection.cores n (size - petals)).map (fun core => (size, core))).Pairwise Before := by
  apply List.pairwise_of_forall_mem_list
  intro a ha b hb
  obtain ⟨ca, hca, rfl⟩ := List.mem_map.mp ha
  obtain ⟨cb, hcb, rfl⟩ := List.mem_map.mp hb
  have ea := (Selection.mem_cores ca _).mp hca
  have eb := (Selection.mem_cores cb _).mp hcb
  exact Or.inr ⟨rfl, by simp only [ea, eb]; exact Nat.le_refl _⟩

theorem size_ordered (n size : Nat) :
    ((List.range size).flatMap (fun petals =>
      (Selection.cores n (size - petals)).map (fun core => (size, core)))).Pairwise Before := by
  apply List.pairwise_flatMap.mpr
  constructor
  · intro petals _; exact cores_ordered n size petals
  · apply List.pairwise_lt_range.imp_of_mem
    intro i j hi hj less a ha b hb
    obtain ⟨ca, hca, rfl⟩ := List.mem_map.mp ha
    obtain ⟨cb, hcb, rfl⟩ := List.mem_map.mp hb
    have ea := (Selection.mem_cores ca _).mp hca
    have eb := (Selection.mem_cores cb _).mp hcb
    exact Or.inr ⟨rfl, by dsimp only; omega⟩

theorem choices_ordered (n k : Nat) : (Selection.choices n k).Pairwise Before := by
  apply List.pairwise_flatMap.mpr
  constructor
  · intro size _; exact size_ordered n size
  · apply List.pairwise_lt_range.imp
    intro i j less a ha b hb
    obtain ⟨_, _, ha⟩ := List.mem_flatMap.mp ha
    obtain ⟨_, _, hb⟩ := List.mem_flatMap.mp hb
    obtain ⟨_, _, rfl⟩ := List.mem_map.mp ha
    obtain ⟨_, _, rfl⟩ := List.mem_map.mp hb
    exact Or.inl less

/-- In a sorted list, the first successful search precedes any other success. -/
theorem first_le (items : List α) (relation : α → α → Prop)
    (reflexive : ∀ a, relation a a) (ordered : items.Pairwise relation)
    (predicate : α → Bool) (found : items.find? predicate = some selected)
    (member : other ∈ items) (success : predicate other = true) : relation selected other := by
  induction items with
  | nil => simp at member
  | cons head rest ih =>
    obtain ⟨first, later⟩ := List.pairwise_cons.mp ordered
    by_cases hit : predicate head = true
    · have eq : head = selected := by simpa [List.find?_cons, hit] using found
      subst selected
      rcases List.mem_cons.mp member with rfl | member
      · exact reflexive _
      · exact first other member
    · have tailFound : rest.find? predicate = some selected := by
        simpa [List.find?_cons, hit] using found
      rcases List.mem_cons.mp member with rfl | member
      · exact False.elim (hit success)
      · exact ih later tailFound member

/-- Minimality in both priority coordinates, without any assumption that cores
are represented in a particular literal order. -/
theorem selected_first (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (found : Selection.select formula threshold k = some (size, core))
    (candidate : Flowers.Candidate formula threshold otherCore otherSize) (bounded : otherSize ≤ k) :
    size < otherSize ∨ (size = otherSize ∧ size - core.length ≤ otherSize - otherCore.length) := by
  apply first_le (other := (otherSize, otherCore)) (Selection.choices n k) Before (fun a => Or.inr ⟨rfl, Nat.le_refl _⟩)
    (choices_ordered n k) (fun pair => decide (Flowers.Candidate formula threshold pair.2 pair.1)) found
  · exact Selection.choice_complete otherCore otherSize k candidate.2.1 candidate.2.2.1 bounded
  · exact decide_eq_true candidate

theorem no_smaller_size (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (found : Selection.select formula threshold k = some (size, core)) (smaller : otherSize < size) :
    ¬ Flowers.Candidate formula threshold otherCore otherSize := by
  intro candidate
  have selectedBound := (Selection.select_sound formula threshold k found).2
  have order := selected_first formula threshold k found candidate (by omega)
  omega

theorem no_smaller_petals (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (found : Selection.select formula threshold k = some (size, core))
    (smaller : size - otherCore.length < size - core.length) :
    ¬ Flowers.Candidate formula threshold otherCore size := by
  intro candidate
  have order := selected_first formula threshold k found candidate
    (Selection.select_sound formula threshold k found).2
  omega

end WordRAM.Conjectures.Sparsification.Priority

/-! Local occurrence bounds implied by the selector's priority order. -/
namespace WordRAM.Conjectures.Sparsification.Occurrences

theorem subset_reverse (small large : Clause n) (nodup : small.Nodup)
    (subset : small ⊆ large) (length : large.length ≤ small.length) : large ⊆ small := by
  intro literal member
  by_cases present : literal ∈ small
  · exact present
  · have distinct : (literal :: small).Nodup := List.nodup_cons.mpr ⟨present, nodup⟩
    have included : literal :: small ⊆ large := by
      intro l hl
      rcases List.mem_cons.mp hl with rfl | hl
      · exact member
      · exact subset hl
    have impossible := distinct.length_le_of_subset included
    simp only [List.length_cons] at impossible
    omega

/-- At most one member of an antichain can have exactly the core's size. -/
theorem full_core_unique (formula : CNF n) (core : Clause n)
    (chain : Normalize.Antichain formula) (nodup : core.Nodup) :
    (Flowers.family formula core core.length).length ≤ 1 := by
  have subchain : Normalize.Antichain (Flowers.family formula core core.length) := chain.filter _
  have properties : ∀ clause ∈ Flowers.family formula core core.length,
      core ⊆ clause ∧ clause ⊆ core := by
    intro clause member
    have properties := of_decide_eq_true (List.mem_filter.mp member).2
    exact ⟨properties.2, subset_reverse core clause nodup properties.2 (Nat.le_of_eq properties.1)⟩
  generalize Flowers.family formula core core.length = selected at *
  cases selected with
  | nil => simp
  | cons first rest =>
    cases rest with
    | nil => simp
    | cons second rest =>
      have a := properties first (by simp)
      have b := properties second (by simp)
      have apart := (List.pairwise_cons.mp subchain).1 second (by simp)
      exact False.elim (apart.1 (List.Subset.trans a.2 b.1))

/-- Before branching, every smaller layer has bounded literal occurrences. -/
theorem old_layer (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (chain : Normalize.Antichain formula) (base : 2 ≤ threshold 0)
    (found : Selection.select formula threshold k = some (size, core))
    (literal : Literal n) (layer : Nat) (positive : 0 < layer) (smaller : layer < size) :
    Counting.layerDegree formula literal layer < threshold (layer - 1) := by
  by_cases unit : layer = 1
  · subst layer
    have bound := Flowers.unit_degree formula chain literal
    simpa only [Nat.sub_self] using Nat.lt_of_le_of_lt bound (by omega : 1 < threshold 0)
  · have larger : 1 < layer := by omega
    have absent := Priority.no_smaller_size (otherCore := [literal]) formula threshold k found smaller
    have below : (Flowers.family formula [literal] layer).length < threshold (layer - 1) := by
      apply Nat.lt_of_not_ge
      intro enough
      exact absent ⟨by simp, by simp, by simpa using larger, by simpa using enough⟩
    simpa only [Flowers.singleton_family] using below

/-- Adding a literal to the core captures exactly those petals containing it. -/
theorem petal_degree (formula : CNF n) (core : Clause n) (size : Nat) (literal : Literal n)
    (outside : literal ∉ core) :
    Counting.degree ((Flowers.family formula core size).map (Branch.petal core)) literal =
      (Flowers.family formula (literal :: core) size).length := by
  induction formula with
  | nil => simp [Flowers.family, Counting.degree]
  | cons clause rest ih =>
    by_cases selected : clause.length = size ∧ core ⊆ clause
    · by_cases member : literal ∈ clause <;>
        simp_all [Flowers.family, Counting.degree, Branch.petal, List.cons_subset]
    · have absent : ¬ (clause.length = size ∧ literal :: core ⊆ clause) := by
        rintro ⟨eq, subset⟩
        apply selected
        exact ⟨eq, fun l hl => subset (List.mem_cons_of_mem _ hl)⟩
      simp_all [Flowers.family, Counting.degree]

theorem core_literal_absent (formula : CNF n) (core : Clause n) (size : Nat) (literal : Literal n)
    (inside : literal ∈ core) :
    Counting.degree ((Flowers.family formula core size).map (Branch.petal core)) literal = 0 := by
  unfold Counting.degree
  have empty : (((Flowers.family formula core size).map (Branch.petal core)).filter
      (fun clause => decide (literal ∈ clause))) = [] := by
    apply List.eq_nil_iff_forall_not_mem.mpr
    intro clause member
    obtain ⟨present, occurs⟩ := List.mem_filter.mp member
    obtain ⟨original, _, rfl⟩ := List.mem_map.mp present
    have occurs : literal ∈ Branch.petal core original := of_decide_eq_true occurs
    simp [Branch.petal, inside] at occurs
  rw [empty]
  rfl

/-- Priority bounds occurrences in newly added petals, including unit petals.
This bound does not assume that different petals are disjoint. -/
theorem new_petals (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (chain : Normalize.Antichain formula) (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select formula threshold k = some (size, core)) (literal : Literal n) :
    Counting.degree ((Flowers.family formula core size).map (Branch.petal core)) literal <
      threshold (size - core.length - 1) := by
  have candidate := (Selection.select_sound formula threshold k found).1
  by_cases inside : literal ∈ core
  · rw [core_literal_absent formula core size literal inside]
    have bound := large (size - core.length - 1)
    omega
  · rw [petal_degree formula core size literal inside]
    have coreNodup : (literal :: core).Nodup := List.nodup_cons.mpr ⟨inside, candidate.1⟩
    have positive := candidate.2.1
    have proper := candidate.2.2.1
    by_cases unit : size = core.length + 1
    · have bound := full_core_unique formula (literal :: core) chain coreNodup
      simp only [List.length_cons] at bound
      rw [unit]
      have base := large 0
      simpa only [Nat.add_sub_cancel_left, Nat.sub_self] using
        Nat.lt_of_le_of_lt bound (by omega : 1 < threshold 0)
    · have extensionProper : (literal :: core).length < size := by simp only [List.length_cons]; omega
      have earlier : size - (literal :: core).length < size - core.length := by
        simp only [List.length_cons]; omega
      have absent := Priority.no_smaller_petals (otherCore := literal :: core) formula threshold k found earlier
      apply Nat.lt_of_not_ge
      intro enough
      apply absent
      refine ⟨coreNodup, by simp, extensionProper, ?_⟩
      simpa only [List.length_cons, Nat.sub_add_eq] using enough

end WordRAM.Conjectures.Sparsification.Occurrences