SETH ⇒ OVC sparsification bundle 15: 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_14

set_option autoImplicit true

/-! Explicit thresholds and a solution of the cumulative-addition recurrence. -/
namespace WordRAM.Conjectures.Sparsification.Thresholds

structure Parameters where
  cumulative : Nat
  coefficient : Nat
  threshold : Nat
  deriving Repr, DecidableEq

/-- At positive sizes the threshold is `a` times the addition coefficient.
The zero layer has no additions, and its threshold is the base constant two. -/
def parameters (a : Nat) : Nat → Parameters
  | 0 => ⟨0, 0, 2⟩
  | i + 1 =>
    let previous := parameters a i
    let cumulative := previous.cumulative + previous.coefficient
    let coefficient := (2 * previous.threshold - 1) * (2 + cumulative)
    ⟨cumulative, coefficient, a * coefficient⟩

def threshold (a i : Nat) : Nat := (parameters a i).threshold

def coefficient (a i : Nat) : Nat := (parameters a i).coefficient

def cumulative (a i : Nat) : Nat := (parameters a i).cumulative

theorem prefix_succ (a i : Nat) : cumulative a (i + 1) = cumulative a i + coefficient a i := rfl

theorem coefficient_succ (a i : Nat) :
    coefficient a (i + 1) = (2 * threshold a i - 1) * (2 + cumulative a (i + 1)) := rfl

theorem threshold_succ (a i : Nat) : threshold a (i + 1) = a * coefficient a (i + 1) := rfl

theorem threshold_large (a : Nat) (positive : 1 ≤ a) (i : Nat) : 2 ≤ threshold a i := by
  induction i with
  | zero => change 2 ≤ 2; decide
  | succ i ih =>
    rw [threshold_succ, coefficient_succ]
    have cap : 1 ≤ 2 * threshold a i - 1 := by omega
    have first : 2 ≤ (2 * threshold a i - 1) * (2 + cumulative a (i + 1)) :=
      Nat.le_trans (by omega) (Nat.le_mul_of_pos_left _ cap)
    exact Nat.le_trans first (Nat.le_mul_of_pos_left _ positive)

theorem added_size (step : Path.Step thresholds k formula child added) : 0 < added ∧ added < k := by
  cases step with
  | left found =>
    have candidate := Selection.select_sound _ _ _ found
    have positive := candidate.1.2.1
    have proper := candidate.1.2.2.1
    omega
  | right found =>
    have candidate := Selection.select_sound _ _ _ found
    have positive := candidate.1.2.1
    have proper := candidate.1.2.2.1
    omega

theorem zero_additions (path : Charges.Sequence thresholds k initial states) (normalized : Path.Normalized initial) :
    Ledger.totalGained initial states 0 = 0 := by
  induction path with
  | nil => rfl
  | cons step tail ih =>
    have positive := (added_size step).1
    rw [Ledger.totalGained, StepLedger.gained_eq step normalized, if_neg (by omega), Nat.zero_add]
    exact ih (Path.step_normalized step)

theorem below_succ (initial : CNF n) (states : List (CNF n)) (i : Nat) :
    Charges.totalBelow initial states (i + 1) =
      Charges.totalBelow initial states i + Ledger.totalGained initial states i := by
  simp [Charges.totalBelow, List.range_succ]

/-- Prefix counts and counts at the next size are bounded simultaneously. -/
theorem addition_bounds (a : Nat) (positive : 1 ≤ a) (initial : CNF n) (states : List (CNF n))
    (path : Charges.Sequence (threshold a) k initial states) (normalized : Path.Normalized initial) (i : Nat) :
    Charges.totalBelow initial states i ≤ cumulative a i * n ∧
      Ledger.totalGained initial states i ≤ coefficient a i * n := by
  induction i with
  | zero => simp [Charges.totalBelow, cumulative, coefficient, parameters, zero_additions path normalized]
  | succ i ih =>
    have prefixBound : Charges.totalBelow initial states (i + 1) ≤ cumulative a (i + 1) * n := by
      rw [below_succ, prefix_succ, Nat.add_mul]
      exact Nat.add_le_add ih.1 ih.2
    refine ⟨prefixBound, ?_⟩
    have recurrence := Charges.additions_recurrence_unconditional initial states path normalized
      (threshold_large a positive) (by omega : 0 < i + 1)
    simp only [Nat.add_sub_cancel] at recurrence
    have scaled := Nat.mul_le_mul_right (2 * threshold a i - 1) prefixBound
    apply Nat.le_trans recurrence
    rw [coefficient_succ]
    calc
      2 * (2 * threshold a i - 1) * n + Charges.totalBelow initial states (i + 1) * (2 * threshold a i - 1)
          ≤ 2 * (2 * threshold a i - 1) * n + (cumulative a (i + 1) * n) * (2 * threshold a i - 1) := Nat.add_le_add_left scaled _
      _ = (2 * threshold a i - 1) * (2 + cumulative a (i + 1)) * n := by
        simp [Nat.mul_add, Nat.add_mul, Nat.mul_assoc, Nat.mul_comm]

theorem coefficient_positive (a : Nat) (positive : 1 ≤ a) (i : Nat) (sizePositive : 0 < i) :
    0 < coefficient a i := by
  cases i with
  | zero => omega
  | succ i =>
    rw [coefficient_succ]
    have large := threshold_large a positive i
    exact Nat.mul_pos (by omega) (by omega)

theorem path_length_le_additions (path : Charges.Sequence thresholds k initial states)
    (normalized : Path.Normalized initial) (large : ∀ i, 2 ≤ thresholds i) :
    states.length ≤ Charges.totalBelow initial states k := by
  induction path with
  | nil => simp
  | @cons initial next added rest step tail ih =>
    have addedBound := (added_size step).2
    have positive := StepLedger.additions_positive step normalized large
    have contribution := Charges.member_le_sum ((List.range k).map (Ledger.gained initial next))
      (List.mem_map.mpr ⟨added, List.mem_range.mpr addedBound, rfl⟩)
    have later := ih (Path.step_normalized step)
    rw [Charges.totalBelow_cons]
    change Ledger.gained initial next added ≤ Charges.below initial next k at contribution
    simp only [List.length_cons]
    omega

theorem path_length (a : Nat) (positive : 1 ≤ a) (initial : CNF n) (states : List (CNF n))
    (path : Charges.Sequence (threshold a) k initial states) (normalized : Path.Normalized initial) :
    states.length ≤ cumulative a k * n :=
  Nat.le_trans (path_length_le_additions path normalized (threshold_large a positive))
    (addition_bounds a positive initial states path normalized k).1

end WordRAM.Conjectures.Sparsification.Thresholds

/-! Branch histories retain which choices were petal branches. -/
namespace WordRAM.Conjectures.Sparsification.RareBranches

/-- A record stores the added clause size and whether this was a petal branch. -/
inductive History (threshold : Nat → Nat) (k : Nat) : CNF n → List (CNF n) → List (Nat × Bool) → Prop
  | nil (formula) : History threshold k formula [] []
  | left (found : Selection.select formula threshold k = some (size, core))
      (tail : History threshold k (Branch.left formula core size) states records) :
      History threshold k formula (Branch.left formula core size :: states) ((core.length, false) :: records)
  | right (found : Selection.select formula threshold k = some (size, core))
      (tail : History threshold k (Branch.right formula core size) states records) :
      History threshold k formula (Branch.right formula core size :: states) ((size - core.length, true) :: records)

def countAt (records : List (Nat × Bool)) (layer : Nat) : Nat :=
  (records.filter (fun record => record.2 && decide (record.1 = layer))).length

theorem sequence (history : History threshold k initial states records) : Charges.Sequence threshold k initial states := by
  induction history with
  | nil => exact .nil _
  | left found tail ih => exact .cons (.left found) ih
  | right found tail ih => exact .cons (.right found) ih

theorem record_length (history : History threshold k initial states records) : records.length = states.length := by
  induction history with
  | nil => rfl
  | left found tail ih => simp only [List.length_cons, ih]
  | right found tail ih => simp only [List.length_cons, ih]

/-- Each petal branch at size i purchases at least threshold(i) new clauses. -/
theorem charge (history : History threshold k initial states records) (normalized : Path.Normalized initial) (layer : Nat) :
    threshold layer * countAt records layer ≤ Ledger.totalGained initial states layer := by
  induction history with
  | nil => simp [countAt, Ledger.totalGained]
  | left found tail ih =>
    have later := ih (Path.step_normalized (Path.Step.left found))
    simp only [countAt, List.filter_cons, Bool.false_and, Bool.false_eq_true, if_false, Ledger.totalGained]
    unfold countAt at later
    omega
  | @right formula size core states records found tail ih =>
    have later := ih (Path.step_normalized (Path.Step.right found))
    by_cases same : size - core.length = layer
    · have gain : Ledger.gained formula (Branch.right formula core size) layer = (Flowers.family formula core size).length := by
        rw [StepLedger.gained_eq (Path.Step.right found) normalized, if_pos same.symm,
          Additions.petal_count formula threshold k normalized found]
      have enough := (Selection.select_sound formula threshold k found).1.2.2.2
      rw [same] at enough
      simp only [countAt, List.filter_cons, same, decide_true, Bool.true_and, if_true, List.length_cons,
        Ledger.totalGained, gain, Nat.mul_add, Nat.mul_one]
      unfold countAt at later
      omega
    · simp only [countAt, List.filter_cons, decide_eq_false same, Bool.true_and, Bool.false_eq_true, if_false,
        Ledger.totalGained]
      unfold countAt at later
      omega

/-- With the chosen thresholds, petal branches at any positive size are rare. -/
theorem rare_at (a : Nat) (positive : 1 ≤ a) (initial : CNF n) (states : List (CNF n))
    (history : History (Thresholds.threshold a) k initial states records) (normalized : Path.Normalized initial)
    (layer : Nat) (layerPositive : 0 < layer) : a * countAt records layer ≤ n := by
  have charged := charge history normalized layer
  have bounded := (Thresholds.addition_bounds a positive initial states (sequence history) normalized layer).2
  have combined := Nat.le_trans charged bounded
  have coeffPositive := Thresholds.coefficient_positive a positive layer layerPositive
  have eq : Thresholds.threshold a layer = a * Thresholds.coefficient a layer := by
    cases layer with
    | zero => omega
    | succ i => exact Thresholds.threshold_succ a i
  rw [eq] at combined
  have scaled : Thresholds.coefficient a layer * (a * countAt records layer) ≤ Thresholds.coefficient a layer * n := by
    simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using combined
  exact Nat.le_of_mul_le_mul_left scaled coeffPositive

theorem record_size (history : History threshold k initial states records) (member : record ∈ records) :
    0 < record.1 ∧ record.1 < k := by
  induction history with
  | nil => simp at member
  | left found tail ih =>
    rcases List.mem_cons.mp member with eq | member
    · rw [eq]; exact Thresholds.added_size (Path.Step.left found)
    · exact ih member
  | right found tail ih =>
    rcases List.mem_cons.mp member with eq | member
    · rw [eq]; exact Thresholds.added_size (Path.Step.right found)
    · exact ih member

def petalCount (records : List (Nat × Bool)) : Nat := (records.filter Prod.snd).length

/-- The total number of petal choices over all clause sizes is small. -/
theorem rare_total (a : Nat) (positive : 1 ≤ a) (initial : CNF n) (states : List (CNF n))
    (history : History (Thresholds.threshold a) k initial states records) (normalized : Path.Normalized initial) :
    petalCount records ≤ k * (n / a) := by
  apply Counting.length_le_buckets (records.filter Prod.snd) Prod.fst k (n / a)
  · intro record member
    have bounds := record_size history (List.mem_filter.mp member).1
    exact ⟨bounds.1, Nat.le_of_lt bounds.2⟩
  · intro layer layerPositive _
    have bound := rare_at a positive initial states history normalized layer layerPositive
    have divided : countAt records layer ≤ n / a :=
      (Nat.le_div_iff_mul_le (by omega)).mpr (by simpa only [Nat.mul_comm] using bound)
    simpa only [countAt, List.filter_filter, Bool.and_comm] using divided

end WordRAM.Conjectures.Sparsification.RareBranches

/-! Branch codes retain the multiplicity of returned leaves. -/
namespace WordRAM.Conjectures.Sparsification.Codes

def prepend (bit : Bool) (entries : List (List Bool × CNF n)) : List (List Bool × CNF n) :=
  entries.map (fun entry => (bit :: entry.1, entry.2))

def leaves (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    List (List Bool × CNF n) :=
  let normalized := Normalize.normalize formula
  if [] ∈ normalized then []
  else match _found : Selection.select normalized threshold k with
    | none => [([], normalized)]
    | some (size, core) =>
      prepend false (leaves (Branch.left normalized core size) threshold k large) ++
        prepend true (leaves (Branch.right normalized core size) threshold k large)
termination_by weight formula
decreasing_by
  · exact (Tree.selected_smaller formula threshold k large _found).1
  · exact (Tree.selected_smaller formula threshold k large _found).2

theorem empty_eq (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (empty : [] ∈ Normalize.normalize formula) : leaves formula threshold k large = [] := by
  rw [leaves]; simp only [if_pos empty]

theorem none_eq (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (nonempty : [] ∉ Normalize.normalize formula)
    (found : Selection.select (Normalize.normalize formula) threshold k = none) :
    leaves formula threshold k large = [([], Normalize.normalize formula)] := by
  rw [leaves]; simp only [if_neg nonempty]
  split
  · rfl
  · rename_i size core selected
    rw [found] at selected
    contradiction

theorem some_eq (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (nonempty : [] ∉ Normalize.normalize formula)
    (found : Selection.select (Normalize.normalize formula) threshold k = some (size, core)) :
    leaves formula threshold k large =
      prepend false (leaves (Branch.left (Normalize.normalize formula) core size) threshold k large) ++
        prepend true (leaves (Branch.right (Normalize.normalize formula) core size) threshold k large) := by
  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
    rfl

/-- Erasing codes returns exactly the original leaf list, including duplicates. -/
theorem erase (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    (leaves formula threshold k large).map Prod.snd = Tree.leaves formula threshold k large := by
  induction formula using Tree.leaves.induct threshold k large with
  | case1 formula normalized empty =>
    dsimp only [normalized] at *
    rw [empty_eq formula threshold k large empty, Tree.leaves]
    simp only [if_pos empty, List.map_nil]
  | case2 formula normalized nonempty found =>
    dsimp only [normalized] at *
    rw [none_eq formula threshold k large nonempty found, Tree.leaves]
    simp only [if_neg nonempty]
    split
    · rfl
    · rename_i size core selected
      rw [found] at selected
      contradiction
  | case3 formula normalized nonempty size core found leftIH rightIH =>
    dsimp only [normalized] at *
    rw [some_eq formula threshold k large nonempty found, Tree.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.map_append, prepend, List.map_map, Function.comp_def]
      rw [leftIH, rightIH]

def PrefixFree (words : List (List Bool)) : Prop :=
  words.Pairwise (fun a b => ¬ List.IsPrefix a b ∧ ¬ List.IsPrefix b a)

theorem fork_prefixFree (left right : List (List Bool)) (hl : PrefixFree left) (hr : PrefixFree right) :
    PrefixFree (left.map (false :: ·) ++ right.map (true :: ·)) := by
  apply List.pairwise_append.mpr
  refine ⟨?_, ?_, ?_⟩
  · apply List.pairwise_map.mpr
    simpa only [PrefixFree, List.cons_prefix_cons, true_and] using hl
  · apply List.pairwise_map.mpr
    simpa only [PrefixFree, List.cons_prefix_cons, true_and] using hr
  · intro a ha b hb
    obtain ⟨a, _, rfl⟩ := List.mem_map.mp ha
    obtain ⟨b, _, rfl⟩ := List.mem_map.mp hb
    simp only [List.cons_prefix_cons, Bool.false_eq_true, Bool.true_eq_false, false_and, not_false_eq_true, and_self]

/-- No returned branch code is a prefix of another. -/
theorem prefix_free (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    PrefixFree ((leaves formula threshold k large).map Prod.fst) := by
  induction formula using Tree.leaves.induct threshold k large with
  | case1 formula normalized empty =>
    rw [empty_eq formula threshold k large empty]
    exact List.Pairwise.nil
  | case2 formula normalized nonempty found =>
    rw [none_eq formula threshold k large nonempty found]
    exact List.pairwise_singleton _ _
  | case3 formula normalized nonempty size core found leftIH rightIH =>
    rw [some_eq formula threshold k large nonempty found]
    simpa only [List.map_append, prepend, List.map_map, Function.comp_def] using fork_prefixFree _ _ leftIH rightIH

theorem code_count (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    ((leaves formula threshold k large).map Prod.fst).length = (Tree.leaves formula threshold k large).length := by
  have eq := congrArg List.length (erase formula threshold k large)
  simpa only [List.length_map] using eq

theorem history (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (member : entry ∈ leaves formula threshold k large) :
    ∃ states records, RareBranches.History threshold k (Normalize.normalize formula) states records ∧
      Ledger.endpoint (Normalize.normalize formula) states = entry.2 ∧ records.map Prod.snd = entry.1 := by
  induction formula using Tree.leaves.induct threshold k large generalizing entry with
  | case1 formula normalized =>
    rename_i empty
    rw [empty_eq formula threshold k large empty] at member
    simp at member
  | case2 formula normalized nonempty =>
    rename_i found
    rw [none_eq formula threshold k large nonempty found] at member
    have eq := List.mem_singleton.mp member
    subst entry
    exact ⟨[], [], RareBranches.History.nil _, rfl, rfl⟩
  | case3 formula normalized nonempty size core found leftIH =>
    rename_i rightIH
    rw [some_eq formula threshold k large nonempty found] at member
    rcases List.mem_append.mp member with member | member
    · obtain ⟨childEntry, childMember, rfl⟩ := List.mem_map.mp member
      obtain ⟨states, records, path, endpoint, bits⟩ := leftIH childMember
      have childEq : Normalize.normalize (Branch.left (Normalize.normalize formula) core size) = Branch.left (Normalize.normalize formula) core size :=
        Normalize.normalize_idempotent _
      rw [childEq] at path endpoint
      refine ⟨Branch.left (Normalize.normalize formula) core size :: states, (core.length, false) :: records,
        RareBranches.History.left found path, endpoint, ?_⟩
      simp only [List.map_cons, bits]
    · obtain ⟨childEntry, childMember, rfl⟩ := List.mem_map.mp member
      obtain ⟨states, records, path, endpoint, bits⟩ := rightIH childMember
      have childEq : Normalize.normalize (Branch.right (Normalize.normalize formula) core size) = Branch.right (Normalize.normalize formula) core size :=
        Normalize.normalize_idempotent _
      rw [childEq] at path endpoint
      refine ⟨Branch.right (Normalize.normalize formula) core size :: states, (size - core.length, true) :: records,
        RareBranches.History.right found path, endpoint, ?_⟩
      simp only [List.map_cons, bits]

def ones (word : List Bool) : Nat := (word.filter id).length

theorem ones_records (records : List (Nat × Bool)) : ones (records.map Prod.snd) = RareBranches.petalCount records := by
  induction records with
  | nil => rfl
  | cons record rest ih =>
    cases eq : record.2 <;> simp_all [ones, RareBranches.petalCount]

/-- The length and weight bounds belong to each particular leaf code. -/
theorem bounds (a : Nat) (positive : 1 ≤ a) (formula : CNF n) (k : Nat)
    (member : entry ∈ leaves formula (Thresholds.threshold a) k (Thresholds.threshold_large a positive)) :
    entry.1.length ≤ Thresholds.cumulative a k * n ∧ ones entry.1 ≤ k * (n / a) := by
  obtain ⟨states, records, path, _, bits⟩ := history formula (Thresholds.threshold a) k
    (Thresholds.threshold_large a positive) member
  have normalized : Path.Normalized (Normalize.normalize formula) :=
    ⟨Normalize.normalize_antichain formula, Normalize.normalize_nodup_literals formula⟩
  constructor
  · rw [← bits, List.length_map, RareBranches.record_length path]
    exact Thresholds.path_length a positive _ states (RareBranches.sequence path) normalized
  · rw [← bits, ones_records]
    exact RareBranches.rare_total a positive _ states path normalized

end WordRAM.Conjectures.Sparsification.Codes