SETH ⇒ OVC sparsification bundle 49: 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_48

set_option autoImplicit true

/-! A fixed word-size factor supplies every memory premise of the public solver. -/
namespace WordRAM.Conjectures.Sparsification.WordBounds
open MemoryEnvelope

def threshold (tuning k : Nat) := Thresholds.threshold (Exponent.tuning tuning k)
theorem large (tuning k : Nat) : ∀ i, 2 ≤ threshold tuning k i :=
  Thresholds.threshold_large _ (Exponent.tuning_positive tuning k)

def factor (solver : Algorithm) (tuning k : Nat) : Nat :=
  (leafRate tuning k + 100) +
  (leafRate tuning k + PowerBudget.leafReserveSlope solver k (Combinatorial.density tuning k)) +
  PowerBudget.leafSlope solver k (Combinatorial.density tuning k) +
  Combinatorial.occurrenceBound tuning k + TraversalBody.dataBase k + 10

theorem positive (solver : Algorithm) (tuning k : Nat) : 0 < factor solver tuning k := by unfold factor; omega

def machine (solver : Algorithm) (tuning k : Nat) : Algorithm :=
  PublicSolver.algorithm solver (threshold tuning k) k (factor solver tuning k) (positive solver tuning k)

def allocation (solver : Algorithm) (tuning k : Nat) (f : SATInstance) : Nat :=
  (Combinatorial.output tuning k f.clauses).length * LeafBudgets.reserve solver k (Combinatorial.density tuning k) f.variables

def finalBudget (solver : Algorithm) (tuning k : Nat) (w : Width) (f : SATInstance) : Nat :=
  LeafRegion.base w + allocation solver tuning k f

private theorem fraction (w : Width) (wide : 3 ≤ w.bits) :
    InputBootstrap.base w = 4 * 2 ^ (w.bits - 3) ∧
    LeafRegion.base w = 6 * 2 ^ (w.bits - 3) ∧
    2 ^ w.bits = 8 * 2 ^ (w.bits - 3) := by
  have half : w.bits - 1 = 2 + (w.bits - 3) := by omega
  have quarter : w.bits - 2 = 1 + (w.bits - 3) := by omega
  have full : w.bits = 3 + (w.bits - 3) := by omega
  constructor
  · simp [InputBootstrap.base, half, Nat.pow_add]
  constructor
  · simp only [LeafRegion.base, quarter, Nat.pow_add]
    rw [← Nat.mul_assoc]
  · conv => lhs; rw [full]
    rw [Nat.pow_add]

structure Parameters (solver : Algorithm) (tuning k : Nat) (w : Width) (f : SATInstance) : Prop where
  wide : 6 ≤ w.bits
  variables : f.variables ≤ w.bits
  inputBelow : f.encode.length < InputBootstrap.base w
  regionRoom : InputBootstrap.base w + max 15 f.encode.length ≤ LeafRegion.base w
  controls : TraversalBody.dataBase k ≤ InputBootstrap.base w + 2
  fits : LeafRegion.base w < 2 ^ w.bits
  finalFits : finalBudget solver tuning k w f < 2 ^ w.bits
  thresholds : ∀ i, i ≤ k → threshold tuning k i < 2 ^ w.bits
  space : NormalizeSetup.endpoint (PublicSetup.workspace (InputBootstrap.base w) f.encode.length f.clauses.length)
      f.clauses.length + 3 + Work.calls (Normalize.normalize f.clauses) (threshold tuning k) k (large tuning k) *
      TraversalBounds.stride f.encode.length ≤ LeafRegion.base w
  solverWidth : LeafBudgets.bits solver k (Combinatorial.density tuning k) f.variables ≤ w.bits

 theorem parameters (solver : Algorithm) (tuning k : Nat) (f : SATInstance) :
    Parameters solver tuning k ((machine solver tuning k).width f.encode f.variables) f := by
  let w := (machine solver tuning k).width f.encode f.variables
  change Parameters solver tuning k w f
  have width : w.bits = factor solver tuning k * MemoryEnvelope.measure f := rfl
  have pos : 1 ≤ MemoryEnvelope.measure f := by unfold MemoryEnvelope.measure; omega
  have atLeast : factor solver tuning k ≤ w.bits := by
    rw [width]; exact Nat.le_mul_of_pos_right _ pos
  have wide : 6 ≤ w.bits := by unfold factor at atLeast; omega
  have fitsEnvelope (coefficient value : Nat) (bound : Bound (MemoryEnvelope.measure f) coefficient value)
      (room : coefficient + 3 ≤ factor solver tuning k) : value ≤ 2 ^ (w.bits - 3) := by
    have scaled := Nat.mul_le_mul_right (MemoryEnvelope.measure f) room
    have exponent : coefficient * MemoryEnvelope.measure f ≤ w.bits - 3 := by
      rw [width]; simp only [Nat.add_mul] at scaled; omega
    unfold Bound at bound
    exact Nat.le_trans bound (Nat.pow_le_pow_right (n := 2) (by decide) exponent)
  have generator := fitsEnvelope _ _ (payload_bound tuning k f) (by unfold factor; omega)
  have leaves := fitsEnvelope _ _ (leaf_allocation solver tuning k f) (by unfold factor; omega)
  have control := fitsEnvelope _ _ (const (MemoryEnvelope.measure f) (TraversalBody.dataBase k) pos) (by unfold factor; omega)
  have thresholdBound := fitsEnvelope _ _ (const (MemoryEnvelope.measure f) (Combinatorial.occurrenceBound tuning k) pos) (by unfold factor; omega)
  obtain ⟨half, region, full⟩ := fraction w (by omega)
  have powerPositive := Nat.two_pow_pos (w.bits - 3)
  have overheadLower : f.encode.length + 15 ≤ payload tuning k f := by unfold payload overhead; omega
  have variables : f.variables ≤ w.bits := by
    have m : MemoryEnvelope.measure f ≤ factor solver tuning k * MemoryEnvelope.measure f := Nat.le_mul_of_pos_left _ (positive solver tuning k)
    unfold MemoryEnvelope.measure at m; rw [width]; unfold MemoryEnvelope.measure; omega
  refine ⟨wide, variables, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · omega
  · omega
  · omega
  · omega
  · change LeafRegion.base w + allocation solver tuning k f < 2 ^ w.bits
    change allocation solver tuning k f ≤ _ at leaves
    omega
  · intro i hi
    have bound := Combinatorial.threshold_bound tuning k i hi
    change threshold tuning k i ≤ _ at bound
    omega
  · have eq : NormalizeSetup.endpoint (PublicSetup.workspace (InputBootstrap.base w) f.encode.length f.clauses.length)
        f.clauses.length + 3 + Work.calls (Normalize.normalize f.clauses) (threshold tuning k) k (large tuning k) *
        TraversalBounds.stride f.encode.length = InputBootstrap.base w + payload tuning k f := by
      simp only [NormalizeSetup.endpoint, PublicSetup.workspace, PublicSetup.records, payload, MemoryEnvelope.overhead, Nat.add_assoc]
      rfl
    rw [eq]
    omega
  · have bits := PowerBudget.leaf_bits solver k (Combinatorial.density tuning k) f.variables
    have first := Nat.mul_le_mul_left (PowerBudget.leafSlope solver k (Combinatorial.density tuning k))
      (show f.variables + 1 ≤ MemoryEnvelope.measure f by unfold MemoryEnvelope.measure; omega)
    have second := Nat.mul_le_mul_right (MemoryEnvelope.measure f)
      (show PowerBudget.leafSlope solver k (Combinatorial.density tuning k) ≤ factor solver tuning k by unfold factor; omega)
    rw [width]
    omega

end WordRAM.Conjectures.Sparsification.WordBounds

/-! Fast sparse SAT supplies a uniform, total SAT machine. Only the final
asymptotic aggregation is separate from this actual execution theorem. -/
namespace WordRAM.Conjectures.Sparsification.Machine

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 ∧
      ∀ f : SATInstance, f.IsKCNF k → ∃ leafTime time,
        DecidesIn (WordBounds.machine solver tuning k) f.encode f.variables time f.Satisfiable ∧
        time ≤ PublicSolver.costBound ((WordBounds.machine solver tuning k).width f.encode f.variables) f
          (WordBounds.threshold tuning k) k f.encode.length
          (LeafBudgets.cost k (Combinatorial.density tuning k) f.variables leafTime) (WordBounds.large tuning k) ∧
        (n₀ ≤ f.variables → leafTime ^ q ≤ C * 2 ^ ((q - 1) * f.variables) *
          (EncodingBounds.lengthBound k (Combinatorial.density tuning k) f.variables + 1) ^ p) := by
  obtain ⟨solver, C, p, n₀, positiveC, eligible⟩ := LeafBudgets.from_fast tuning k q positive fast
  refine ⟨solver, C, p, n₀, positiveC, ?_⟩
  intro f width
  obtain ⟨leafTime, eligible, leafBound⟩ := eligible f.variables f.clauses width
  let w := (WordBounds.machine solver tuning k).width f.encode f.variables
  have parameters := WordBounds.parameters solver tuning k f
  obtain ⟨time, final, bound, trace, halted, boolean, correct⟩ :=
    PublicSolver.executes solver (WordBounds.threshold tuning k) k (WordBounds.factor solver tuning k)
      f.encode.length (LeafBudgets.cost k (Combinatorial.density tuning k) f.variables leafTime)
      (LeafBudgets.reserve solver k (Combinatorial.density tuning k) f.variables) (LeafRegion.base w)
      (WordBounds.finalBudget solver tuning k w f) (WordBounds.positive solver tuning k)
      (WordBounds.large tuning k) w f parameters.wide parameters.variables parameters.inputBelow
      parameters.regionRoom parameters.controls parameters.fits (Nat.le_refl _) parameters.finalFits
      parameters.thresholds width (MemoryEnvelope.weight_le_length f) parameters.space
      (eligible w parameters.solverWidth) (Nat.le_refl _)
  exact ⟨leafTime, time, ⟨final, trace, halted, boolean, correct⟩, bound, leafBound⟩

end WordRAM.Conjectures.Sparsification.Machine

namespace WordRAM.Conjectures.Sparsification.Polynomial

def base (n length : Nat) : Nat := (n + 1) * (length + 1)
@[irreducible] def Bounded (f : Nat → Nat → Nat) : Prop :=
  ∃ C degree, 0 < C ∧ ∀ n length, f n length ≤ C * base n length ^ degree

theorem constant (value : Nat) : Bounded (fun _ _ => value) := by
  unfold Bounded
  exact ⟨value + 1, 0, by omega, by intros; simp⟩

theorem variables : Bounded (fun n _ => n) := by
  unfold Bounded
  refine ⟨1, 1, by decide, ?_⟩
  intro n length
  have h := Nat.le_mul_of_pos_right (n + 1) (by omega : 0 < length + 1)
  simpa only [Nat.one_mul, Nat.pow_one] using (show n ≤ base n length by unfold base; omega)

theorem length : Bounded (fun _ length => length) := by
  unfold Bounded
  refine ⟨1, 1, by decide, ?_⟩
  intro n length
  have h := Nat.le_mul_of_pos_left (length + 1) (by omega : 0 < n + 1)
  simpa only [Nat.one_mul, Nat.pow_one] using (show length ≤ base n length by unfold base; omega)

theorem add (hf : Bounded f) (hg : Bounded g) : Bounded (fun n length => f n length + g n length) := by
  unfold Bounded at hf hg ⊢
  obtain ⟨C, d, cp, fb⟩ := hf
  obtain ⟨D, e, dp, gb⟩ := hg
  refine ⟨C + D, d + e, by omega, ?_⟩
  intro n length
  have pos : 0 < base n length := Nat.mul_pos (by omega) (by omega)
  have first := Nat.le_trans (fb n length) (Nat.mul_le_mul_left C
    (Nat.pow_le_pow_right pos (Nat.le_add_right d e)))
  have second := Nat.le_trans (gb n length) (Nat.mul_le_mul_left D
    (Nat.pow_le_pow_right pos (Nat.le_add_left e d)))
  simpa only [Nat.add_mul] using Nat.add_le_add first second

theorem mul (hf : Bounded f) (hg : Bounded g) : Bounded (fun n length => f n length * g n length) := by
  unfold Bounded at hf hg ⊢
  obtain ⟨C, d, cp, fb⟩ := hf
  obtain ⟨D, e, dp, gb⟩ := hg
  refine ⟨C * D, d + e, Nat.mul_pos cp dp, ?_⟩
  intro n length
  simpa only [Nat.pow_add, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using
    Nat.mul_le_mul (fb n length) (gb n length)

theorem pow (hf : Bounded f) (p : Nat) : Bounded (fun n length => f n length ^ p) := by
  unfold Bounded at hf ⊢
  obtain ⟨C, d, cp, fb⟩ := hf
  refine ⟨C ^ p, d * p, Nat.pow_pos cp, ?_⟩
  intro n length
  simpa only [Nat.mul_pow, ← Nat.pow_mul] using Nat.pow_le_pow_left (fb n length) p

end WordRAM.Conjectures.Sparsification.Polynomial

namespace WordRAM.Conjectures.Sparsification.RuntimePolynomial

def wordCost (factor k n length : Nat) : Nat := factor * (2 * n + k + 2 * length + 3)
def baseCost (k bits length : Nat) : Nat :=
  17 * length + 56 + (length * (10 * k + 12 * bits + 35) + 2) +
    length * (35 * length + 34) + 12 * length + 66 + 9

def leafOverhead (k density n : Nat) : Nat :=
  density * n * (22 * n + 29) + 7 * EncodingBounds.lengthBound k density n +
    4 * EncodingBounds.magnitudeBound k density n + 52

def coefficient (factor k density n length : Nat) : Nat :=
  baseCost k (wordCost factor k n length) length +
    2 * (TraversalBounds.bodyCost n k (wordCost factor k n length) length + 2) +
    leafOverhead k density n + 19

theorem polynomial (factor k density : Nat) : Polynomial.Bounded (coefficient factor k density) := by
  unfold coefficient baseCost wordCost TraversalBounds.bodyCost SelectBranch.cost FlowerSearch.coreBound
    leafOverhead EncodingBounds.lengthBound EncodingBounds.magnitudeBound
  repeat first
    | exact Polynomial.variables
    | exact Polynomial.length
    | apply Polynomial.add
    | apply Polynomial.mul
    | apply Polynomial.pow
    | apply Polynomial.constant

theorem word_bound (solver : Algorithm) (tuning k : Nat) (f : SATInstance) (width : f.IsKCNF k) :
    ((WordBounds.machine solver tuning k).width f.encode f.variables).bits ≤
      wordCost (WordBounds.factor solver tuning k) k f.variables f.encode.length := by
  have mag := EncodingBounds.magnitude_general f width
  have log := Nat.log2_le_self (inputMagnitude f.encode)
  exact Nat.mul_le_mul_left _ (by omega)

theorem records_bound (w : Width) (formula : CNF n) (width : ∀ clause ∈ formula, clause.length ≤ k) :
    RecordTable.cost w formula ≤ formula.length * (10 * k + 12 * w.bits + 35) + 2 := by
  induction formula with
  | nil => simp [RecordTable.cost]
  | cons clause rest ih =>
    have head := Nat.mul_le_mul_left 10 (width clause (by simp))
    have tail := ih (fun c hc => width c (by simp [hc]))
    simp only [RecordTable.cost, List.length_cons, Nat.add_mul, Nat.one_mul]
    omega

theorem body_mono (n k length a b : Nat) (le : a ≤ b) :
    TraversalBounds.bodyCost n k a length ≤ TraversalBounds.bodyCost n k b length := by
  have word := Nat.mul_le_mul_left 12 le
  have core := Nat.mul_le_mul_right ((2 * n + 1) ^ k)
    (show 10 * k + 12 * a + 18 * length + 61 ≤ 10 * k + 12 * b + 18 * length + 61 by omega)
  have search := Nat.mul_le_mul_left ((k + 1) * (k + 1)) (Nat.add_le_add_right core 5)
  have branch := Nat.mul_le_mul_right ((length + 1) ^ 2) (show 12 * a + 396 ≤ 12 * b + 396 by omega)
  unfold TraversalBounds.bodyCost SelectBranch.cost FlowerSearch.coreBound
  omega

theorem combine (base body overhead leaves time scale : Nat) :
    base + (2 * leaves + 1) * body + leaves * (overhead + scale * time) ≤
      (base + 2 * body + overhead + scale) * (leaves + 1) * (time + 1) := by
  have first1 : base ≤ base * (leaves + 1) := Nat.le_mul_of_pos_right base (by omega)
  have first2 : base * (leaves + 1) ≤ base * (leaves + 1) * (time + 1) := Nat.le_mul_of_pos_right _ (by omega)
  have first := Nat.le_trans first1 first2
  have second : (2 * leaves + 1) * body ≤ (2 * body) * (leaves + 1) * (time + 1) := by
    have h := Nat.mul_le_mul_right body (show 2 * leaves + 1 ≤ 2 * (leaves + 1) by omega)
    have grow := Nat.le_mul_of_pos_right ((2 * body) * (leaves + 1)) (show 0 < time + 1 by omega)
    apply Nat.le_trans _ grow
    simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using h
  have third : leaves * (overhead + scale * time) ≤ (overhead + scale) * (leaves + 1) * (time + 1) := by
    have call : overhead + scale * time ≤ (overhead + scale) * (time + 1) := by
      simp only [Nat.add_mul, Nat.mul_add, Nat.mul_one]
      omega
    have h := Nat.mul_le_mul (Nat.le_succ leaves) call
    simpa only [Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using h
  have h := Nat.add_le_add (Nat.add_le_add first second) third
  have rearrange : base * (leaves + 1) * (time + 1) + (2 * body) * (leaves + 1) * (time + 1) +
      (overhead + scale) * (leaves + 1) * (time + 1) =
      (base + 2 * body + overhead + scale) * (leaves + 1) * (time + 1) := by
    rw [← Nat.add_mul, ← Nat.add_mul, ← Nat.add_mul, ← Nat.add_mul]
    simp only [Nat.add_assoc]
  exact Nat.le_trans h (Nat.le_of_eq rearrange)

theorem bounds (solver : Algorithm) (tuning k : Nat) (f : SATInstance) (width : f.IsKCNF k) (time : Nat) :
    PublicSolver.costBound ((WordBounds.machine solver tuning k).width f.encode f.variables) f
      (WordBounds.threshold tuning k) k f.encode.length
      (LeafBudgets.cost k (Combinatorial.density tuning k) f.variables time) (WordBounds.large tuning k) ≤
    coefficient (WordBounds.factor solver tuning k) k (Combinatorial.density tuning k) f.variables f.encode.length *
      ((Combinatorial.output tuning k f.clauses).length + 1) * (time + 1) := by
  let w := (WordBounds.machine solver tuning k).width f.encode f.variables
  let bits := wordCost (WordBounds.factor solver tuning k) k f.variables f.encode.length
  let leaves := (Combinatorial.output tuning k f.clauses).length
  have word := word_bound solver tuning k f width
  change w.bits ≤ bits at word
  have count : f.clauses.length ≤ f.encode.length := by
    have span := MaskTable.span_eq f.clauses
    have len := InputScan.encoding_length f
    omega
  have records := records_bound w f.clauses width
  have table := Nat.mul_le_mul count (show 10 * k + 12 * w.bits + 35 ≤ 10 * k + 12 * bits + 35 by omega)
  have normalize := Nat.mul_le_mul count (show 35 * f.clauses.length + 34 ≤ 35 * f.encode.length + 34 by omega)
  have calls := Work.calls_bound (Normalize.normalize f.clauses) (WordBounds.threshold tuning k) k (WordBounds.large tuning k)
  rw [SerializedGenerate.normalized_leaves] at calls
  have body := body_mono f.variables k f.encode.length w.bits bits word
  have generated := Nat.mul_le_mul calls (Nat.add_le_add_right body 2)
  have combined := combine (baseCost k bits f.encode.length)
    (TraversalBounds.bodyCost f.variables k bits f.encode.length + 2)
    (leafOverhead k (Combinatorial.density tuning k) f.variables) leaves time 19
  apply Nat.le_trans _ combined
  change PublicSolver.costBound w f _ _ _ _ _ ≤ _
  unfold PublicSolver.costBound baseCost
  change Work.calls (Normalize.normalize f.clauses) (WordBounds.threshold tuning k) k (WordBounds.large tuning k) *
      (TraversalBounds.bodyCost f.variables k w.bits f.encode.length + 2) ≤
      (2 * leaves + 1) * (TraversalBounds.bodyCost f.variables k bits f.encode.length + 2) at generated
  have leafEq : LeafBudgets.cost k (Combinatorial.density tuning k) f.variables time + 2 =
      leafOverhead k (Combinatorial.density tuning k) f.variables + 19 * time := by
    unfold LeafBudgets.cost leafOverhead; omega
  have leafCount : (Tree.leaves f.clauses (WordBounds.threshold tuning k) k (WordBounds.large tuning k)).length = leaves := rfl
  rw [leafEq, leafCount]
  omega

end WordRAM.Conjectures.Sparsification.RuntimePolynomial

/-! Polynomial factors in the variable count are eventually absorbed by an
arbitrarily small exponential budget; no real-number asymptotics are assumed. -/
namespace WordRAM.Conjectures.Sparsification.PolynomialAbsorption

theorem power_le (degree n : Nat) (large : 2 ^ (degree + 4) ≤ n) :
    (n + 1) ^ degree ≤ 2 ^ n := by
  let logarithm := (n + 1).log2
  have logLarge : degree + 4 ≤ logarithm :=
    (Nat.le_log2 (by omega : n + 1 ≠ 0)).mpr (by omega)
  have square := Exponent.square_le_power logarithm (by omega)
  have linear : (logarithm + 1) * degree < logarithm * logarithm := by
    have scaled := Nat.mul_le_mul_left logarithm (show degree + 1 ≤ logarithm by omega)
    simp only [Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul] at scaled ⊢
    omega
  have below : 2 ^ logarithm ≤ n + 1 := (Nat.le_log2 (by omega : n + 1 ≠ 0)).mp (Nat.le_refl _)
  have exponent : (logarithm + 1) * degree ≤ n := by omega
  have upper : n + 1 ≤ 2 ^ (logarithm + 1) := Nat.le_of_lt Nat.lt_log2_self
  have raised := Nat.pow_le_pow_left upper degree
  rw [← Nat.pow_mul] at raised
  exact Nat.le_trans raised (Nat.pow_le_pow_right (n := 2) (by decide) exponent)

/-- Combining a polynomial and a leaf bound spends at most one full factor 2^n.
The squared hypotheses reserve half that exponent for each factor. -/
theorem times_le (degree q n leaves : Nat) (_positive : 0 < q)
    (large : 2 ^ (degree * (4 * q) + 4) ≤ n)
    (leafBound : leaves ^ (4 * q) ≤ 2 ^ n) :
    ((n + 1) ^ degree * leaves) ^ (2 * q) ≤ 2 ^ n := by
  apply (Nat.pow_le_pow_iff_left (n := 2) (by decide)).mp
  have polynomial := power_le (degree * (4 * q)) n large
  have product := Nat.mul_le_mul polynomial leafBound
  have exponent : 2 * q * 2 = 4 * q := by omega
  rw [← Nat.pow_mul, exponent, Nat.mul_pow, ← Nat.pow_mul]
  simpa only [Nat.pow_succ, Nat.pow_zero, Nat.one_mul, Nat.mul_one] using product

end WordRAM.Conjectures.Sparsification.PolynomialAbsorption