Prove2Me

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

Definition
SETHOV_Sparsification_24

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

fine-grained-complexityorthogonal-vectorssethsparsificationword-ram

Bundle 24 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_23

set_option autoImplicit true

/-! Connecting actual serialized literal input to complete clause normalization. -/
namespace WordRAM.Conjectures.Sparsification.SerializedNormalize

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

def save : Algorithm :=
  ⟨[.copy (.direct 25) (reg 11), .copy (.direct 26) (reg 13), .halt], 1, by decide⟩

def bridge : Algorithm :=
  ⟨[.copy (.direct 11) (reg 25), .copy (.direct 12) (reg 26), .copy (.direct 13) (reg 27), .halt], 1, by decide⟩

/-- Inputs: clause count 11, serialized input cursor 12, record buffer 13,
normalization workspace 27. Returns normalized table pointer 22 and count 24. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code save.code (SourceChain.code RecordTable.algorithm.code
    (SourceChain.code bridge.code NormalizeMachine.initialized.code)), 1, by decide⟩

theorem saves (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (save.program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 25 = s.mem 11 ∧ t.mem 26 = s.mem 13 ∧
      (∀ a, a ≠ 25 → a ≠ 26 → t.mem a = s.mem a) := by
  simp [save, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h25 h26; simp [h25, h26]

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 11 = s.mem 25 ∧ t.mem 12 = s.mem 26 ∧
      t.mem 13 = s.mem 27 ∧ (∀ a, a ≠ 11 → a ≠ 12 → a ≠ 13 → t.mem a = s.mem a) := by
  simp [bridge, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h11 h12 h13; simp [h11, h12, h13]

private theorem trace_of_ticks (program : Program w .multiplication 1) (s : State w) (fuel : Nat)
    (cost : (run widthConstant program fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant program fuel s (run widthConstant program fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant program fuel s
  have ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time
  exact trace

/-- Every step from original serialized literals to the normalized table,
including mask construction, deduplication, size calculation, and subsumption. -/
theorem normalizes (clauses : CNF n) (s : State w) (source records workspace : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
    (inputBefore : source + MaskTable.span clauses ≤ records)
    (recordsBefore : records + 3 * clauses.length ≤ workspace)
    (fits : workspace + clauses.length * (3 * (clauses.length + 1)) < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits)
    (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) :
    ∃ time final resultAddress,
      time ≤ RecordTable.cost w clauses + clauses.length * (35 * clauses.length + 34) + 20 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem resultAddress (RecordTable.words w (Normalize.normalize clauses)) ∧
      final.mem 22 = BitVec.ofNat w.bits resultAddress ∧
      final.mem 24 = BitVec.ofNat w.bits (Normalize.normalize clauses).length ∧
      records + 3 * clauses.length ≤ resultAddress ∧
      resultAddress + 3 * (Normalize.normalize clauses).length ≤ workspace + clauses.length * (3 * (clauses.length + 1)) ∧
      (∀ a, 32 ≤ a → (a < records ∨ records + 3 * clauses.length ≤ a) →
        (a < workspace ∨ workspace + clauses.length * (3 * (clauses.length + 1)) ≤ a) → final.mem a = s.mem a) := by
  let saved := run widthConstant (save.program w) 3 s
  obtain ⟨savedHalt, savedTicks, savedCount, savedPointer, sf⟩ := saves s pc live
  have savedInput : MaskTable.Encoded saved.mem source clauses := by
    apply MaskTable.Encoded.frame _ _ input
    intro a lo _; exact sf a (by omega) (by omega)
  obtain ⟨parsed, parseTrace, parsedHalt, table, pf⟩ :=
    RecordTable.builds clauses (SourceChain.resume saved) source records rfl rfl (by omega) inputBefore (by omega) variablesFit
      ((sf 12 (by decide) (by decide)).trans pointer)
      ((sf 11 (by decide) (by decide)).trans count)
      ((sf 13 (by decide) (by decide)).trans recordPointer) savedInput
  have parsedCount : parsed.mem 25 = BitVec.ofNat w.bits clauses.length :=
    (pf 25 (by decide) (Or.inl (by omega))).trans (savedCount.trans count)
  have parsedPointer : parsed.mem 26 = BitVec.ofNat w.bits records :=
    (pf 26 (by decide) (Or.inl (by omega))).trans (savedPointer.trans recordPointer)
  have parsedWorkspace : parsed.mem 27 = BitVec.ofNat w.bits workspace :=
    (pf 27 (by decide) (Or.inl (by omega))).trans ((sf 27 (by decide) (by decide)).trans workspacePointer)
  let middle := run widthConstant (bridge.program w) 4 (SourceChain.resume parsed)
  obtain ⟨middleHalt, middleTicks, mc, mp, md, mf⟩ := bridges (SourceChain.resume parsed) rfl rfl
  have nextInput : VectorBuilder.Stored middle.mem records (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a lo _; exact mf a (by omega) (by omega) (by omega)
  obtain ⟨time, out, resultAddress, bound, trace, outHalt, normalized, resultPointer, resultCount, lower, upper, nf⟩ :=
    NormalizeMachine.normalizes clauses (SourceChain.resume middle) records workspace rfl rfl (by omega)
      recordsBefore fits variablesFit (mc.trans parsedCount) (mp.trans parsedPointer) (md.trans parsedWorkspace) nextInput
  have tail := SourceChain.traces bridge.code NormalizeMachine.initialized.code (SourceChain.resume parsed) middle out
    4 time rfl middleHalt (trace_of_ticks _ _ 4 middleTicks) trace
  have body := SourceChain.traces RecordTable.algorithm.code (SourceChain.code bridge.code NormalizeMachine.initialized.code)
    (SourceChain.resume saved) parsed _ (RecordTable.cost w clauses) (4 + time) rfl parsedHalt parseTrace tail
  have full := SourceChain.traces save.code
    (SourceChain.code RecordTable.algorithm.code (SourceChain.code bridge.code NormalizeMachine.initialized.code))
    s saved _ 3 (RecordTable.cost w clauses + (4 + time)) live savedHalt (trace_of_ticks _ s 3 savedTicks) body
  refine ⟨3 + (RecordTable.cost w clauses + (4 + time)),
    ((out.relocate bridge.code.length).relocate RecordTable.algorithm.code.length).relocate save.code.length,
    resultAddress, by omega, full, outHalt, normalized, resultPointer, resultCount, lower, upper, ?_⟩
  intro a ha outsideRecords outsideWorkspace
  exact (nf a ha outsideWorkspace).trans
    ((mf a (by omega) (by omega) (by omega)).trans
      ((pf a (by omega) outsideRecords).trans (sf a (by omega) (by omega))))

end WordRAM.Conjectures.Sparsification.SerializedNormalize
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