Prove2Me

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

Definition
SETHOV_Sparsification_14

by wurtle · Nov 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

fine-grained-complexityorthogonal-vectorssethsparsificationword-ram

Bundle 14 of the machine-checked formalization of the algorithmic sparsification transfer used in the proof that SETH implies the Orthogonal Vectors Conjecture on a concrete word RAM. It contains the combinatorial sparsification tree, clause normalization, leaf counting and the sparse-leaf solver bounds. The bundle is self-contained over the preceding bundles and the platform WordRAM definitions, and every declaration is proved with no axioms or placeholders.

Definition code
import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_13

set_option autoImplicit true

/-! Exact clause-count accounting for duplicate-free formulas. -/
namespace WordRAM.Conjectures.Sparsification.Ledger

def layer (formula : CNF n) (size : Nat) : CNF n :=
  formula.filter (fun clause => decide (clause.length = size))

def gained (old child : CNF n) (size : Nat) : Nat :=
  (layer (Additions.newClauses old child) size).length

def lost (old child : CNF n) (size : Nat) : Nat := gained child old size

theorem intersection_length (a b : CNF n) (nodupA : a.Nodup) (nodupB : b.Nodup) :
    (a.filter (fun clause => decide (clause ∈ b))).length =
      (b.filter (fun clause => decide (clause ∈ a))).length := by
  apply Nat.le_antisymm
  · apply List.Nodup.length_le_of_subset (nodupA.filter _)
    intro clause member
    obtain ⟨ha, hb⟩ := List.mem_filter.mp member
    exact List.mem_filter.mpr ⟨of_decide_eq_true hb, decide_eq_true ha⟩
  · apply List.Nodup.length_le_of_subset (nodupB.filter _)
    intro clause member
    obtain ⟨hb, ha⟩ := List.mem_filter.mp member
    exact List.mem_filter.mpr ⟨of_decide_eq_true ha, decide_eq_true hb⟩

theorem balance (old child : CNF n) (nodupOld : old.Nodup) (nodupChild : child.Nodup) :
    old.length + (Additions.newClauses old child).length =
      child.length + (Additions.newClauses child old).length := by
  have oldSplit := Branch.filter_lengths old (fun clause => decide (clause ∈ child))
  have childSplit := Branch.filter_lengths child (fun clause => decide (clause ∈ old))
  have same := intersection_length old child nodupOld nodupChild
  unfold Additions.newClauses
  omega

theorem new_layer (old child : CNF n) (size : Nat) :
    Additions.newClauses (layer old size) (layer child size) =
      layer (Additions.newClauses old child) size := by
  simp only [Additions.newClauses, layer, List.filter_filter]
  congr 1
  funext clause
  by_cases eq : clause.length = size <;> simp [eq]

/-- Clauses at a fixed size obey the exact additions/deletions identity. -/
theorem layer_balance (old child : CNF n) (size : Nat)
    (nodupOld : old.Nodup) (nodupChild : child.Nodup) :
    (layer old size).length + gained old child size =
      (layer child size).length + lost old child size := by
  have result := balance (layer old size) (layer child size) (nodupOld.filter _) (nodupChild.filter _)
  rw [new_layer, new_layer] at result
  exact result

def totalGained (initial : CNF n) : List (CNF n) → Nat → Nat
  | [], _ => 0
  | next :: rest, size => gained initial next size + totalGained next rest size

def totalLost (initial : CNF n) : List (CNF n) → Nat → Nat
  | [], _ => 0
  | next :: rest, size => lost initial next size + totalLost next rest size

def endpoint (initial : CNF n) : List (CNF n) → CNF n
  | [] => initial
  | next :: rest => endpoint next rest

/-- Telescoping the exact identity over a finite sequence of formula states. -/
theorem sequence_balance (initial : CNF n) (states : List (CNF n)) (size : Nat)
    (distinct : ∀ formula ∈ initial :: states, formula.Nodup) :
    (layer initial size).length + totalGained initial states size =
      (layer (endpoint initial states) size).length + totalLost initial states size := by
  induction states generalizing initial with
  | nil => simp [totalGained, totalLost, endpoint]
  | cons next rest ih =>
    have first := layer_balance initial next size (distinct initial (by simp)) (distinct next (by simp))
    have tail := ih next (fun formula member => distinct formula (List.mem_cons_of_mem _ member))
    simp only [totalGained, totalLost, endpoint]
    omega

/-- Bounding surviving clauses and deletions bounds all additions. -/
theorem totalGained_le (initial : CNF n) (states : List (CNF n)) (size : Nat)
    (distinct : ∀ formula ∈ initial :: states, formula.Nodup) :
    totalGained initial states size ≤
      (layer (endpoint initial states) size).length + totalLost initial states size := by
  have balance := sequence_balance initial states size distinct
  omega

end WordRAM.Conjectures.Sparsification.Ledger

/-! Exact per-step ledger entries for the verified sparsification branches. -/
namespace WordRAM.Conjectures.Sparsification.StepLedger

theorem new_member (formula retained added : CNF n) (retainedSub : retained ⊆ formula)
    (nodup : ∀ c ∈ retained ++ added, c.Nodup)
    (member : clause ∈ Additions.newClauses formula (Normalize.normalize (retained ++ added))) : clause ∈ added := by
  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 old | added
  · exact False.elim (absent (retainedSub old))
  · exact added

theorem new_uniform (step : Path.Step threshold k formula child added)
    (normalized : Path.Normalized formula)
    (member : clause ∈ Additions.newClauses formula child) : clause.length = added := by
  cases step with
  | @left size core found =>
    have candidate := (Selection.select_sound _ _ _ found).1
    have clean : ∀ c ∈ Branch.remaining formula core size ++ [core], c.Nodup := by
      intro c hc
      rcases List.mem_append.mp hc with hc | hc
      · exact normalized.2 c (List.mem_filter.mp hc).1
      · simpa only [List.mem_singleton.mp hc] using candidate.1
    have present := new_member formula (Branch.remaining formula core size) [core]
      (fun _ h => (List.mem_filter.mp h).1) clean member
    rw [List.mem_singleton.mp present]
  | @right size core found =>
    have candidate := (Selection.select_sound _ _ _ found).1
    have clean : ∀ c ∈ Branch.remaining formula core size ++
        (Flowers.family formula core size).map (Branch.petal core), c.Nodup := by
      intro c hc
      rcases List.mem_append.mp hc with hc | hc
      · exact normalized.2 c (List.mem_filter.mp hc).1
      · obtain ⟨original, present, rfl⟩ := List.mem_map.mp hc
        exact (normalized.2 original (List.mem_filter.mp present).1).filter _
    have present := new_member formula (Branch.remaining formula core size)
      ((Flowers.family formula core size).map (Branch.petal core))
      (fun _ h => (List.mem_filter.mp h).1) clean member
    obtain ⟨original, present, eq⟩ := List.mem_map.mp present
    obtain ⟨old, properties⟩ := List.mem_filter.mp present
    have properties := of_decide_eq_true properties
    have length := Branch.petal_length core original candidate.1 (normalized.2 original old) properties.2
    rw [eq] at length
    omega

theorem gained_eq (step : Path.Step threshold k formula child added) (normalized : Path.Normalized formula)
    (layer : Nat) : Ledger.gained formula child layer =
      if layer = added then (Additions.newClauses formula child).length else 0 := by
  unfold Ledger.gained Ledger.layer
  by_cases same : layer = added
  · rw [if_pos same]
    have eq : (Additions.newClauses formula child).filter (fun clause => decide (clause.length = layer)) =
        Additions.newClauses formula child := by
      apply List.filter_eq_self.mpr
      intro clause member
      exact decide_eq_true ((new_uniform step normalized member).trans same.symm)
    rw [eq]
  · rw [if_neg same]
    have eq : (Additions.newClauses formula child).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
      have eq := of_decide_eq_true eq
      exact same (eq.symm.trans (new_uniform step normalized present))
    rw [eq]
    rfl

theorem additions_positive (step : Path.Step threshold k formula child added) (normalized : Path.Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) : 0 < Ledger.gained formula child added := by
  rw [gained_eq step normalized, if_pos rfl]
  cases step with
  | left found => rw [Additions.core_count _ _ _ normalized large found]; decide
  | @right size core found =>
    rw [Additions.petal_count _ _ _ normalized found]
    have candidate := (Selection.select_sound _ _ _ found).1
    have lower := large (size - core.length)
    have enough := candidate.2.2.2
    omega

theorem lost_eq (formula child : CNF n) (layer : Nat) : Ledger.lost formula child layer =
    (formula.filter (fun clause => decide (clause.length = layer ∧ clause ∉ child))).length := by
  simp [Ledger.lost, Ledger.gained, Ledger.layer, Additions.newClauses, List.filter_filter]

theorem lost_zero (step : Path.Step threshold k formula child added) (normalized : Path.Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) (smaller : layer ≤ added) : Ledger.lost formula child layer = 0 := by
  rw [lost_eq]
  have empty : (formula.filter (fun clause => decide (clause.length = layer ∧ clause ∉ child))) = [] := by
    apply List.eq_nil_iff_forall_not_mem.mpr
    intro clause member
    obtain ⟨old, properties⟩ := List.mem_filter.mp member
    have properties := of_decide_eq_true properties
    cases step with
    | left found =>
      have strict := Additions.core_removal_size _ _ _ normalized large found old properties.2
      omega
    | right found =>
      have strict := Additions.petal_removal_size _ _ _ normalized found old properties.2
      omega
  rw [empty]
  rfl

/-- A deletion is charged to actual additions, all at the step's added size. -/
theorem lost_bound (step : Path.Step threshold k formula child added) (normalized : Path.Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) (controlled : Path.Controlled threshold formula layer) :
    Ledger.lost formula child layer ≤ Ledger.gained formula child added * (2 * threshold (layer - 1) - 1) := by
  rw [gained_eq step normalized, if_pos rfl, lost_eq]
  cases step with
  | left found =>
    rw [Additions.core_count _ _ _ normalized large found, Nat.one_mul]
    exact Deletion.left_removed _ _ _ _ normalized controlled found
  | @right size core found =>
    rw [Additions.petal_count _ _ _ normalized found]
    exact Deletion.right_removed _ _ _ _ normalized controlled found

/-- The priority rule already controls the added size immediately before its
first addition, even when the input has many clauses of other sizes. -/
theorem before_added (step : Path.Step threshold k formula child added) (normalized : Path.Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) : Path.Controlled threshold formula added := by
  intro literal
  cases step with
  | @left size core found =>
    have candidate := (Selection.select_sound _ _ _ found).1
    have bound := Occurrences.old_layer formula threshold k normalized.1 (large 0) found literal core.length
      candidate.2.1 candidate.2.2.1
    have lower := large (core.length - 1)
    omega
  | @right size core found =>
    have candidate := (Selection.select_sound _ _ _ found).1
    have positive := candidate.2.1
    have proper := candidate.2.2.1
    have bound := Occurrences.old_layer formula threshold k normalized.1 (large 0) found literal (size - core.length)
      (by omega) (by omega)
    have lower := large (size - core.length - 1)
    omega

end WordRAM.Conjectures.Sparsification.StepLedger

/-! Summing deletion charges over valid sequences of branching states. -/
namespace WordRAM.Conjectures.Sparsification.Charges

inductive Sequence (threshold : Nat → Nat) (k : Nat) : CNF n → List (CNF n) → Prop
  | nil (formula) : Sequence threshold k formula []
  | cons (step : Path.Step threshold k initial next added) (tail : Sequence threshold k next rest) :
      Sequence threshold k initial (next :: rest)

def below (old child : CNF n) (layer : Nat) : Nat :=
  ((List.range layer).map (Ledger.gained old child)).sum

def totalBelow (initial : CNF n) (states : List (CNF n)) (layer : Nat) : Nat :=
  ((List.range layer).map (Ledger.totalGained initial states)).sum

theorem member_le_sum (items : List Nat) (member : value ∈ items) : value ≤ items.sum := by
  induction items with
  | nil => simp at member
  | cons head rest ih =>
    rcases List.mem_cons.mp member with rfl | member
    · simp
    · have bound := ih member; simp only [List.sum_cons]; omega

theorem step_charge (step : Path.Step threshold k formula child added) (normalized : Path.Normalized formula)
    (large : ∀ i, 2 ≤ threshold i) (controlled : Path.Controlled threshold formula layer) :
    Ledger.lost formula child layer ≤ below formula child layer * (2 * threshold (layer - 1) - 1) := by
  by_cases smaller : added < layer
  · have inclusion := member_le_sum ((List.range layer).map (Ledger.gained formula child))
      (List.mem_map.mpr ⟨added, List.mem_range.mpr smaller, rfl⟩)
    exact Nat.le_trans (StepLedger.lost_bound step normalized large controlled)
      (Nat.mul_le_mul_right _ inclusion)
  · rw [StepLedger.lost_zero step normalized large (by omega)]
    exact Nat.zero_le _

theorem sum_add (items : List Nat) (f g : Nat → Nat) :
    (items.map (fun i => f i + g i)).sum = (items.map f).sum + (items.map g).sum := by
  induction items with
  | nil => simp
  | cons head rest ih => simp [ih, Nat.add_assoc, Nat.add_left_comm]

theorem totalBelow_cons (initial next : CNF n) (rest : List (CNF n)) (layer : Nat) :
    totalBelow initial (next :: rest) layer = below initial next layer + totalBelow next rest layer := by
  unfold totalBelow below
  simp only [Ledger.totalGained]
  exact sum_add _ _ _

theorem normalized_states (path : Sequence threshold k initial states) (normalized : Path.Normalized initial) :
    ∀ formula ∈ initial :: states, Path.Normalized formula := by
  induction path with
  | nil => intro formula member; simpa only [List.mem_singleton.mp member] using normalized
  | cons step tail ih =>
    intro formula member
    rcases List.mem_cons.mp member with eq | member
    · simpa only [eq] using normalized
    · exact ih (Path.step_normalized step) formula member

theorem endpoint_controlled (path : Sequence threshold k initial states) (normalized : Path.Normalized initial)
    (large : ∀ i, 2 ≤ threshold i) (controlled : Path.Controlled threshold initial layer) :
    Path.Controlled threshold (Ledger.endpoint initial states) layer := by
  induction path with
  | nil => exact controlled
  | cons step tail ih =>
    exact ih (Path.step_normalized step) (Path.step_preserves step normalized large controlled)

/-- Total deletions at a controlled size are charged to additions at smaller sizes. -/
theorem total_charge (path : Sequence threshold k initial states) (normalized : Path.Normalized initial)
    (large : ∀ i, 2 ≤ threshold i) (controlled : Path.Controlled threshold initial layer) :
    Ledger.totalLost initial states layer ≤ totalBelow initial states layer * (2 * threshold (layer - 1) - 1) := by
  induction path with
  | nil => simp [Ledger.totalLost]
  | cons step tail ih =>
    have first := step_charge step normalized large controlled
    have later := ih (Path.step_normalized step) (Path.step_preserves step normalized large controlled)
    rw [Ledger.totalLost, totalBelow_cons, Nat.add_mul]
    exact Nat.add_le_add first later

/-- The exact ledger and the deletion charges bound cumulative additions. -/
theorem additions_le (path : Sequence threshold k initial states) (normalized : Path.Normalized initial)
    (large : ∀ i, 2 ≤ threshold i) (controlled : Path.Controlled threshold initial layer) :
    Ledger.totalGained initial states layer ≤
      (Ledger.layer (Ledger.endpoint initial states) layer).length +
        totalBelow initial states layer * (2 * threshold (layer - 1) - 1) := by
  have distinct : ∀ formula ∈ initial :: states, formula.Nodup := fun formula member =>
    Additions.antichain_nodup formula (normalized_states path normalized formula member).1
  exact Nat.le_trans (Ledger.totalGained_le initial states layer distinct)
    (Nat.add_le_add_left (total_charge path normalized large controlled) _)

theorem endpoint_mem (initial : CNF n) (states : List (CNF n)) :
    Ledger.endpoint initial states ∈ initial :: states := by
  induction states generalizing initial with
  | nil => exact List.mem_cons_self
  | cons next rest ih => exact List.mem_cons_of_mem _ (ih next)

theorem controlled_layer_size (formula : CNF n) (normalized : Path.Normalized formula)
    (positive : 0 < layer) (controlled : Path.Controlled threshold formula layer) :
    (Ledger.layer formula layer).length ≤ (2 * (2 * threshold (layer - 1) - 1)) * n := by
  apply Counting.sparse _ (2 * threshold (layer - 1) - 1)
  · intro clause member
    exact normalized.2 clause (List.mem_filter.mp member).1
  · intro clause member empty
    have eq := of_decide_eq_true (List.mem_filter.mp member).2
    rw [empty] at eq
    simp only [List.length_nil] at eq
    omega
  · intro literal
    have eq : Counting.degree (Ledger.layer formula layer) literal = Counting.layerDegree formula literal layer := by
      unfold Counting.degree Ledger.layer Counting.layerDegree
      rw [List.filter_filter, List.filter_filter]
      congr 2
      funext clause
      exact Bool.and_comm _ _
    rw [eq]
    exact controlled literal

/-- Cumulative additions are linear in the variable count plus charges to
smaller additions, once the layer is controlled at the starting state. -/
theorem additions_recurrence (initial : CNF n) (states : List (CNF n)) (path : Sequence threshold k initial states) (normalized : Path.Normalized initial)
    (large : ∀ i, 2 ≤ threshold i) (positive : 0 < layer)
    (controlled : Path.Controlled threshold initial layer) :
    Ledger.totalGained initial states layer ≤
      (2 * (2 * threshold (layer - 1) - 1)) * n +
        totalBelow initial states layer * (2 * threshold (layer - 1) - 1) := by
  have finalNormalized := normalized_states path normalized _ (endpoint_mem initial states)
  have survivors := controlled_layer_size _ finalNormalized positive (endpoint_controlled path normalized large controlled)
  exact Nat.le_trans (additions_le path normalized large controlled) (Nat.add_le_add_right survivors _)

/-- The cumulative recurrence needs no occurrence assumption on the input:
skip the prefix before this size is first added, then use priority to establish
control at the start of the charged suffix. -/
theorem additions_recurrence_unconditional (initial : CNF n) (states : List (CNF n))
    (path : Sequence threshold k initial states) (normalized : Path.Normalized initial)
    (large : ∀ i, 2 ≤ threshold i) (positive : 0 < layer) :
    Ledger.totalGained initial states layer ≤
      (2 * (2 * threshold (layer - 1) - 1)) * n +
        totalBelow initial states layer * (2 * threshold (layer - 1) - 1) := by
  induction path with
  | nil => simp [Ledger.totalGained]
  | @cons initial next added rest step tail ih =>
    by_cases same : layer = added
    · have controlled := StepLedger.before_added step normalized large
      rw [← same] at controlled
      exact additions_recurrence initial (next :: rest) (Sequence.cons step tail) normalized large positive controlled
    · have noGain : Ledger.gained initial next layer = 0 := by
        rw [StepLedger.gained_eq step normalized, if_neg same]
      rw [Ledger.totalGained, noGain, Nat.zero_add, totalBelow_cons]
      have later := ih (Path.step_normalized step)
      apply Nat.le_trans later
      apply Nat.add_le_add_left
      apply Nat.mul_le_mul_right
      omega

end WordRAM.Conjectures.Sparsification.Charges
Source
Impagliazzo, Paturi and Zane, Which problems have strongly exponential complexity?, J. Comput. Syst. Sci. 63(4):512–530, 2001, Corollary 1 (p. 523), https://doi.org/10.1006/jcss.2001.1774; user-supplied WordRAM project, git commit 68be5b4418cf34d8d990686d0b9c09a85cfc641b (sparsification transfer development).

View graph