SETH ⇒ OVC sparsification bundle 50: 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_49

set_option autoImplicit true

/-! The final rational-exponent accounting for construction, all leaves, and
sparse solver calls. Polynomial dependence on unused variables is absorbed here. -/
namespace WordRAM.Conjectures.Sparsification.Aggregate

def callConstant (q C A p : Nat) : Nat := 2 ^ q * (C * A ^ p + 1)
def constant (q K C A p : Nat) : Nat := (2 * K) ^ (2 * q) * callConstant q C A p ^ 2

theorem positive (q K C A p : Nat) (hk : 0 < K) : 0 < constant q K C A p := by
  unfold constant callConstant
  exact Nat.mul_pos (Nat.pow_pos (Nat.mul_pos (by decide) hk))
    (Nat.pow_pos (Nat.mul_pos (Nat.two_pow_pos _) (by omega)))

theorem call_bound (q C A p n time : Nat)
    (solver : time ^ q ≤ C * 2 ^ ((q - 1) * n) * (A * (n + 1)) ^ p) :
    (time + 1) ^ q ≤ callConstant q C A p * 2 ^ ((q - 1) * n) * (n + 1) ^ p := by
  let rate := 2 ^ ((q - 1) * n) * (n + 1) ^ p
  have ratePositive : 0 < rate := Nat.mul_pos (Nat.two_pow_pos _) (Nat.pow_pos (by omega))
  have solver' : time ^ q ≤ (C * A ^ p) * rate := by
    simpa only [rate, Nat.mul_pow, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using solver
  have sum : time ^ q + 1 ≤ (C * A ^ p + 1) * rate := by rw [Nat.add_mul, Nat.one_mul]; omega
  have raised := ReductionRuntime.add_power_bound time 1 q
  have result := Nat.le_trans raised (Nat.mul_le_mul_left (2 ^ q) (by simpa using sum))
  simpa only [callConstant, rate, Nat.mul_assoc] using result

theorem total_bound (q K C A p degree n length leaves call time : Nat) (qLarge : 2 ≤ q)
    (runtime : time ≤ K * ((n + 1) * (length + 1)) ^ degree * (leaves + 1) * (call + 1))
    (solver : call ^ q ≤ C * 2 ^ ((q - 1) * n) * (A * (n + 1)) ^ p)
    (leafBound : leaves ^ (4 * q) ≤ 2 ^ n)
    (large : 2 ^ ((degree + p) * (4 * q) + 4) ≤ n) :
    time ^ (2 * q) ≤ constant q K C A p * 2 ^ ((2 * q - 1) * n) * (length + 1) ^ (degree * (2 * q)) := by
  let count := max 1 leaves
  have maxBound : count ^ (4 * q) ≤ 2 ^ n := by
    by_cases small : leaves ≤ 1
    · simp only [count, Nat.max_eq_left small, Nat.one_pow]
      exact Nat.two_pow_pos _
    · simpa only [count, Nat.max_eq_right (by omega : 1 ≤ leaves)] using leafBound
  have countBound : leaves + 1 ≤ 2 * count := by dsimp [count]; omega
  have runtime' : time ≤ (2 * K) * ((n + 1) * (length + 1)) ^ degree * count * (call + 1) := by
    have h := Nat.mul_le_mul_right (call + 1)
      (Nat.mul_le_mul_left (K * ((n + 1) * (length + 1)) ^ degree) countBound)
    apply Nat.le_trans runtime
    simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using h
  have callBound := Nat.pow_le_pow_left (call_bound q C A p n call solver) 2
  have callExponent : q * 2 = 2 * q := by omega
  have callFull : (call + 1) ^ (2 * q) ≤ callConstant q C A p ^ 2 *
      2 ^ (((q - 1) * n) * 2) * (n + 1) ^ (p * 2) := by
    simpa only [Nat.mul_pow, ← Nat.pow_mul, callExponent] using callBound
  have polynomial := PolynomialAbsorption.times_le (degree + p) q n count (by omega) large maxBound
  have degreeBound : degree * (2 * q) + p * 2 ≤ (degree + p) * (2 * q) := by
    have h := Nat.mul_le_mul_left p (show 2 ≤ 2 * q by omega)
    rw [Nat.add_mul]
    omega
  have extra : (n + 1) ^ (degree * (2 * q)) * (n + 1) ^ (p * 2) * count ^ (2 * q) ≤ 2 ^ n := by
    have h := Nat.mul_le_mul_right (count ^ (2 * q))
      (Nat.pow_le_pow_right (by omega : 0 < n + 1) degreeBound)
    rw [Nat.pow_add] at h
    apply Nat.le_trans h
    simpa only [Nat.mul_pow, ← Nat.pow_mul] using polynomial
  have raised := Nat.pow_le_pow_left runtime' (2 * q)
  simp only [Nat.mul_pow, ← Nat.pow_mul] at raised
  have simulated := Nat.mul_le_mul_left
    ((2 * K) ^ (2 * q) * ((n + 1) ^ (degree * (2 * q)) * (length + 1) ^ (degree * (2 * q))) * count ^ (2 * q)) callFull
  rw [Nat.mul_pow] at simulated
  have bounded := Nat.le_trans raised simulated
  let outside := (2 * K) ^ (2 * q) * callConstant q C A p ^ 2 *
    2 ^ (((q - 1) * n) * 2) * (length + 1) ^ (degree * (2 * q))
  have collected : time ^ (2 * q) ≤ outside *
      ((n + 1) ^ (degree * (2 * q)) * (n + 1) ^ (p * 2) * count ^ (2 * q)) := by
    simpa only [outside, Nat.mul_pow, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using bounded
  have result := Nat.le_trans collected (Nat.mul_le_mul_left outside extra)
  have exponent : ((q - 1) * n) * 2 + n = (2 * q - 1) * n := by
    have coefficient : (q - 1) * 2 + 1 = 2 * q - 1 := by omega
    calc
      ((q - 1) * n) * 2 + n = ((q - 1) * 2 + 1) * n := by simp [Nat.mul_add, Nat.mul_assoc, Nat.mul_comm]
      _ = _ := by rw [coefficient]
  have eq : outside * 2 ^ n = constant q K C A p * 2 ^ ((2 * q - 1) * n) *
      (length + 1) ^ (degree * (2 * q)) := by
    rw [← exponent, Nat.pow_add]
    simp only [outside, constant, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm]
  rw [eq] at result
  exact result

end WordRAM.Conjectures.Sparsification.Aggregate