Deterministic SETH and the Orthogonal Vectors Conjecture on the word RAM

Definition

WordRAM_Conjectures

by wurtle · Oct 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

computational-complexityfine-grained-complexitysatisfiabilityword-ram

Definitions of the deterministic Strong Exponential Time Hypothesis (SETH) and the low-dimensional Orthogonal Vectors Conjecture (OVC) over a concrete word RAM. Running time is the number of instructions a fixed program actually executes, with no abstract "fast algorithm" predicate.

Machine and algorithms. The machine is the multiplication word RAM of Def_WordRAMEquivalence_Foundation1. Each instruction takes one step. Words are $w$ -bit, and the instructions are $+,-,\cdot$ modulo $2^w$ , shifts, AND, OR, NOT, copy, unsigned comparisons and branches, jumps and halt, with direct and indirect addressing. This file adds the exact-step relation $s \xrightarrow{t} s'$ : precisely $t$ successful instruction executions lead from $s$ to $s'$ . An algorithm $a$ consists of:

a finite program, the same at every input size, whose immediates are natural-number literals truncated to $w$ bits and whose only built-in constant is the word width $w$ ;
a positive constant $\lambda_a$ , its word-size factor.

On input $x=(x_1,\dots,x_L)\in\mathbb N^L$ , with an extra-bits parameter $e$ , let $M(x)=\max(x_1,\dots,x_L,L)+1$ . The algorithm runs with word width

w = \lambda_a\,\bigl(e+\lfloor\log_2 M(x)\rfloor+1\bigr).

Cell $0$ holds the output and starts at $0$ . Cells $1,\dots,L$ hold $x_1,\dots,x_L$ reduced modulo $2^w$ , and every other cell is $0$ . We say $a$ decides $P$ on $x$ in $t$ steps if the machine runs exactly $t$ steps from this state to a halted state whose cell $0$ holds $0$ or $1$ , and cell $0$ holds $1$ if and only if $P$ holds.

$k$ -SAT. A CNF formula $F$ has $n$ variables and a list of $m$ clauses of literals. $F$ is a $k$ -CNF if every clause has at most $k$ literals. Empty clauses and repeated literals are allowed. $F$ is encoded as $\langle F\rangle=(n,m,\ \text{for each clause: its length, then a (variable index, polarity) pair per literal})$ , and $L_F$ is the length of this list. For natural numbers $k$ and $q$ , $\mathrm{FastSAT}(k,q)$ says there are an algorithm $a$ and constants $C>0$ , $p$ , $n_0$ such that, for every $k$ -CNF $F$ , $a$ decides satisfiability of $F$ on $\langle F\rangle$ with $e=n$ in some $t$ steps, where

n\ge n_0 \implies t^{q}\le C\cdot 2^{(q-1)n}\,(L_F+1)^{p}.

That is, $t=O\!\bigl(2^{(1-1/q)n}\operatorname{poly}(L_F)\bigr)$ .

\textbf{SETH}:\qquad \forall q\ge 2\ \ \exists k\ge 3:\ \neg\,\mathrm{FastSAT}(k,q).

Orthogonal Vectors. An OV instance consists of two lists $u_1,\dots,u_n$ and $v_1,\dots,v_n$ in $\{0,1\}^d$ . Duplicates are allowed. The question is whether some $u_i,v_j$ are orthogonal, that is, share no coordinate equal to $1$ . The instance is encoded as $(n,d)$ followed by all bits of the left list in row order, then the right list, one word per bit. For natural numbers $c$ and $q$ , $\mathrm{FastOV}(c,q)$ says there are an algorithm $a$ and constants $C>0$ , $n_0$ such that, for every instance with $n\ge 2$ and $d\le c\,\lceil\log_2 n\rceil$ , $a$ decides the instance with $e=0$ in some $t$ steps, where

n\ge n_0 \implies t^{q}\le C\cdot n^{2q-1}.

That is, $t=O(n^{2-1/q})$ .

\textbf{OVC}:\qquad \forall q\ge 2\ \ \exists c\ge 1:\ \neg\,\mathrm{FastOV}(c,q).

The file also defines the proposition $\mathrm{SETH}\Rightarrow\mathrm{OVC}$ as SETHImpliesOV. These are the standard hypotheses of fine-grained complexity, fixed here to one machine model, input encoding and step count so that conditional lower bounds can be stated and proved without hidden assumptions.

Formalization Note The improvement $\varepsilon$ ranges over $1/q$ with $q\ge2$ , which is enough to rule out every fixed $\varepsilon>0$ . Raising $t$ to the power $q$ keeps the bounds in $\mathbb N$ . The hypotheses are deterministic, whereas Cygan et al. allow bounded-error randomized algorithms. A solver must decide every input correctly, including inputs below $n_0$ . SAT runs get $n$ extra word bits, so a $2^{O(n)}$ -size workspace is addressable. OV runs get logarithmic words. The ceiling uses $\lceil\log_2 n\rceil = \lfloor\log_2(n-1)\rfloor+1$ for $n\ge2$ . Lean names: WordRAM.Runs, WordRAM.Conjectures.{Algorithm, DecidesIn, SATInstance, HasFastSAT, SETH, OVInstance, HasFastOV, OVConjecture, SETHImpliesOV}.

Definition code

import Definitions.Def_WordRAMEquivalence_Foundation1

set_option autoImplicit true

namespace WordRAM

/-- Exactly `n` successful instruction executions; allows unbounded reasoning
about finite executions independently of the fuel-based interpreter. -/
inductive Runs (constants : NativeConstants k) (p : Program w m k) :
    Nat → State w → State w → Prop where
  | refl (s) : Runs constants p 0 s s
  | cons : step constants p s = some t → Runs constants p n t u →
      Runs constants p (n + 1) s u

end WordRAM


/-!
# Deterministic SETH and the Orthogonal Vectors conjecture

These definitions use the multiplication word RAM from `Basic`, fixed finite
programs, explicit input encodings, and its actual instruction-step relation.
They do not take an unspecified "fast solver" predicate as a parameter.

Reference conventions:
* Cygan et al., On Problems as Hard as CNFSAT, https://arxiv.org/abs/1112.2275
* Abboud, Vassilevska Williams, Wang, §1.2 (OVC and SETH ⇒ OVC):
  https://theory.stanford.edu/~virgi/dirRad.pdf

We quantify over improvements ε = 1/q, q ≥ 2. This suffices to express the
absence of ANY fixed positive improvement. Natural-number inequalities on
t^q express the rational-exponent time bounds without importing real analysis.
Equivalence with other machine/encoding conventions is not proved here.

`SETHImpliesOV` at the end is a proposition stating the desired implication,
NOT a proof or an axiom asserting it.

`WordRAM.Runs` is the exact-step execution relation from the source model's
`Basic.lean`; the rest of the word-RAM model is imported unchanged from
`Def_WordRAMEquivalence_Foundation1`.
-/
namespace WordRAM.Conjectures

/-! ## Finite, uniform programs -/

/-- An immediate is a fixed natural literal in finite source code, not an
arbitrary function of word width. Compilation truncates it to a word. -/
inductive SourceOperand where
  | immediate (literal : Nat)
  | memory (address : Address)
  deriving Repr

def SourceOperand.compile (w : Width) : SourceOperand → Operand w
  | .immediate n => .immediate (BitVec.ofNat w.bits n)
  | .memory a => .memory a

/-- One syntax tree is used at every input size and word width. The only native
constant available to these algorithms is the word width itself. -/
inductive SourceInstruction where
  | copy (dst : Address) (src : SourceOperand)
  | binary (op : BinOp .multiplication) (dst : Address) (x y : SourceOperand)
  | bitNot (dst : Address) (src : SourceOperand)
  | wordWidth (dst : Address)
  | jump (target : Nat)
  | branch (cmp : Comparison) (x y : SourceOperand) (target : Nat)
  | halt
  deriving Repr

def SourceInstruction.compile (w : Width) : SourceInstruction → Instruction w .multiplication 1
  | .copy dst src => .copy dst (src.compile w)
  | .binary op dst x y => .binary op dst (x.compile w) (y.compile w)
  | .bitNot dst src => .bitNot dst (src.compile w)
  | .wordWidth dst => .native dst ⟨0, by decide⟩
  | .jump target => .jump target
  | .branch cmp x y target => .branch cmp (x.compile w) (y.compile w) target
  | .halt => .halt

structure Algorithm where
  code : List SourceInstruction
  /-- Fixed constant factor in the word-size convention, independent of input. -/
  wordFactor : Nat
  wordFactor_pos : 0 < wordFactor

def Algorithm.program (a : Algorithm) (w : Width) : Program w .multiplication 1 :=
  a.code.map (SourceInstruction.compile w)

def widthConstant : NativeConstants 1 := fun w _ => BitVec.ofNat w.bits w.bits

/-- The maximum includes the input length to allow addressing all input cells. -/
def inputMagnitude (input : List Nat) : Nat := input.foldl max input.length + 1

/-- OV uses extraBits = 0 (logarithmic words). SAT uses extraBits = n to
permit addresses into exponential workspace. Polynomial-bit SAT operations
are the convention here; machine-simulation equivalences are not proved. -/
def Algorithm.width (a : Algorithm) (input : List Nat) (extraBits : Nat) : Width :=
  ⟨a.wordFactor * (extraBits + (inputMagnitude input).log2 + 1),
    Nat.mul_pos a.wordFactor_pos (by omega)⟩

/-- Output is cell 0; input words begin at cell 1; other memory starts at zero.
Input loading is a convention outside the measured instruction count. -/
def initialState (w : Width) (input : List Nat) : State w :=
  { mem := fun address =>
      if address = 0 then 0
      else BitVec.ofNat w.bits (input[address - 1]?.getD 0) }

/-- An ACTUAL t-step execution, ending in halt with output exactly 0 or 1.
The final output is 1 iff the input's mathematical decision predicate holds. -/
def DecidesIn (a : Algorithm) (input : List Nat) (extraBits t : Nat)
    (answer : Prop) : Prop :=
  let w := a.width input extraBits
  ∃ final : State w,
    Runs widthConstant (a.program w) t (initialState w input) final ∧
    final.halted = true ∧
    (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧
    (final.mem 0 = 1 ↔ answer)

/-! ## k-CNF satisfiability -/

structure Literal (n : Nat) where
  index : Fin n
  positive : Bool
  deriving DecidableEq, Repr

def Literal.eval (assignment : Fin n → Bool) (literal : Literal n) : Bool :=
  if literal.positive then assignment literal.index else !(assignment literal.index)

structure SATInstance where
  variables : Nat
  clauses : List (List (Literal variables))

/-- Clauses have AT MOST k literals. Empty clauses and duplicate literals are
allowed, with their ordinary Boolean meanings. -/
def SATInstance.IsKCNF (f : SATInstance) (k : Nat) : Prop :=
  ∀ clause ∈ f.clauses, clause.length ≤ k

def SATInstance.Satisfiable (f : SATInstance) : Prop :=
  ∃ assignment : Fin f.variables → Bool,
    ∀ clause ∈ f.clauses, ∃ literal ∈ clause, literal.eval assignment = true

/-- Encoding: n, number of clauses, then for each clause its length followed
by (variable index, polarity) pairs. Positive polarity is 1, negative is 0. -/
def SATInstance.encode (f : SATInstance) : List Nat :=
  [f.variables, f.clauses.length] ++ f.clauses.flatMap fun clause =>
    clause.length :: clause.flatMap fun literal =>
      [literal.index.val, if literal.positive then 1 else 0]

/-- A uniform deterministic solver in O(2^((1−1/q)n) · L^O(1)) time,
where L is encoded input length. Raising the time to q avoids real powers:
t^q ≤ C · 2^((q−1)n) · (L+1)^p. The polynomial exponent p is unrestricted.
Correctness/termination is required also below the asymptotic threshold n₀. -/
def HasFastSAT (k q : Nat) : Prop :=
  ∃ a : Algorithm, ∃ C p n₀ : Nat, 0 < C ∧
    ∀ f : SATInstance, f.IsKCNF k →
      ∃ t : Nat, DecidesIn a f.encode f.variables t f.Satisfiable ∧
        (n₀ ≤ f.variables →
          t ^ q ≤ C * 2 ^ ((q - 1) * f.variables) * (f.encode.length + 1) ^ p)

/-- For every fixed exponential improvement, some fixed clause width k is hard.
The solver and its constants may depend on k and q, but not on the instance. -/
def SETH : Prop :=
  ∀ q : Nat, 2 ≤ q → ∃ k : Nat, 3 ≤ k ∧ ¬ HasFastSAT k q

/-! ## Bichromatic Boolean Orthogonal Vectors -/

abbrev BooleanVector (d : Nat) := Fin d → Bool

/-- For Boolean coordinates, dot product zero means no shared 1 coordinate. -/
def Orthogonal (x y : BooleanVector d) : Prop :=
  ∀ i : Fin d, x i = false ∨ y i = false

/-- Two lists, each containing n vectors of common dimension d. Duplicates
are allowed; the pair must contain one vector from each list. -/
structure OVInstance where
  count : Nat
  dimension : Nat
  left : Fin count → BooleanVector dimension
  right : Fin count → BooleanVector dimension

def OVInstance.HasOrthogonalPair (v : OVInstance) : Prop :=
  ∃ i j : Fin v.count, Orthogonal (v.left i) (v.right j)

/-- Encoding: n, d, then all bits of the left list in row order, then the right
list. A coordinate takes one word; no compression or precomputed answers. -/
def OVInstance.encode (v : OVInstance) : List Nat :=
  [v.count, v.dimension] ++
    (List.ofFn fun i : Fin v.count =>
      List.ofFn fun j : Fin v.dimension => if v.left i j then 1 else 0).flatten ++
    (List.ofFn fun i : Fin v.count =>
      List.ofFn fun j : Fin v.dimension => if v.right i j then 1 else 0).flatten

/-- ceil(log₂ n) for n ≥ 2 (the only counts used in the conjecture). -/
def ceilLog2 (n : Nat) : Nat := (n - 1).log2 + 1

/-- O(n^(2−1/q)) time for all dimensions d ≤ c·ceil(log₂ n).
The single program may depend on c and q, but must work for every valid input.
Constants and the threshold are independent of n, d, and the vector contents. -/
def HasFastOV (c q : Nat) : Prop :=
  ∃ a : Algorithm, ∃ C n₀ : Nat, 0 < C ∧
    ∀ v : OVInstance, 2 ≤ v.count → v.dimension ≤ c * ceilLog2 v.count →
      ∃ t : Nat, DecidesIn a v.encode 0 t v.HasOrthogonalPair ∧
        (n₀ ≤ v.count → t ^ q ≤ C * v.count ^ (2 * q - 1))

/-- For every fixed subquadratic improvement, some constant logarithmic
dimension factor c is hard. This is the deterministic, low-dimensional OVC. -/
def OVConjecture : Prop :=
  ∀ q : Nat, 2 ≤ q → ∃ c : Nat, 1 ≤ c ∧ ¬ HasFastOV c q

/-- The requested STATEMENT. No theorem asserting it has been proved here.
A proof requires a SAT-to-OV reduction, sparsification (for logarithmic
dimension), and verified running-time/machine simulations. -/
def SETHImpliesOV : Prop := SETH → OVConjecture

end WordRAM.Conjectures

Source

SETH: Marek Cygan, Holger Dell, Daniel Lokshtanov, Dániel Marx, Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh, Magnus Wahlström, On Problems as Hard as CNF-SAT, ACM Trans. Algorithms 12(3):41, 2016, https://doi.org/10.1145/2925416 , arXiv:1112.2275 (https://arxiv.org/abs/1112.2275): SETH stated in §1, p. 2, and defined formally in §2.2 (Definition 2.1 and the paragraph after it, p. 9) as lim_{k→∞} σ(k-CNF-Sat/n) = 1. OVC: Amir Abboud, Virginia Vassilevska Williams, Joshua Wang, Approximation and Fixed Parameter Subquadratic Algorithms for Radius and Diameter in Sparse Graphs, SODA 2016, pp. 377–391, arXiv:1506.01799 (https://arxiv.org/abs/1506.01799): "The Orthogonal Vectors Conjecture", §1, p. 2, with the remark that Williams [52] showed SETH implies it. Lean source: the contributor's WordRAM project (private repository), commit 24159584b91d0e5298def8cd6491aafd480b8f2a: WordRAM/Conjectures.lean (every declaration, unchanged) and WordRAM/Basic.lean lines 191–198 (WordRAM.Runs). The rest of the word-RAM model is imported from Def_WordRAMEquivalence_Foundation1, which is identical to that commit's WordRAM/Basic.lean apart from explicit `variable` binders.

Human review

Endorsed by Community (Bot) · Oct 28, 2026
Endorsed by wurtle · Oct 28, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by Shuze Chen · Nov 8, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Nov 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph