SETH ⇒ OVC sparsification bundle 12: 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_11

set_option autoImplicit true

/-! Occurrence bounds survive normalization of the actual child formulas. -/
namespace WordRAM.Conjectures.Sparsification.ChildBounds

theorem insert_sublist (clause : Clause n) (formula : CNF n) :
    List.Sublist (Normalize.insert clause formula) (clause :: formula) := by
  unfold Normalize.insert
  split
  · exact List.sublist_cons_self _ _
  · exact List.Sublist.cons_cons clause List.filter_sublist

theorem minimize_sublist (formula : CNF n) : List.Sublist (Normalize.minimize formula) formula := by
  induction formula with
  | nil => exact .refl _
  | cons clause rest ih =>
    exact (insert_sublist clause (Normalize.minimize rest)).trans (.cons_cons clause ih)

theorem normalize_sublist (formula : CNF n) (nodup : ∀ clause ∈ formula, clause.Nodup) :
    List.Sublist (Normalize.normalize formula) formula := by
  have eq : formula.map Normalize.clean = formula := by
    induction formula with
    | nil => rfl
    | cons clause rest ih =>
      simp only [List.map_cons]
      rw [Normalize.clean_eq clause (nodup clause (by simp)), ih (fun c hc => nodup c (by simp [hc]))]
  unfold Normalize.normalize
  rw [eq]
  exact minimize_sublist formula

theorem layer_mono (small large : CNF n) (sublist : List.Sublist small large) (literal : Literal n) (size : Nat) :
    Counting.layerDegree small literal size ≤ Counting.layerDegree large literal size :=
  ((sublist.filter (fun clause => decide (literal ∈ clause))).filter
    (fun clause : Clause n => decide (clause.length = size))).length_le

theorem layer_append (a b : CNF n) (literal : Literal n) (size : Nat) :
    Counting.layerDegree (a ++ b) literal size =
      Counting.layerDegree a literal size + Counting.layerDegree b literal size := by
  simp [Counting.layerDegree, List.filter_append]

theorem layer_le_degree (formula : CNF n) (literal : Literal n) (size : Nat) :
    Counting.layerDegree formula literal size ≤ Counting.degree formula literal :=
  List.length_filter_le _ _

theorem left_bound (formula : CNF n) (core : Clause n) (size layer : Nat) (literal : Literal n)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (coreNodup : core.Nodup) :
    Counting.layerDegree (Branch.left formula core size) literal layer ≤
      Counting.layerDegree formula literal layer + 1 := by
  have clean : ∀ clause ∈ Branch.remaining formula core size ++ [core], clause.Nodup := by
    intro clause member
    rcases List.mem_append.mp member with member | member
    · exact nodup clause (List.mem_filter.mp member).1
    · simpa only [List.mem_singleton.mp member] using coreNodup
  have bound := layer_mono _ _ (normalize_sublist _ clean) literal layer
  rw [layer_append] at bound
  have rest := layer_mono (Branch.remaining formula core size) formula List.filter_sublist literal layer
  have one : Counting.layerDegree [core] literal layer ≤ 1 :=
    Nat.le_trans (List.length_filter_le _ _) (List.length_filter_le _ _)
  exact Nat.le_trans bound (Nat.add_le_add rest one)

theorem right_bound (formula : CNF n) (core : Clause n) (size layer : Nat) (literal : Literal n)
    (nodup : ∀ clause ∈ formula, clause.Nodup) :
    Counting.layerDegree (Branch.right formula core size) literal layer ≤
      Counting.layerDegree formula literal layer +
        Counting.degree ((Flowers.family formula core size).map (Branch.petal core)) literal := by
  have clean : ∀ clause ∈ Branch.remaining formula core size ++
      (Flowers.family formula core size).map (Branch.petal core), clause.Nodup := by
    intro clause member
    rcases List.mem_append.mp member with member | member
    · exact nodup clause (List.mem_filter.mp member).1
    · obtain ⟨original, present, rfl⟩ := List.mem_map.mp member
      exact (nodup original (List.mem_filter.mp present).1).filter _
  have bound := layer_mono _ _ (normalize_sublist _ clean) literal layer
  rw [layer_append] at bound
  have rest := layer_mono (Branch.remaining formula core size) formula List.filter_sublist literal layer
  exact Nat.le_trans bound (Nat.add_le_add rest (layer_le_degree _ literal layer))

/-- A core-adding step establishes the occurrence invariant at the core's size. -/
theorem left_occurrences (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (chain : Normalize.Antichain formula) (nodup : ∀ clause ∈ formula, clause.Nodup)
    (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select formula threshold k = some (size, core)) (literal : Literal n) :
    Counting.layerDegree (Branch.left formula core size) literal core.length ≤
      2 * threshold (core.length - 1) - 1 := by
  have candidate := (Selection.select_sound formula threshold k found).1
  have old := Occurrences.old_layer formula threshold k chain (large 0) found literal core.length
    candidate.2.1 candidate.2.2.1
  have bound := left_bound formula core size core.length literal nodup candidate.1
  have positive := large (core.length - 1)
  omega

/-- A petal-adding step establishes the same invariant at the petal size. -/
theorem right_occurrences (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (chain : Normalize.Antichain formula) (nodup : ∀ clause ∈ formula, clause.Nodup)
    (large : ∀ i, 2 ≤ threshold i)
    (found : Selection.select formula threshold k = some (size, core)) (literal : Literal n) :
    Counting.layerDegree (Branch.right formula core size) literal (size - core.length) ≤
      2 * threshold (size - core.length - 1) - 1 := by
  have candidate := (Selection.select_sound formula threshold k found).1
  have positive := candidate.2.1
  have proper := candidate.2.2.1
  have old := Occurrences.old_layer formula threshold k chain (large 0) found literal (size - core.length)
    (by omega) (by omega)
  have added := Occurrences.new_petals formula threshold k chain large found literal
  have bound := right_bound formula core size (size - core.length) literal nodup
  omega

theorem layer_absent (formula : CNF n) (literal : Literal n) (layer : Nat)
    (absent : ∀ clause ∈ formula, clause.length ≠ layer) : Counting.layerDegree formula literal layer = 0 := by
  unfold Counting.layerDegree
  have empty : ((formula.filter (fun clause => decide (literal ∈ clause))).filter
      (fun clause => decide (clause.length = layer))) = [] := by
    apply List.eq_nil_iff_forall_not_mem.mpr
    intro clause member
    obtain ⟨present, eq⟩ := List.mem_filter.mp member
    exact absent clause (List.mem_filter.mp present).1 (of_decide_eq_true eq)
  rw [empty]
  rfl

theorem unchanged_layer (formula retained added : CNF n)
    (retainedSub : List.Sublist retained formula)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (addedNodup : ∀ clause ∈ added, clause.Nodup)
    (literal : Literal n) (layer : Nat) (absent : ∀ clause ∈ added, clause.length ≠ layer) :
    Counting.layerDegree (Normalize.normalize (retained ++ added)) literal layer ≤
      Counting.layerDegree formula literal layer := by
  have clean : ∀ clause ∈ retained ++ added, clause.Nodup := by
    intro clause member
    rcases List.mem_append.mp member with member | member
    · exact nodup clause (retainedSub.subset member)
    · exact addedNodup clause member
  have bound := layer_mono _ _ (normalize_sublist _ clean) literal layer
  rw [layer_append, layer_absent added literal layer absent, Nat.add_zero] at bound
  exact Nat.le_trans bound (layer_mono retained formula retainedSub literal layer)

theorem left_unchanged (formula : CNF n) (core : Clause n) (size layer : Nat) (literal : Literal n)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (coreNodup : core.Nodup) (different : core.length ≠ layer) :
    Counting.layerDegree (Branch.left formula core size) literal layer ≤ Counting.layerDegree formula literal layer := by
  apply unchanged_layer formula (Branch.remaining formula core size) [core] List.filter_sublist nodup
  · intro clause member
    simpa only [List.mem_singleton.mp member] using coreNodup
  · intro clause member
    simpa only [List.mem_singleton.mp member] using different

theorem right_unchanged (formula : CNF n) (core : Clause n) (size layer : Nat) (literal : Literal n)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (coreNodup : core.Nodup)
    (different : size - core.length ≠ layer) :
    Counting.layerDegree (Branch.right formula core size) literal layer ≤ Counting.layerDegree formula literal layer := by
  apply unchanged_layer formula (Branch.remaining formula core size)
    ((Flowers.family formula core size).map (Branch.petal core)) List.filter_sublist nodup
  · intro clause member
    obtain ⟨original, present, rfl⟩ := List.mem_map.mp member
    exact (nodup original (List.mem_filter.mp present).1).filter _
  · intro clause member
    obtain ⟨original, present, rfl⟩ := List.mem_map.mp member
    obtain ⟨originalMember, properties⟩ := List.mem_filter.mp present
    have properties := of_decide_eq_true properties
    have length := Branch.petal_length core original coreNodup (nodup original originalMember) properties.2
    omega

end WordRAM.Conjectures.Sparsification.ChildBounds

/-! Occurrence invariant along arbitrary paths of the verified branching rule.
A size becomes controlled as soon as a step adds clauses of that size. -/
namespace WordRAM.Conjectures.Sparsification.Path

def Normalized (formula : CNF n) : Prop :=
  Normalize.Antichain formula ∧ ∀ clause ∈ formula, clause.Nodup

def Controlled (threshold : Nat → Nat) (formula : CNF n) (layer : Nat) : Prop :=
  ∀ literal, Counting.layerDegree formula literal layer ≤ 2 * threshold (layer - 1) - 1

inductive Step (threshold : Nat → Nat) (k : Nat) : CNF n → CNF n → Nat → Prop
  | left (found : Selection.select formula threshold k = some (size, core)) :
      Step threshold k formula (Branch.left formula core size) core.length
  | right (found : Selection.select formula threshold k = some (size, core)) :
      Step threshold k formula (Branch.right formula core size) (size - core.length)

theorem step_normalized (step : Step threshold k formula child added) : Normalized child := by
  cases step with
  | left found => exact ⟨Normalize.normalize_antichain _, Normalize.normalize_nodup_literals _⟩
  | right found => exact ⟨Normalize.normalize_antichain _, Normalize.normalize_nodup_literals _⟩

theorem step_added (step : Step threshold k formula child added) (normalized : Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) : Controlled threshold child added := by
  cases step with
  | left found => exact ChildBounds.left_occurrences _ _ _ normalized.1 normalized.2 large found
  | right found => exact ChildBounds.right_occurrences _ _ _ normalized.1 normalized.2 large found

theorem step_preserves (step : Step threshold k formula child added) (normalized : Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) (controlled : Controlled threshold formula layer) :
    Controlled threshold child layer := by
  by_cases same : added = layer
  · subst layer
    exact step_added step normalized large
  · intro literal
    cases step with
    | left found =>
      have candidate := (Selection.select_sound _ _ _ found).1
      exact Nat.le_trans (ChildBounds.left_unchanged _ _ _ _ literal normalized.2 candidate.1 same) (controlled literal)
    | right found =>
      have candidate := (Selection.select_sound _ _ _ found).1
      exact Nat.le_trans (ChildBounds.right_unchanged _ _ _ _ literal normalized.2 candidate.1 same) (controlled literal)

end WordRAM.Conjectures.Sparsification.Path