SETH ⇒ OVC sparsification bundle 47: 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_46

set_option autoImplicit true

/-! A fixed program starts leaf simulation in the upper quarter of word memory.
The generator must fit below this boundary; leaf allocation fits above it. -/
namespace WordRAM.Conjectures.Sparsification.LeafRegion
open TraversalBody

def base (w : Width) : Nat := 3 * 2 ^ (w.bits - 2)

private def reg (a : Nat) : SourceOperand := .memory (.direct a)

def algorithm (k : Nat) : Algorithm :=
  ⟨[.wordWidth (.direct (freeCell k)),
    .binary .sub (.direct (freeCell k)) (reg (freeCell k)) (.immediate 2),
    .binary .shl (.direct (freeCell k)) (.immediate 1) (reg (freeCell k)),
    .binary (.mul rfl) (.direct (freeCell k)) (.immediate 3) (reg (freeCell k)), .halt], 1, by decide⟩

private theorem pointer (w : Width) (large : 3 ≤ w.bits) :
    (3#w.bits) * ((1#w.bits) <<< (BitVec.ofNat w.bits w.bits - 2#w.bits).toNat) =
      BitVec.ofNat w.bits (base w) := by
  have small : 2 < 2 ^ w.bits := by
    have := Nat.pow_le_pow_right (n := 2) (by decide) large
    omega
  have widthFit : w.bits < 2 ^ w.bits := Nat.lt_pow_self (by decide)
  rw [BitVec.ofNat_sub_ofNat_of_le _ _ small (by omega)]
  have predFit : w.bits - 2 < 2 ^ w.bits := by omega
  simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt predFit]
  have shift : (1#w.bits) <<< (w.bits - 2) = BitVec.ofNat w.bits (2 ^ (w.bits - 2)) := by
    change BitVec.twoPow w.bits (w.bits - 2) = _
    apply BitVec.eq_of_toNat_eq
    exact BitVec.toNat_twoPow _ _
  rw [shift, ← BitVec.ofNat_mul]
  rfl

theorem prepares (k : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) (large : 3 ≤ w.bits) :
    let t := run widthConstant ((algorithm k).program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧
      t.mem (freeCell k) = BitVec.ofNat w.bits (base w) ∧
      (∀ a, a ≠ freeCell k → t.mem a = s.mem a) := by
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, widthConstant,
    pc, live, Nat.add_assoc, pointer w large, -BitVec.toNat_sub, -BitVec.toNat_ofNat]
  intro a h; simp [h]

def calls (solver : Algorithm) (k : Nat) : Algorithm :=
  ⟨SourceChain.code (algorithm k).code (LeafLoop.algorithm solver k).code, 1, by decide⟩

theorem decides (solver : Algorithm) (k cost reserve budget : Nat)
    (tasks : List (StackInvariant.Task n)) (head limit : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (large : 3 ≤ w.bits)
    (pending : StackInvariant.Stored s.mem (dataBase k) limit head tasks)
    (eligible : ∀ task ∈ tasks, LeafLoop.Eligible solver w cost reserve task.formula)
    (variables : s.mem (variableCell k) = BitVec.ofNat w.bits n)
    (output : s.mem (outputCell k) = BitVec.ofNat w.bits head)
    (answer : s.mem (todoCell k) = 0#w.bits)
    (controls : dataBase k ≤ base w) (before : limit ≤ base w)
    (fresh : ∀ a, base w ≤ a → s.mem a = 0#w.bits)
    (space : base w + tasks.length * reserve ≤ budget) :
    ∃ time final, time ≤ tasks.length * (cost + 2) + 9 ∧
      Runs widthConstant ((calls solver k).program w) time s final ∧ final.halted = true ∧
      (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ LeafLoop.AnySAT tasks) := by
  have coords : variableCell k < dataBase k ∧ todoCell k < dataBase k ∧ outputCell k < dataBase k ∧
      freeCell k < dataBase k ∧ variableCell k ≠ freeCell k ∧ todoCell k ≠ freeCell k ∧
      outputCell k ≠ freeCell k := by dsimp [variableCell, todoCell, outputCell, freeCell, dataBase]; omega
  let prepared := run widthConstant ((algorithm k).program w) 5 s
  obtain ⟨ph, pt, pf, frame⟩ := prepares k s pc live large
  have stored : StackInvariant.Stored prepared.mem (dataBase k) (base w) head tasks := by
    apply StackInvariant.weaken tasks prepared.mem (dataBase k) limit (base w) head _ before
    apply StackInvariant.frame tasks s.mem prepared.mem (dataBase k) limit head pending
    intro a ha _; exact frame a (by omega)
  obtain ⟨time, out, bound, trace, halted, boolean, correct, _⟩ :=
    LeafLoop.decides solver k cost reserve budget tasks head (base w) (SourceChain.resume prepared)
      rfl rfl fits variablesFit (by omega) stored eligible
      ((frame _ coords.2.2.2.2.1).trans variables)
      ((frame _ coords.2.2.2.2.2.2).trans output) pf
      ((frame _ coords.2.2.2.2.2.1).trans answer)
      (fun a ha => (frame a (by omega)).trans (fresh a ha)) space
  obtain ⟨ticks, _, setupTrace⟩ := run_has_trace widthConstant ((algorithm k).program w) 5 s
  have ticksCost := runs_cost setupTrace
  have eq : ticks = 5 := by omega
  subst ticks
  have full := SourceChain.traces (algorithm k).code (LeafLoop.algorithm solver k).code
    s prepared out 5 time live ph setupTrace trace
  exact ⟨5 + time, out.relocate (algorithm k).code.length, by omega, full, halted, boolean, correct⟩

end WordRAM.Conjectures.Sparsification.LeafRegion

/-! One fixed program generates sparse leaves and executes the supplied solver
on all of them. Resource eligibility remains explicit for the asymptotic proof. -/
namespace WordRAM.Conjectures.Sparsification.SerializedSolver
open TraversalBody TraversalBounds

def algorithm (solver : Algorithm) (threshold : Nat → Nat) (k : Nat) : Algorithm :=
  ⟨SourceChain.code (SerializedGenerate.algorithm threshold k).code (LeafRegion.calls solver k).code, 1, by decide⟩

theorem decides (solver : Algorithm) (cost reserve finalBudget : Nat) (clauses : CNF n) (threshold : Nat → Nat) (k capacity budget : Nat)
    (large : ∀ i, 2 ≤ threshold i) (s : State w) (source records workspace : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : dataBase k ≤ source)
    (inputBefore : source + MaskTable.span clauses ≤ records)
    (recordsBefore : records + 3 * clauses.length ≤ workspace)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits)
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (recordPointer : s.mem 13 = BitVec.ofNat w.bits records)
    (workspacePointer : s.mem 27 = BitVec.ofNat w.bits workspace)
    (input : MaskTable.Encoded s.mem source clauses)
    (clauseWidth : ∀ clause ∈ clauses, clause.length ≤ k)
    (weight : Sparsification.weight clauses ≤ capacity)
    (space : NormalizeSetup.endpoint workspace clauses.length + 3 +
      Work.calls (Normalize.normalize clauses) threshold k large * stride capacity ≤ budget)
    (region : budget ≤ LeafRegion.base w)
    (finalFits : finalBudget < 2 ^ w.bits)
    (fresh : ∀ a, LeafRegion.base w ≤ a → s.mem a = 0#w.bits)
    (eligible : ∀ formula ∈ Tree.leaves clauses threshold k large, LeafLoop.Eligible solver w cost reserve formula)
    (leafSpace : LeafRegion.base w + (Tree.leaves clauses threshold k large).length * reserve ≤ finalBudget) :
    ∃ time final, time ≤ RecordTable.cost w clauses + clauses.length * (35 * clauses.length + 34) +
        Work.calls (Normalize.normalize clauses) threshold k large * (bodyCost n k w.bits capacity + 2) +
        12 * clauses.length + 66 + (Tree.leaves clauses threshold k large).length * (cost + 2) + 9 ∧
      Runs widthConstant ((algorithm solver threshold k).program w) time s final ∧ final.halted = true ∧
      (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ (SATInstance.mk n clauses).Satisfiable) := by
  obtain ⟨genTime, generated, genBound, genTrace, genHalt, emitted, head, limit,
    stored, order, todo, output, free, limitBound, variableValue, frame⟩ :=
    SerializedGenerateFresh.generates clauses threshold k capacity budget large s source records workspace
      pc live base inputBefore recordsBefore fits variablesFit width thresholdFits variables count pointer
      recordPointer workspacePointer input clauseWidth weight space
  have member (task : StackInvariant.Task n) (h : task ∈ emitted) :
      task.formula ∈ Tree.leaves clauses threshold k large := by
    rw [← order, List.mem_reverse]
    exact List.mem_map.mpr ⟨task, h, rfl⟩
  have length : emitted.length = (Tree.leaves clauses threshold k large).length := by
    rw [← order, List.length_reverse, List.length_map]
  have controls : dataBase k ≤ LeafRegion.base w := by
    have lower : workspace ≤ NormalizeSetup.endpoint workspace clauses.length := by
      unfold NormalizeSetup.endpoint; omega
    omega
  obtain ⟨callTime, final, callBound, callTrace, callHalt, boolean, correct⟩ :=
    LeafRegion.decides solver k cost reserve finalBudget emitted head limit (SourceChain.resume generated)
      rfl rfl finalFits variablesFit width stored (fun task h => eligible task.formula (member task h))
      variableValue output todo controls (by omega)
      (fun a ha => (frame a (by omega)).trans (fresh a ha)) (by simpa only [length] using leafSpace)
  have meaning : LeafLoop.AnySAT emitted ↔ (SATInstance.mk n clauses).Satisfiable := by
    rw [Tree.leaves_satisfiable clauses threshold k large]
    constructor
    · rintro ⟨task, h, sat⟩
      exact ⟨task.formula, member task h, sat⟩
    · rintro ⟨formula, h, sat⟩
      rw [← order, List.mem_reverse] at h
      obtain ⟨task, h, eq⟩ := List.mem_map.mp h
      exact ⟨task, h, eq ▸ sat⟩
  have full := SourceChain.traces (SerializedGenerate.algorithm threshold k).code (LeafRegion.calls solver k).code
    s generated final genTime callTime live genHalt genTrace callTrace
  refine ⟨genTime + callTime, final.relocate (SerializedGenerate.algorithm threshold k).code.length,
    ?_, full, callHalt, boolean, correct.trans meaning⟩
  rw [length] at callBound
  omega

end WordRAM.Conjectures.Sparsification.SerializedSolver

/-! Set parser arguments from the relocated public SAT encoding. -/
namespace WordRAM.Conjectures.Sparsification.PublicSetup

private def reg (a : Nat) : SourceOperand := .memory (.direct a)
def records (backup length : Nat) : Nat := backup + length + 15
def workspace (backup length count : Nat) : Nat := records backup length + 3 * count

def algorithm : Algorithm :=
  ⟨[.copy (.direct 16) (reg 6),
    .binary .add (.direct 12) (reg 5) (.immediate 2),
    .binary .add (.direct 13) (reg 5) (.immediate 1),
    .copy (.direct 11) (.memory (.indirect 13)),
    .binary .add (.direct 13) (reg 5) (reg 7),
    .binary .add (.direct 13) (reg 13) (.immediate 15),
    .binary (.mul rfl) (.direct 27) (.immediate 3) (reg 11),
    .binary .add (.direct 27) (reg 13) (reg 27), .halt], 1, by decide⟩

theorem prepares (s : State w) (backup length variables count : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (low : 32 ≤ backup) (fits : backup + 1 < 2 ^ w.bits)
    (bp : s.mem 5 = BitVec.ofNat w.bits backup)
    (nv : s.mem 6 = BitVec.ofNat w.bits variables)
    (len : s.mem 7 = BitVec.ofNat w.bits length)
    (clauses : s.mem (backup + 1) = BitVec.ofNat w.bits count) :
    let t := run widthConstant (algorithm.program w) 9 s
    t.halted = true ∧ t.ticks = s.ticks + 9 ∧
      t.mem 16 = BitVec.ofNat w.bits variables ∧ t.mem 11 = BitVec.ofNat w.bits count ∧
      t.mem 12 = BitVec.ofNat w.bits (backup + 2) ∧
      t.mem 13 = BitVec.ofNat w.bits (records backup length) ∧
      t.mem 27 = BitVec.ofNat w.bits (workspace backup length count) ∧
      (∀ a, 32 ≤ a → t.mem a = s.mem a) := by
  have header : backup + 1 ≠ 16 ∧ backup + 1 ≠ 12 ∧ backup + 1 ≠ 13 := by omega
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
    pc, live, Nat.add_assoc, bp, nv, len, ← BitVec.ofNat_add, ← BitVec.ofNat_mul,
    Nat.mod_eq_of_lt fits, header, clauses, records, workspace]
  intro a ha
  have neq : a ≠ 16 ∧ a ≠ 12 ∧ a ≠ 13 ∧ a ≠ 11 ∧ a ≠ 27 := by omega
  simp [neq]

def setupPrefix : Algorithm :=
  ⟨SourceChain.code InputRelocation.algorithm.code algorithm.code, 1, by decide⟩

theorem initializes (w : Width) (f : SATInstance) (wide : 6 ≤ w.bits)
    (inputBelow : f.encode.length < InputBootstrap.base w)
    (region : InputBootstrap.base w + max 15 f.encode.length ≤ LeafRegion.base w) :
    ∃ time final, time ≤ 17 * f.encode.length + 56 ∧
      Runs widthConstant (setupPrefix.program w) time (initialState w f.encode) final ∧ final.halted = true ∧
      final.mem 16 = BitVec.ofNat w.bits f.variables ∧
      final.mem 11 = BitVec.ofNat w.bits f.clauses.length ∧
      final.mem 12 = BitVec.ofNat w.bits (InputBootstrap.base w + 2) ∧
      final.mem 13 = BitVec.ofNat w.bits (records (InputBootstrap.base w) f.encode.length) ∧
      final.mem 27 = BitVec.ofNat w.bits (workspace (InputBootstrap.base w) f.encode.length f.clauses.length) ∧
      MaskTable.Encoded final.mem (InputBootstrap.base w + 2) f.clauses ∧
      (∀ a, LeafRegion.base w ≤ a → final.mem a = 0#w.bits) := by
  obtain ⟨time, bound, relocated, trace, halted, bp, nv, len, saved, frame⟩ :=
    InputRelocation.relocates w f wide inputBelow
  have bounds := InputBootstrap.base_bounds wide
  have count : relocated.mem (InputBootstrap.base w + 1) = BitVec.ofNat w.bits f.clauses.length := by
    have h := saved 1 (by simp [SATInstance.encode])
    simpa [SATInstance.encode] using h
  let final := run widthConstant (algorithm.program w) 9 (SourceChain.resume relocated)
  obtain ⟨fh, ft, variables, clauses, pointer, recordPointer, workspacePointer, setupFrame⟩ :=
    prepares (SourceChain.resume relocated) (InputBootstrap.base w) f.encode.length f.variables f.clauses.length
      rfl rfl bounds.1 (by omega) bp nv len count
  obtain ⟨ticks, _, setupTrace⟩ := run_has_trace widthConstant (algorithm.program w) 9 (SourceChain.resume relocated)
  have tickCost := runs_cost setupTrace
  have eq : ticks = 9 := by omega
  subst ticks
  have full := SourceChain.traces InputRelocation.algorithm.code algorithm.code (initialState w f.encode)
    relocated final time 9 rfl halted trace setupTrace
  refine ⟨time + 9, final.relocate InputRelocation.algorithm.code.length, ?_, full, fh,
    variables, clauses, pointer, recordPointer, workspacePointer, ?_, ?_⟩
  · have length := InputScan.encoding_length f
    have span := MaskTable.span_eq f.clauses
    omega
  · apply MaskTable.Encoded.frame _ _ (InputRelocation.encoded_clauses w f relocated.mem (InputBootstrap.base w) saved)
    intro a ha _; exact setupFrame a (by omega)
  · intro a ha
    change final.mem a = 0#w.bits
    rw [setupFrame a (by omega)]
    change relocated.mem a = 0#w.bits
    rw [frame a (by omega) (Or.inr (by omega))]
    simp [initialState, show a ≠ 0 by omega, List.getElem?_eq_none (show f.encode.length ≤ a - 1 by omega)]

end WordRAM.Conjectures.Sparsification.PublicSetup

/-! A uniform SAT machine, beginning at the public input convention, that
relocates its input, sparsifies it, and decides every leaf using a supplied solver.
The subsequent asymptotic argument must discharge its explicit resource bounds. -/
namespace WordRAM.Conjectures.Sparsification.PublicSolver
open TraversalBody TraversalBounds

def algorithm (solver : Algorithm) (threshold : Nat → Nat) (k factor : Nat) (positive : 0 < factor) : Algorithm :=
  ⟨SourceChain.code PublicSetup.setupPrefix.code (SerializedSolver.algorithm solver threshold k).code, factor, positive⟩

def costBound (w : Width) (f : SATInstance) (threshold : Nat → Nat) (k capacity cost : Nat)
    (large : ∀ i, 2 ≤ threshold i) : Nat :=
  17 * f.encode.length + 56 + RecordTable.cost w f.clauses + f.clauses.length * (35 * f.clauses.length + 34) +
    Work.calls (Normalize.normalize f.clauses) threshold k large * (bodyCost f.variables k w.bits capacity + 2) +
    12 * f.clauses.length + 66 + (Tree.leaves f.clauses threshold k large).length * (cost + 2) + 9

theorem executes (solver : Algorithm) (threshold : Nat → Nat) (k factor capacity cost reserve budget finalBudget : Nat)
    (positive : 0 < factor) (large : ∀ i, 2 ≤ threshold i) (w : Width) (f : SATInstance)
    (wide : 6 ≤ w.bits) (variablesFit : f.variables ≤ w.bits)
    (inputBelow : f.encode.length < InputBootstrap.base w)
    (regionRoom : InputBootstrap.base w + max 15 f.encode.length ≤ LeafRegion.base w)
    (controls : dataBase k ≤ InputBootstrap.base w + 2)
    (fits : budget < 2 ^ w.bits) (region : budget ≤ LeafRegion.base w)
    (finalFits : finalBudget < 2 ^ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits)
    (clauseWidth : ∀ clause ∈ f.clauses, clause.length ≤ k)
    (weight : Sparsification.weight f.clauses ≤ capacity)
    (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 k large * stride capacity ≤ budget)
    (eligible : ∀ formula ∈ Tree.leaves f.clauses threshold k large, LeafLoop.Eligible solver w cost reserve formula)
    (leafSpace : LeafRegion.base w + (Tree.leaves f.clauses threshold k large).length * reserve ≤ finalBudget) :
    ∃ time final, time ≤ costBound w f threshold k capacity cost large ∧
      Runs widthConstant ((algorithm solver threshold k factor positive).program w) time (initialState w f.encode) final ∧
      final.halted = true ∧ (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ f.Satisfiable) := by
  obtain ⟨setupTime, prepared, setupBound, setupTrace, setupHalt, variables, count, pointer,
    recordPointer, workspacePointer, input, fresh⟩ := PublicSetup.initializes w f wide inputBelow regionRoom
  have inputBefore : InputBootstrap.base w + 2 + MaskTable.span f.clauses ≤
      PublicSetup.records (InputBootstrap.base w) f.encode.length := by
    have len := InputScan.encoding_length f
    unfold PublicSetup.records
    omega
  obtain ⟨time, final, bound, trace, halted, boolean, correct⟩ :=
    SerializedSolver.decides solver cost reserve finalBudget f.clauses threshold k capacity budget large
      (SourceChain.resume prepared) (InputBootstrap.base w + 2)
      (PublicSetup.records (InputBootstrap.base w) f.encode.length)
      (PublicSetup.workspace (InputBootstrap.base w) f.encode.length f.clauses.length)
      rfl rfl controls inputBefore (Nat.le_refl _) fits variablesFit (by omega) thresholdFits
      variables count pointer recordPointer workspacePointer input clauseWidth weight space region finalFits fresh eligible leafSpace
  have full := SourceChain.traces PublicSetup.setupPrefix.code (SerializedSolver.algorithm solver threshold k).code
    (initialState w f.encode) prepared final setupTime time rfl setupHalt setupTrace trace
  refine ⟨setupTime + time, final.relocate PublicSetup.setupPrefix.code.length, ?_, full, halted, boolean, correct⟩
  unfold costBound
  omega

end WordRAM.Conjectures.Sparsification.PublicSolver

/-! Uniform sizes of sparse SAT encodings, including unused variables. -/
namespace WordRAM.Conjectures.Sparsification.EncodingBounds

def lengthBound (k density n : Nat) : Nat := 2 + density * n * (1 + 2 * k)
def magnitudeBound (k density n : Nat) : Nat := n + k + 2 * lengthBound k density n + 2

theorem span_le (formula : CNF n) (width : ∀ clause ∈ formula, clause.length ≤ k) :
    MaskTable.span formula ≤ formula.length * (1 + 2 * k) := by
  induction formula with
  | nil => simp [MaskTable.span]
  | cons clause rest ih =>
    have head := width clause (by simp)
    have tail := ih (fun c hc => width c (by simp [hc]))
    have scaled := Nat.mul_le_mul_left 2 head
    simp only [MaskTable.span, List.length_cons, Nat.add_mul, Nat.one_mul]
    omega

theorem length_le (f : SATInstance) (width : f.IsKCNF k) (sparse : f.clauses.length ≤ density * f.variables) :
    f.encode.length ≤ lengthBound k density f.variables := by
  have span := span_le f.clauses width
  have scaled := Nat.mul_le_mul_right (1 + 2 * k) sparse
  rw [InputScan.encoding_length]
  unfold lengthBound
  omega

theorem value_le (f : SATInstance) (width : f.IsKCNF k) (value : Nat) (member : value ∈ f.encode) :
    value ≤ f.variables + k + f.encode.length + 1 := by
  have clauses : f.clauses.length ≤ f.encode.length := by
    have span := MaskTable.span_eq f.clauses
    have len := InputScan.encoding_length f
    omega
  simp only [SATInstance.encode, List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at member
  rcases member with (eq | eq) | member
  · omega
  · omega
  · obtain ⟨clause, hc, member⟩ := List.mem_flatMap.mp member
    simp only [List.mem_cons] at member
    rcases member with eq | member
    · have bound := width clause hc; omega
    · obtain ⟨literal, _, member⟩ := List.mem_flatMap.mp member
      simp only [List.mem_cons, List.not_mem_nil, or_false] at member
      rcases member with eq | eq
      · have bound := literal.index.isLt; omega
      · split at eq <;> omega

private theorem fold_le (xs : List Nat) (seed bound : Nat) (initial : seed ≤ bound)
    (values : ∀ x ∈ xs, x ≤ bound) : xs.foldl max seed ≤ bound := by
  induction xs generalizing seed with
  | nil => exact initial
  | cons x xs ih =>
    apply ih (max seed x) (by have := values x (by simp); omega)
    intro a ha; exact values a (by simp [ha])

theorem magnitude_general (f : SATInstance) (width : f.IsKCNF k) :
    inputMagnitude f.encode ≤ f.variables + k + 2 * f.encode.length + 2 := by
  have folded := fold_le f.encode f.encode.length (f.variables + k + f.encode.length + 1)
    (by omega) (value_le f width)
  unfold inputMagnitude
  omega

theorem magnitude_le (f : SATInstance) (width : f.IsKCNF k) (sparse : f.clauses.length ≤ density * f.variables) :
    inputMagnitude f.encode ≤ magnitudeBound k density f.variables := by
  have len := length_le f width sparse
  have values := value_le f width
  have folded := fold_le f.encode f.encode.length (f.variables + k + f.encode.length + 1) (by omega) values
  unfold inputMagnitude magnitudeBound
  omega

theorem canonical_length (formula : CNF n) (width : ∀ clause ∈ formula, clause.length ≤ k)
    (sparse : formula.length ≤ density * n) :
    (LeafCall.satInput formula).encode.length ≤ lengthBound k density n :=
  length_le _ (Canonical.width formula width) (by simpa only [LeafCall.satInput, Canonical.formula_length] using sparse)

theorem canonical_magnitude (formula : CNF n) (width : ∀ clause ∈ formula, clause.length ≤ k)
    (sparse : formula.length ≤ density * n) :
    inputMagnitude (LeafCall.satInput formula).encode ≤ magnitudeBound k density n :=
  magnitude_le _ (Canonical.width formula width) (by simpa only [LeafCall.satInput, Canonical.formula_length] using sparse)

end WordRAM.Conjectures.Sparsification.EncodingBounds