SETH ⇒ OVC sparsification bundle 48: 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_47

set_option autoImplicit true

namespace WordRAM.Conjectures.Sparsification.LeafProperties

theorem normalized (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    ∀ leaf ∈ Tree.leaves formula threshold k large, Normalize.normalize leaf = leaf := by
  induction formula using Tree.leaves.induct threshold k large with
  | case1 formula normalized empty =>
    dsimp only [normalized] at *
    intro leaf member
    rw [Tree.leaves] at member
    simp only [if_pos empty, List.not_mem_nil] at member
  | case2 formula normalized nonempty found =>
    dsimp only [normalized] at *
    intro leaf member
    rw [Tree.leaves] at member
    simp only [if_neg nonempty] at member
    split at member
    · have eq := List.mem_singleton.mp member
      subst leaf
      exact Normalize.normalize_idempotent formula
    · rename_i size core selected
      rw [found] at selected
      contradiction
  | case3 formula normalized nonempty size core found leftIH rightIH =>
    dsimp only [normalized] at *
    intro leaf member
    rw [Tree.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 leaf member
      · exact rightIH leaf member

theorem nodup (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (leaf : CNF n) (member : leaf ∈ Tree.leaves formula threshold k large) :
    ∀ clause ∈ leaf, clause.Nodup := by
  have h := Normalize.normalize_nodup_literals leaf
  rw [normalized formula threshold k large leaf member] at h
  exact h

end WordRAM.Conjectures.Sparsification.LeafProperties

/-! Obtain actual canonical-leaf solver executions and a common time bound from
fast sparse SAT. The finite maximum also handles inputs below the asymptotic cutoff. -/
namespace WordRAM.Conjectures.Sparsification.SparseSolver

private theorem uniform_times (xs : List α) (q bound : Nat) (positive : 0 < q) (enabled : Prop)
    (decision : α → Nat → Prop)
    (calls : ∀ x ∈ xs, ∃ time, decision x time ∧ (enabled → time ^ q ≤ bound)) :
    ∃ time, (∀ x ∈ xs, ∃ t, decision x t ∧ t ≤ time) ∧ (enabled → time ^ q ≤ bound) := by
  induction xs with
  | nil =>
    refine ⟨0, by simp, ?_⟩
    intro _; rw [Nat.zero_pow positive]; exact Nat.zero_le _
  | cons x xs ih =>
    obtain ⟨head, headDecision, headBound⟩ := calls x (by simp)
    obtain ⟨tail, tailDecisions, tailBound⟩ := ih (fun y hy => calls y (by simp [hy]))
    refine ⟨max head tail, ?_, ?_⟩
    · intro y hy
      rcases List.mem_cons.mp hy with eq | member
      · subst y; exact ⟨head, headDecision, Nat.le_max_left _ _⟩
      · obtain ⟨t, decision, le⟩ := tailDecisions y member
        exact ⟨t, decision, Nat.le_trans le (Nat.le_max_right _ _)⟩
    · intro h
      by_cases le : head ≤ tail
      · rw [Nat.max_eq_right le]; exact tailBound h
      · rw [Nat.max_eq_left (by omega)]; exact headBound h

theorem leaf_times (tuning k q : Nat) (positive : 0 < q)
    (solver : Algorithm) (C p n₀ : Nat)
    (fast : ∀ f : SATInstance, f.IsKCNF k → f.clauses.length ≤ Combinatorial.density tuning k * f.variables →
      ∃ t, DecidesIn solver f.encode f.variables t f.Satisfiable ∧
        (n₀ ≤ f.variables → t ^ q ≤ C * 2 ^ ((q - 1) * f.variables) * (f.encode.length + 1) ^ p))
    (formula : CNF n) (width : ∀ clause ∈ formula, clause.length ≤ k) :
    ∃ time,
      (∀ leaf ∈ Combinatorial.output tuning k formula, ∃ t,
        DecidesIn solver (LeafCall.satInput leaf).encode n t (LeafCall.satInput leaf).Satisfiable ∧ t ≤ time) ∧
      (n₀ ≤ n → time ^ q ≤ C * 2 ^ ((q - 1) * n) *
        (EncodingBounds.lengthBound k (Combinatorial.density tuning k) n + 1) ^ p) := by
  apply uniform_times _ q _ positive (n₀ ≤ n)
    (fun leaf time => DecidesIn solver (LeafCall.satInput leaf).encode n time (LeafCall.satInput leaf).Satisfiable)
  intro leaf member
  obtain ⟨leafWidth, leafSparse⟩ := Combinatorial.sparse_outputs tuning k formula width leaf member
  obtain ⟨time, decision, bound⟩ := fast (LeafCall.satInput leaf) (Canonical.width leaf leafWidth)
    (by simpa only [LeafCall.satInput, Canonical.formula_length] using leafSparse)
  refine ⟨time, decision, ?_⟩
  intro large
  have runtime := bound large
  have length := EncodingBounds.canonical_length leaf leafWidth leafSparse
  exact Nat.le_trans runtime (Nat.mul_le_mul_left _ (Nat.pow_le_pow_left (by omega) p))

/-- The solver and constants are fixed before the input formula is chosen. -/
theorem from_fast (tuning k q : Nat) (positive : 0 < q)
    (fast : HasFastSparseSAT k (Combinatorial.density tuning k) q) :
    ∃ (solver : Algorithm) (C p n₀ : Nat), 0 < C ∧
      ∀ (n : Nat) (formula : CNF n), (∀ clause ∈ formula, clause.length ≤ k) →
        ∃ time,
          (∀ leaf ∈ Combinatorial.output tuning k formula, ∃ t,
            DecidesIn solver (LeafCall.satInput leaf).encode n t (LeafCall.satInput leaf).Satisfiable ∧ t ≤ time) ∧
          (n₀ ≤ n → time ^ q ≤ C * 2 ^ ((q - 1) * n) *
            (EncodingBounds.lengthBound k (Combinatorial.density tuning k) n + 1) ^ p) := by
  obtain ⟨solver, C, p, n₀, positiveC, fast⟩ := fast
  exact ⟨solver, C, p, n₀, positiveC, fun _ formula width => leaf_times tuning k q positive solver C p n₀ fast formula width⟩

end WordRAM.Conjectures.Sparsification.SparseSolver

/-! Concrete uniform per-leaf budgets from sparse solver executions. -/
namespace WordRAM.Conjectures.Sparsification.LeafBudgets
open EncodingBounds

def bits (solver : Algorithm) (k density n : Nat) : Nat :=
  solver.wordFactor * (n + magnitudeBound k density n + 1)

def reserve (solver : Algorithm) (k density n : Nat) : Nat :=
  max (2 ^ bits solver k density n) (SimulationBounds.programBound solver.code + 1) +
    (3 + density * n * (1 + 4 * n))

def cost (k density n time : Nat) : Nat :=
  density * n * (22 * n + 29) + 7 * lengthBound k density n +
    4 * magnitudeBound k density n + 19 * time + 50

theorem eligible (solver : Algorithm) (k density time : Nat) (formula : CNF n)
    (width : ∀ clause ∈ formula, clause.length ≤ k) (sparse : formula.length ≤ density * n)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (fits : bits solver k density n ≤ w.bits)
    (decision : ∃ t, DecidesIn solver (LeafCall.satInput formula).encode n t (LeafCall.satInput formula).Satisfiable ∧ t ≤ time) :
    LeafLoop.Eligible solver w (cost k density n time) (reserve solver k density n) formula := by
  have len := canonical_length formula width sparse
  have magnitude := canonical_magnitude formula width sparse
  have logarithm := Nat.le_trans (Nat.log2_le_self (inputMagnitude (LeafCall.satInput formula).encode)) magnitude
  have wordBound : (solver.width (LeafCall.satInput formula).encode n).bits ≤ bits solver k density n := by
    exact Nat.mul_le_mul_left _ (by omega)
  have footprint : SimulationFootprint.span (solver.width (LeafCall.satInput formula).encode n) solver.code ≤
      reserve solver k density n := by
    have powered := Nat.pow_le_pow_right (n := 2) (by decide) wordBound
    unfold SimulationFootprint.span reserve
    omega
  have serialize := Nat.mul_le_mul_right (1 + 4 * n) sparse
  refine ⟨nodup, Nat.le_trans wordBound fits, footprint, ?_, ?_⟩
  · unfold reserve; omega
  · obtain ⟨t, decision, bound⟩ := decision
    refine ⟨t, decision, ?_⟩
    have clauses := Nat.mul_le_mul_right (22 * n + 29) sparse
    have lengths := Nat.mul_le_mul_left 7 len
    have logs := Nat.mul_le_mul_left 4 logarithm
    have calls := Nat.mul_le_mul_left 19 bound
    unfold cost
    omega

/-- All generated leaves meet the machine loop's requirements, provided its
single uniform word-width bound fits. The execution-time maximum is finite even
below the asymptotic cutoff. -/
theorem from_fast (tuning k q : Nat) (positive : 0 < q)
    (fast : HasFastSparseSAT k (Combinatorial.density tuning k) q) :
    ∃ (solver : Algorithm) (C p n₀ : Nat), 0 < C ∧
      ∀ (n : Nat) (formula : CNF n), (∀ clause ∈ formula, clause.length ≤ k) →
        ∃ time,
          (∀ (w : Width), bits solver k (Combinatorial.density tuning k) n ≤ w.bits →
            ∀ leaf ∈ Combinatorial.output tuning k formula,
              LeafLoop.Eligible solver w (cost k (Combinatorial.density tuning k) n time)
                (reserve solver k (Combinatorial.density tuning k) n) leaf) ∧
          (n₀ ≤ n → time ^ q ≤ C * 2 ^ ((q - 1) * n) *
            (lengthBound k (Combinatorial.density tuning k) n + 1) ^ p) := by
  obtain ⟨solver, C, p, n₀, positiveC, calls⟩ := SparseSolver.from_fast tuning k q positive fast
  refine ⟨solver, C, p, n₀, positiveC, ?_⟩
  intro n formula width
  obtain ⟨time, decisions, bound⟩ := calls n formula width
  refine ⟨time, ?_, bound⟩
  intro w fits leaf member
  obtain ⟨leafWidth, sparse⟩ := Combinatorial.sparse_outputs tuning k formula width leaf member
  exact eligible solver k _ time leaf leafWidth sparse
    (LeafProperties.nodup formula _ k _ leaf member) fits (decisions leaf member)

end WordRAM.Conjectures.Sparsification.LeafBudgets

/-! Elementary exponential envelopes for the concrete memory budgets. -/
namespace WordRAM.Conjectures.Sparsification.PowerBudget

theorem self (n : Nat) : n ≤ 2 ^ n := Nat.le_of_lt (Nat.lt_pow_self (by decide))

theorem add (x y a b : Nat) (hx : x ≤ 2 ^ a) (hy : y ≤ 2 ^ b) :
    x + y ≤ 2 ^ (a + b + 1) := by
  have left := Nat.le_trans hx (Nat.pow_le_pow_right (n := 2) (by decide) (Nat.le_add_right a b))
  have right := Nat.le_trans hy (Nat.pow_le_pow_right (n := 2) (by decide) (Nat.le_add_left b a))
  rw [Nat.pow_succ]
  omega

theorem mul (x y a b : Nat) (hx : x ≤ 2 ^ a) (hy : y ≤ 2 ^ b) :
    x * y ≤ 2 ^ (a + b) := by
  rw [Nat.pow_add]
  exact Nat.mul_le_mul hx hy

def leafSlope (solver : Algorithm) (k density : Nat) : Nat :=
  solver.wordFactor * (2 + 2 * density * (1 + 2 * k) + k + 7)

theorem leaf_bits (solver : Algorithm) (k density n : Nat) :
    LeafBudgets.bits solver k density n ≤ leafSlope solver k density * (n + 1) := by
  unfold LeafBudgets.bits leafSlope
  rw [Nat.mul_assoc]
  apply Nat.mul_le_mul_left
  simp only [EncodingBounds.magnitudeBound, EncodingBounds.lengthBound,
    Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul,
    Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]
  omega

def leafReserveSlope (solver : Algorithm) (k density : Nat) : Nat :=
  leafSlope solver k density + (SimulationBounds.programBound solver.code + 1) + density + 13

theorem leaf_reserve (solver : Algorithm) (k density n : Nat) :
    LeafBudgets.reserve solver k density n ≤ 2 ^ (leafReserveSlope solver k density * (n + 1)) := by
  let fixed := SimulationBounds.programBound solver.code + 1
  let bits := LeafBudgets.bits solver k density n
  have maxBound : max (2 ^ bits) fixed ≤ 2 ^ (bits + fixed) := by
    have left := Nat.pow_le_pow_right (n := 2) (by decide) (Nat.le_add_right bits fixed)
    have right := Nat.le_trans (self fixed) (Nat.pow_le_pow_right (n := 2) (by decide) (Nat.le_add_left fixed bits))
    omega
  have linear := add 1 (4 * n) 1 (4 + n) (self 1) (mul 4 n 4 n (self 4) (self n))
  have product := mul (density * n) (1 + 4 * n) (density + n) (1 + (4 + n) + 1)
    (mul density n density n (self density) (self n)) linear
  have space := add 3 (density * n * (1 + 4 * n)) 3
    ((density + n) + (1 + (4 + n) + 1)) (self 3) product
  have total := add (max (2 ^ bits) fixed) (3 + density * n * (1 + 4 * n))
    (bits + fixed) (3 + ((density + n) + (1 + (4 + n) + 1)) + 1) maxBound space
  have bitBound := leaf_bits solver k density n
  have exponent : (bits + fixed) + (3 + ((density + n) + (1 + (4 + n) + 1)) + 1) + 1 ≤
      leafReserveSlope solver k density * (n + 1) := by
    unfold leafReserveSlope
    dsimp only [bits]
    simp only [Nat.add_mul, Nat.mul_add, Nat.mul_one] at bitBound ⊢
    dsimp only [fixed] at *
    omega
  exact Nat.le_trans total (Nat.pow_le_pow_right (n := 2) (by decide) exponent)

end WordRAM.Conjectures.Sparsification.PowerBudget

/-! Exponential envelopes measured in the SAT word-size parameter. These bounds
hold for every input size, including inputs below asymptotic thresholds. -/
namespace WordRAM.Conjectures.Sparsification.MemoryEnvelope

def measure (f : SATInstance) : Nat := f.variables + (inputMagnitude f.encode).log2 + 1

@[irreducible] def Bound (m coefficient value : Nat) : Prop := value ≤ 2 ^ (coefficient * m)

theorem const (m value : Nat) (positive : 1 ≤ m) : Bound m value value := by
  unfold Bound
  exact Nat.le_trans (PowerBudget.self value) (Nat.pow_le_pow_right (n := 2) (by decide)
    (Nat.le_mul_of_pos_right value positive))

theorem add (positive : 1 ≤ m) (hx : Bound m a x) (hy : Bound m b y) : Bound m (a + b + 1) (x + y) := by
  unfold Bound at hx hy ⊢
  have h := PowerBudget.add x y (a * m) (b * m) hx hy
  apply Nat.le_trans h (Nat.pow_le_pow_right (n := 2) (by decide) ?_)
  simp only [Nat.add_mul, Nat.one_mul]
  omega

theorem mul (hx : Bound m a x) (hy : Bound m b y) : Bound m (a + b) (x * y) := by
  unfold Bound at hx hy ⊢
  have h := PowerBudget.mul x y (a * m) (b * m) hx hy
  simpa only [Bound, Nat.add_mul] using h

theorem pow (hx : Bound m a x) (p : Nat) : Bound m (a * p) (x ^ p) := by
  unfold Bound at hx ⊢
  have h := Nat.pow_le_pow_left hx p
  rw [← Nat.pow_mul] at h
  simpa only [Bound, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using h

theorem length (f : SATInstance) : Bound (measure f) 1 f.encode.length := by
  unfold Bound
  have lower := OVMagnitude.fold_ge f.encode f.encode.length
  have len : f.encode.length < inputMagnitude f.encode := by unfold inputMagnitude; omega
  have log : inputMagnitude f.encode < 2 ^ ((inputMagnitude f.encode).log2 + 1) := Nat.lt_log2_self
  exact Nat.le_trans (Nat.le_of_lt (Nat.lt_trans len log))
    (Nat.pow_le_pow_right (n := 2) (by decide) (by simp [measure]))

theorem weight_le_length (f : SATInstance) : Sparsification.weight f.clauses ≤ f.encode.length := by
  have weight : ∀ (clauses : CNF f.variables), Sparsification.weight clauses ≤ MaskTable.span clauses := by
    intro clauses
    induction clauses with
    | nil => simp [Sparsification.weight, MaskTable.span]
    | cons c cs ih => simp only [Sparsification.weight, MaskTable.span]; omega
  have h := weight f.clauses
  rw [InputScan.encoding_length]
  omega

def leafRate (tuning k : Nat) : Nat := Exponent.rate (Exponent.tuningExponent tuning k) k

theorem leaves (tuning k : Nat) (f : SATInstance) :
    Bound (measure f) (leafRate tuning k) (Combinatorial.output tuning k f.clauses).length := by
  unfold Bound
  have bound := Exponent.leaf_exponent (Exponent.tuningExponent tuning k) k f.clauses
  have divide := Nat.div_le_self f.variables (2 ^ Exponent.tuningExponent tuning k)
  have exponent : (f.variables / 2 ^ Exponent.tuningExponent tuning k + 1) * leafRate tuning k ≤
      leafRate tuning k * measure f := by
    have scaled := Nat.mul_le_mul_right (leafRate tuning k) (show f.variables / 2 ^ Exponent.tuningExponent tuning k + 1 ≤ measure f by unfold measure; omega)
    simpa only [Nat.mul_comm] using scaled
  exact Nat.le_trans bound (Nat.pow_le_pow_right (n := 2) (by decide) exponent)

theorem calls (tuning k : Nat) (f : SATInstance) :
    Bound (measure f) (leafRate tuning k + 4)
      (Work.calls (Normalize.normalize f.clauses) (Thresholds.threshold (Exponent.tuning tuning k)) k
        (Thresholds.threshold_large _ (Exponent.tuning_positive tuning k))) := by
  have bound := Work.calls_bound (Normalize.normalize f.clauses) (Thresholds.threshold (Exponent.tuning tuning k)) k
    (Thresholds.threshold_large _ (Exponent.tuning_positive tuning k))
  rw [SerializedGenerate.normalized_leaves] at bound
  have positive : 1 ≤ measure f := by unfold measure; omega
  have h := add positive (mul (const (measure f) 2 positive) (leaves tuning k f)) (const (measure f) 1 positive)
  unfold Bound at h ⊢
  apply Nat.le_trans bound
  have eq : (2 + leafRate tuning k) + 1 + 1 = leafRate tuning k + 4 := by omega
  rw [eq] at h
  exact h

def overhead (f : SATInstance) : Nat :=
  f.encode.length + 15 + 3 * f.clauses.length + f.clauses.length * (3 * (f.clauses.length + 1)) + 3

def payload (tuning k : Nat) (f : SATInstance) : Nat :=
  overhead f + Work.calls (Normalize.normalize f.clauses) (Thresholds.threshold (Exponent.tuning tuning k)) k
    (Thresholds.threshold_large _ (Exponent.tuning_positive tuning k)) * TraversalBounds.stride f.encode.length

theorem overhead_bound (f : SATInstance) : Bound (measure f) 34 (overhead f) := by
  have positive : 1 ≤ measure f := by unfold measure; omega
  have len := length f
  have count : Bound (measure f) 1 f.clauses.length := by
    have span := MaskTable.span_eq f.clauses
    have encode := InputScan.encoding_length f
    unfold Bound at len ⊢
    exact Nat.le_trans (by omega) len
  have one := const (measure f) 1 positive
  have three := const (measure f) 3 positive
  have fifteen := const (measure f) 15 positive
  have first : Bound (measure f) 17 (f.encode.length + 15) := add positive len fifteen
  have second : Bound (measure f) 4 (3 * f.clauses.length) := mul three count
  have subtotal : Bound (measure f) 22 (f.encode.length + 15 + 3 * f.clauses.length) := add positive first second
  have plus : Bound (measure f) 3 (f.clauses.length + 1) := add positive count one
  have step : Bound (measure f) 6 (3 * (f.clauses.length + 1)) := mul three plus
  have square : Bound (measure f) 7 (f.clauses.length * (3 * (f.clauses.length + 1))) := mul count step
  have subtotal' : Bound (measure f) 30
      (f.encode.length + 15 + 3 * f.clauses.length + f.clauses.length * (3 * (f.clauses.length + 1))) :=
    add positive subtotal square
  exact add positive subtotal' three

theorem stride_bound (f : SATInstance) : Bound (measure f) 61 (TraversalBounds.stride f.encode.length) := by
  have positive : 1 ≤ measure f := by unfold measure; omega
  have plus : Bound (measure f) 3 (f.encode.length + 1) := add positive (length f) (const _ 1 positive)
  have square : Bound (measure f) 6 ((f.encode.length + 1) ^ 2) := pow plus 2
  have scaled : Bound (measure f) 54 (48 * (f.encode.length + 1) ^ 2) := mul (const _ 48 positive) square
  exact add positive scaled (const _ 6 positive)

theorem payload_bound (tuning k : Nat) (f : SATInstance) :
    Bound (measure f) (leafRate tuning k + 100) (payload tuning k f) := by
  have positive : 1 ≤ measure f := by unfold measure; omega
  have h := add positive (overhead_bound f) (mul (calls tuning k f) (stride_bound f))
  have eq : 34 + (leafRate tuning k + 4 + 61) + 1 = leafRate tuning k + 100 := by omega
  rw [eq] at h
  exact h

theorem leaf_allocation (solver : Algorithm) (tuning k : Nat) (f : SATInstance) :
    Bound (measure f) (leafRate tuning k + PowerBudget.leafReserveSlope solver k (Combinatorial.density tuning k))
      ((Combinatorial.output tuning k f.clauses).length * LeafBudgets.reserve solver k (Combinatorial.density tuning k) f.variables) := by
  have reserve := PowerBudget.leaf_reserve solver k (Combinatorial.density tuning k) f.variables
  have scaled : PowerBudget.leafReserveSlope solver k (Combinatorial.density tuning k) * (f.variables + 1) ≤
      PowerBudget.leafReserveSlope solver k (Combinatorial.density tuning k) * measure f :=
    Nat.mul_le_mul_left _ (by unfold measure; omega)
  have bounded : Bound (measure f) (PowerBudget.leafReserveSlope solver k (Combinatorial.density tuning k))
      (LeafBudgets.reserve solver k (Combinatorial.density tuning k) f.variables) := by
    unfold Bound
    exact Nat.le_trans reserve (Nat.pow_le_pow_right (n := 2) (by decide) scaled)
  exact mul (leaves tuning k f) bounded

end WordRAM.Conjectures.Sparsification.MemoryEnvelope