Cook–Levin tableau core

This file defines the Cook–Levin tableau formula and proves its semantic correctness. The polynomial-time emitter, reductions, and final theorem SAT.NPComplete_language are assembled in SAT/CookLevin/Assembly.lean. Membership language ∈ NP is supplied by SAT/Headline.lean.

Completed development

NPComplete_language                       (= ⟨language_mem_NP, NPHard_language⟩)
└ NPHard_language                         (unpack any L ∈ NP → its NTM)
  └ cookLevin_reduction               (multi-tape → single-tape, then ↓)
    ├ NTM.exists_singleTape_decidesInTime   (SingleTape.lean)
    └ cookLevin_reduction_singleTape
        ├ reductionFn                 (def: x ↦ (tableauCNFFlat …).encode)
        ├ reductionFn_mem_FP          ✓ poly-time emitter TM
        └ tableauCNF_correct          (= encode_mem_LSAT_iff ∘ B ∘ hdec)
            ├ tableauCNF              ✓ the tableau formula
            ├ tableauCNF_satisfiable_iff  ✓ sat ↔ accepting computation
            └ encode_mem_LSAT_iff     ✓ (CNF.encode injective)

All nodes in this outline are proved. The reduction machine and final NP-hardness/NP-completeness assembly live in SAT/CookLevin/Assembly.lean; the emitter implementation is split across the modules under SAT/CookLevin/.

Tableau variable encoding

The computation-tableau formula's Boolean variables are indexed by ℕ. Each "atom" of the tableau — a state bit, a nondeterministic choice bit, a tape-cell bit, or a head-position bit, all indexed by a time-step — is injected into ℕ by iterated Nat.pair, so distinct atoms receive distinct SAT variables.

def Complexity.SAT.Tableau.enc (tag a b c d : ℕ) : ℕ

Inject a tagged 4-tuple of naturals into one natural by iterated Nat.pair.

Equations

• Complexity.SAT.Tableau.enc tag a b c d = Nat.pair tag (Nat.pair a (Nat.pair b (Nat.pair c d)))

theorem Complexity.SAT.Tableau.enc_inj {tag a b c d tag' a' b' c' d' : ℕ} (h : enc tag a b c d = enc tag' a' b' c' d') : tag = tag' ∧ a = a' ∧ b = b' ∧ c = c' ∧ d = d'

enc is injective on each component (it is a composition of bijective pairings).

def Complexity.SAT.Tableau.vState (t q : ℕ) : ℕ

Variable: at time t the machine is in the state with index q (one-hot).

Equations

• Complexity.SAT.Tableau.vState t q = Complexity.SAT.Tableau.enc 0 t q 0 0

def Complexity.SAT.Tableau.vChoice (t : ℕ) : ℕ

Variable: at time t the nondeterministic choice bit is true.

Equations

• Complexity.SAT.Tableau.vChoice t = Complexity.SAT.Tableau.enc 1 t 0 0 0

def Complexity.SAT.Tableau.vCell (t tp pos s : ℕ) : ℕ

Variable: at time t, cell pos of tape tp holds the symbol with index s.

Equations

• Complexity.SAT.Tableau.vCell t tp pos s = Complexity.SAT.Tableau.enc 2 t tp (Nat.pair pos s) 0

def Complexity.SAT.Tableau.vHead (t tp pos : ℕ) : ℕ

Variable: at time t, the head of tape tp is at cell pos.

Equations

• Complexity.SAT.Tableau.vHead t tp pos = Complexity.SAT.Tableau.enc 3 t tp pos 0

def Complexity.SAT.Tableau.symIdx : Γ → ℕ

The symbol index of a tape symbol: 0,1,2,3 for 0,1,□,▷. Injective, so a one-hot encoding over {0,1,2,3} faithfully names the four tape symbols.

Equations

• Complexity.SAT.Tableau.symIdx Complexity.Γ.zero = 0
• Complexity.SAT.Tableau.symIdx Complexity.Γ.one = 1
• Complexity.SAT.Tableau.symIdx Complexity.Γ.blank = 2
• Complexity.SAT.Tableau.symIdx Complexity.Γ.start = 3

theorem Complexity.SAT.Tableau.symIdx_inj : Function.Injective symIdx

symIdx is injective: distinct tape symbols receive distinct indices.

def Complexity.SAT.Tableau.atLeastOne (vars : List ℕ) : Clause

"At least one of vars is true": the single disjunction of positive literals.

Equations

• Complexity.SAT.Tableau.atLeastOne vars = List.map (fun (v : ℕ) => { sign := true, var := v }) vars

def Complexity.SAT.Tableau.atMostOne : List ℕ → List Clause

"At most one of vars is true": for every ordered pair (vᵢ, vⱼ) the binary clause ¬vᵢ ∨ ¬vⱼ.

Equations

• Complexity.SAT.Tableau.atMostOne [] = []
• Complexity.SAT.Tableau.atMostOne (v :: vs) = List.map (fun (w : ℕ) => [{ sign := false, var := v }, { sign := false, var := w }]) vs ++ Complexity.SAT.Tableau.atMostOne vs

def Complexity.SAT.Tableau.exactlyOne (vars : List ℕ) : List Clause

"Exactly one of vars is true" as a list of clauses (at-least-one and the pairwise at-most-one constraints).

Equations

• Complexity.SAT.Tableau.exactlyOne vars = Complexity.SAT.Tableau.atLeastOne vars :: Complexity.SAT.Tableau.atMostOne vars

theorem Complexity.SAT.Tableau.atLeastOne_eval (α : Assignment) (vars : List ℕ) : Clause.eval α (atLeastOne vars) = vars.any fun (v : ℕ) => α.get v

The at-least-one clause is satisfied iff some variable in the list is true.

theorem Complexity.SAT.Tableau.atLeastOne_sat (α : Assignment) (vars : List ℕ) : Clause.eval α (atLeastOne vars) = true ↔ ∃ v ∈ vars, α.get v = true

The at-least-one clause is satisfied iff some listed variable is true (Prop form).

theorem Complexity.SAT.Tableau.atMostOne_sat (α : Assignment) (vars : List ℕ) : CNF.eval α (atMostOne vars) = true ↔ List.Pairwise (fun (v w : ℕ) => ¬(α.get v = true ∧ α.get w = true)) vars

The at-most-one clauses are satisfied iff no two listed variables are both true.

theorem Complexity.SAT.Tableau.exactlyOne_sat (α : Assignment) (vars : List ℕ) : CNF.eval α (exactlyOne vars) = true ↔ (∃ v ∈ vars, α.get v = true) ∧ List.Pairwise (fun (v w : ℕ) => ¬(α.get v = true ∧ α.get w = true)) vars

The exactly-one clauses are satisfied iff exactly one listed variable is true (some variable is true, and no two are). The decoder for one-hot slots.

theorem Complexity.SAT.Tableau.atMostOne_unique {α : Assignment} {vars : List ℕ} {v w : ℕ} (h : List.Pairwise (fun (a b : ℕ) => ¬(α.get a = true ∧ α.get b = true)) vars) (hv : v ∈ vars) (hw : w ∈ vars) (hvt : α.get v = true) (hwt : α.get w = true) : v = w

Under the at-most-one (pairwise) constraint, any two true listed variables coincide — the uniqueness half of one-hot decoding.

theorem Complexity.SAT.Tableau.clause_cond_conseq (α : Assignment) (cond : Clause) (c : Lit) (hsat : Clause.eval α (cond ++ [c]) = true) (hcond : List.any cond (Lit.eval α) = false) : Lit.eval α c = true

An implication clause cond ++ [conseq] whose cond literals are all false is satisfied only if its consequent literal is true. (Each active-transition clause is of this shape; when the read-config matches, the consequence is forced.)

theorem Complexity.SAT.Tableau.litTrue {α : Assignment} {v : ℕ} (h : Lit.eval α { sign := true, var := v } = true) : α.get v = true

A satisfied positive literal ⟨true, v⟩ means its variable is true.

theorem Complexity.SAT.Tableau.unit_eval (α : Assignment) (v : ℕ) : Clause.eval α [{ sign := true, var := v }] = α.get v

A positive unit clause [v] is satisfied iff its variable is true.

theorem Complexity.SAT.Tableau.allUnit_eval (α : Assignment) (vs : List ℕ) : CNF.eval α (List.map (fun (v : ℕ) => [{ sign := true, var := v }]) vs) = true ↔ ∀ v ∈ vs, α.get v = true

A list of positive unit clauses is satisfied iff every listed variable is true.

theorem Complexity.SAT.Tableau.cnf_eval_map {β : Type u_1} (α : Assignment) (l : List β) (f : β → Clause) : CNF.eval α (List.map f l) = l.all fun (a : β) => Clause.eval α (f a)

CNF.eval of a map-built clause list: every mapped clause holds.

theorem Complexity.SAT.Tableau.cnf_eval_flatMap {β : Type u_1} (α : Assignment) (l : List β) (f : β → CNF) : CNF.eval α (List.flatMap f l) = l.all fun (a : β) => CNF.eval α (f a)

CNF.eval of a flatMap-built clause list: every sub-CNF holds.

noncomputable def Complexity.SAT.Tableau.stateIdx {k : ℕ} (N : NTM k) (q : N.Q) : ℕ

Index of a machine state as a natural, via the canonical Fintype enumeration of N.Q; injective, so a one-hot encoding over Fin (card Q) names the states.

Equations

• Complexity.SAT.Tableau.stateIdx N q = ↑((Fintype.equivFin N.Q) q)

theorem Complexity.SAT.Tableau.stateIdx_inj {k : ℕ} (N : NTM k) : Function.Injective (stateIdx N)

stateIdx is injective: distinct machine states receive distinct indices.

def Complexity.SAT.Tableau.initCellSym (x : List Bool) (tp pos : ℕ) : Γ

The symbol at position pos of tape tp in the start configuration on input x: cell 0 is always ▷; tape 0 (the input) carries x at cells 1…|x|; every other cell is blank. Mirrors Tape.init applied to each tape.

Equations

• Complexity.SAT.Tableau.initCellSym x tp pos = if pos = 0 then Complexity.Γ.start else if tp = 0 then (List.map Complexity.Γ.ofBool x)[pos - 1]?.getD Complexity.Γ.blank else Complexity.Γ.blank

noncomputable def Complexity.SAT.Tableau.oneHotStates {k : ℕ} (N : NTM k) (steps : ℕ) : List Clause

One-hot constraint that every time-step 0…steps is in exactly one state.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tableau.oneHotCells (k steps P : ℕ) : List Clause

One-hot constraint that every cell (each tape 0…k+1, position 0…P, time 0…steps) holds exactly one of the four symbols.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tableau.oneHotHeads (k steps P : ℕ) : List Clause

One-hot constraint that every tape head (each tape 0…k+1, time 0…steps) is at exactly one position in 0…P.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.startClauses {k : ℕ} (N : NTM k) (steps : ℕ) (x : List Bool) : List Clause

Unit clauses fixing the start configuration at time 0: state qstart, every head at cell 0, and every cell holding its initCellSym value.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.acceptClauses {k : ℕ} (N : NTM k) (steps : ℕ) : List Clause

Unit clauses fixing acceptance at time steps: the state is qhalt and cell 1 of the output tape (index k+1) holds 1.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tableau.frameClauses (k steps P : ℕ) : List Clause

Transition frame. A cell not under its tape's head keeps its symbol from time t to t+1. For each tape/position/symbol, the two clauses encode ¬(head at pos) → (cellₜ = cellₜ₊₁) (a head literal disjoined with each direction of the ↔). The complementary "active" clauses (cell under the head updated per N.δ) are supplied separately.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tableau.posMove (pos : ℕ) (d : Dir3) : ℕ

New head position after a move (mirrors Tape.move): left decrements (clamped at 0 by Nat subtraction), right increments, stay keeps.

Equations

• Complexity.SAT.Tableau.posMove pos Complexity.Dir3.left = pos - 1
• Complexity.SAT.Tableau.posMove pos Complexity.Dir3.right = pos + 1
• Complexity.SAT.Tableau.posMove pos Complexity.Dir3.stay = pos

def Complexity.SAT.Tableau.allSyms : List Γ

The four tape symbols, enumerated.

Equations

• Complexity.SAT.Tableau.allSyms = [Complexity.Γ.zero, Complexity.Γ.one, Complexity.Γ.blank, Complexity.Γ.start]

@[simp]

theorem Complexity.SAT.Tableau.mem_allSyms (s : Γ) : s ∈ allSyms

Every tape symbol appears in allSyms.

theorem Complexity.SAT.Tableau.mem_true_false (b : Bool) : b ∈ [true, false]

Every Boolean appears in the two-element list [true, false].

noncomputable def Complexity.SAT.Tableau.activeCond (N : NTM 1) (t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) : Clause

The shared "read-config" condition literals (all negated) of one transition tuple: state q, the three heads at pi/pw/po reading si/sw/so, and choice b. When α exhibits exactly this read-config every literal is false.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.activeClausesAt (N : NTM 1) (t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) : List Clause

The seven transition clauses for one read-config + choice tuple at time t, encoding N.trace's step: if q = qhalt the configuration stays (the machine has halted), otherwise the next state is out.1 (out := N.δ b q …), the work/output cells under their heads become out's writes, and the three heads move per out (the input cell is read-only).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.activeTransitionClauses (N : NTM 1) (steps P : ℕ) : List Clause

Active transition clauses — activeClausesAt for every time t < steps, state q, the three head positions/read symbols, and choice bit b. Together with the frame clauses these enforce c_{t+1} = step c_t (choice t).

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.Tableau.acceptClauses_sat (N : NTM 1) (steps : ℕ) (α : Assignment) : CNF.eval α (acceptClauses N steps) = true ↔ α.get (vState steps (stateIdx N N.qhalt)) = true ∧ α.get (vCell steps 2 1 (symIdx Γ.one)) = true

The acceptance clauses hold iff the final state is qhalt and output cell 1 holds 1 (the two facts witnessing an accepting halt).

theorem Complexity.SAT.Tableau.startClauses_sat (N : NTM 1) (steps : ℕ) (x : List Bool) (α : Assignment) : CNF.eval α (startClauses N steps x) = true ↔ α.get (vState 0 (stateIdx N N.qstart)) = true ∧ (∀ tp < 3, α.get (vHead 0 tp 0) = true) ∧ ∀ tp < 3, ∀ pos ≤ steps + x.length + 1, α.get (vCell 0 tp pos (symIdx (initCellSym x tp pos))) = true

The start clauses hold iff time-0 is the start configuration: state qstart, every head (tapes 0,1,2) at cell 0, and every cell holding its initCellSym value.

theorem Complexity.SAT.Tableau.frameClauses_sat (k steps P : ℕ) (α : Assignment) : CNF.eval α (frameClauses k steps P) = true ↔ ∀ t < steps, ∀ tp < k + 2, ∀ pos ≤ P, ∀ s < 4, α.get (vHead t tp pos) = false → α.get (vCell t tp pos s) = α.get (vCell (t + 1) tp pos s)

The frame clauses hold iff, whenever a tape head is not at a position, that cell keeps its symbol from time t to t+1.

theorem Complexity.SAT.Tableau.oneHotStates_sat (N : NTM 1) (steps : ℕ) (α : Assignment) : CNF.eval α (oneHotStates N steps) = true ↔ ∀ t ≤ steps, CNF.eval α (exactlyOne (List.map (vState t) (List.range (Fintype.card N.Q)))) = true

The state one-hot clauses hold iff every time-step satisfies its exactly-one state constraint.

theorem Complexity.SAT.Tableau.oneHotCells_sat (k steps P : ℕ) (α : Assignment) : CNF.eval α (oneHotCells k steps P) = true ↔ ∀ t ≤ steps, ∀ tp < k + 2, ∀ pos ≤ P, CNF.eval α (exactlyOne (List.map (vCell t tp pos) (List.range 4))) = true

The cell one-hot clauses hold iff every cell satisfies its exactly-one symbol constraint.

theorem Complexity.SAT.Tableau.oneHotHeads_sat (k steps P : ℕ) (α : Assignment) : CNF.eval α (oneHotHeads k steps P) = true ↔ ∀ t ≤ steps, ∀ tp < k + 2, CNF.eval α (exactlyOne (List.map (vHead t tp) (List.range (P + 1)))) = true

The head one-hot clauses hold iff every tape head satisfies its exactly-one position constraint.

theorem Complexity.SAT.Tableau.activeTransitionClauses_sat (N : NTM 1) (steps P : ℕ) (α : Assignment) : CNF.eval α (activeTransitionClauses N steps P) = true ↔ ∀ t < steps, ∀ (q : N.Q), ∀ pi ≤ P, ∀ (si : Γ), ∀ pw ≤ P, ∀ (sw : Γ), ∀ po ≤ P, ∀ (so : Γ) (b : Bool), CNF.eval α (activeClausesAt N t q pi si pw sw po so b) = true

The active transition clauses hold iff, for every read-config + choice tuple, its activeClausesAt block holds (which says: if α exhibits that read-config at time t, then time t+1 is the N.δ-step).

theorem Complexity.SAT.Tableau.activeCond_false (N : NTM 1) (α : Assignment) (t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) (h1 : α.get (vState t (stateIdx N q)) = true) (h2 : α.get (vHead t 0 pi) = true) (h3 : α.get (vCell t 0 pi (symIdx si)) = true) (h4 : α.get (vHead t 1 pw) = true) (h5 : α.get (vCell t 1 pw (symIdx sw)) = true) (h6 : α.get (vHead t 2 po) = true) (h7 : α.get (vCell t 2 po (symIdx so)) = true) (h8 : α.get (vChoice t) = b) : List.any (activeCond N t q pi si pw sw po so b) (Lit.eval α) = false

When α exhibits the read-config of a transition tuple — state q, the heads at pi/pw/po reading si/sw/so, and choice b — every literal of activeCond is false (so each transition clause forces its consequence).

noncomputable def Complexity.SAT.tableauCNF (N : NTM 1) (steps : ℕ) (x : List Bool) : CNF

Computation-tableau formula. tableauCNF N steps x is the CNF that is satisfiable exactly when the (single-work-tape) machine N has an accepting computation on input x within steps steps — variables encode the tape / head / state contents at each time-step together with the nondeterministic choice bits, and clauses enforce the start configuration, per-step transition validity, and acceptance.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.tableauCNF_eval_split (N : NTM 1) (steps : ℕ) (x : List Bool) (α : Assignment) : CNF.eval α (tableauCNF N steps x) = true ↔ CNF.eval α (Tableau.oneHotStates N steps) = true ∧ CNF.eval α (Tableau.oneHotCells 1 steps (steps + x.length + 1)) = true ∧ CNF.eval α (Tableau.oneHotHeads 1 steps (steps + x.length + 1)) = true ∧ CNF.eval α (Tableau.startClauses N steps x) = true ∧ CNF.eval α (Tableau.frameClauses 1 steps (steps + x.length + 1)) = true ∧ CNF.eval α (Tableau.activeTransitionClauses N steps (steps + x.length + 1)) = true ∧ CNF.eval α (Tableau.acceptClauses N steps) = true

The tableau is satisfied (by α) exactly when all seven clause families are — the bridge from tableauCNF to the per-family characterizations.

def Complexity.SAT.Represents (N : NTM 1) (α : Assignment) (P t : ℕ) (c : Cfg 1 N.Q) : Prop

α represents configuration c at time t (positions bounded by P): the one-hot state/cell/head variables that hold of c are all set true in α. The invariant carried through the backward (sat → accepts) direction.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.traceStep (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : Cfg 1 N.Q

One step of N.trace from configuration c with choice bit b: stays if halted, otherwise applies N.δ. (N.trace (t+1) is this applied to N.trace t.)

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.trace_one_eq (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : N.trace 1 (fun (x : Fin 1) => b) c = traceStep N c b

N.trace 1 is a single traceStep.

theorem Complexity.SAT.trace_succ_eq (N : NTM 1) (g : ℕ → Bool) (t : ℕ) (c : Cfg 1 N.Q) : N.trace (t + 1) (fun (i : Fin (t + 1)) => g ↑i) c = traceStep N (N.trace t (fun (i : Fin t) => g ↑i) c) (g t)

Peel the last step: N.trace (t+1) is one traceStep from N.trace t.

theorem Complexity.SAT.represents_init (N : NTM 1) (α : Assignment) (steps : ℕ) (x : List Bool) (hstart : CNF.eval α (Tableau.startClauses N steps x) = true) : Represents N α (steps + x.length + 1) 0 (N.initCfg x)

Base case: a satisfying assignment for the start clauses represents the initial configuration at time 0.

Tape move/writeAndMove cell/head behaviour, used to match traceStep's fields against the active-transition consequence variables.

theorem Complexity.SAT.tape_move_head (t : Tape) (d : Dir3) : (t.move d).head = Tableau.posMove t.head d

Tape.move changes the head exactly as Tableau.posMove computes.

theorem Complexity.SAT.tape_writeAndMove_head (t : Tape) (s : Γ) (d : Dir3) : (t.writeAndMove s d).head = Tableau.posMove t.head d

Tape.writeAndMove changes the head exactly as Tableau.posMove computes.

theorem Complexity.SAT.tape_writeAndMove_cells_ne (t : Tape) (s : Γ) (d : Dir3) {pos : ℕ} (h : pos ≠ t.head) : (t.writeAndMove s d).cells pos = t.cells pos

Tape.writeAndMove leaves every cell other than the (old) head position unchanged.

theorem Complexity.SAT.tape_writeAndMove_cells_self (t : Tape) (s : Γ) (d : Dir3) : (t.writeAndMove s d).cells t.head = if t.head = 0 then t.cells t.head else s

Tape.writeAndMove sets the (old) head cell to the written symbol, except at cell 0 where writing is a no-op.

theorem Complexity.SAT.represents_conseqs (N : NTM 1) (α : Assignment) (steps P : ℕ) (hactive : CNF.eval α (Tableau.activeTransitionClauses N steps P) = true) (t : ℕ) (ht : t < steps) (c : Cfg 1 N.Q) (hrep : Represents N α P t c) (hhi : c.input.head ≤ P) (hhw : (c.work 0).head ≤ P) (hho : c.output.head ≤ P) : have b := α.get (Tableau.vChoice t); have out := N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read; α.get (Tableau.vState (t + 1) (Tableau.stateIdx N (if c.state = N.qhalt then c.state else out.1))) = true ∧ α.get (Tableau.vCell (t + 1) 0 c.input.head (Tableau.symIdx c.input.read)) = true ∧ α.get (Tableau.vCell (t + 1) 1 (c.work 0).head (Tableau.symIdx (if c.state = N.qhalt then (c.work 0).read else if (c.work 0).head = 0 then (c.work 0).read else (out.2.1 0).toΓ))) = true ∧ α.get (Tableau.vCell (t + 1) 2 c.output.head (Tableau.symIdx (if c.state = N.qhalt then c.output.read else if c.output.head = 0 then c.output.read else out.2.2.1.toΓ))) = true ∧ α.get (Tableau.vHead (t + 1) 0 (if c.state = N.qhalt then c.input.head else Tableau.posMove c.input.head out.2.2.2.1)) = true ∧ α.get (Tableau.vHead (t + 1) 1 (if c.state = N.qhalt then (c.work 0).head else Tableau.posMove (c.work 0).head (out.2.2.2.2.1 0))) = true ∧ α.get (Tableau.vHead (t + 1) 2 (if c.state = N.qhalt then c.output.head else Tableau.posMove c.output.head out.2.2.2.2.2)) = true

The seven consequence variables of the matching active-transition tuple are all true: when α represents c at time t, the read-config matches, so each activeClausesAt clause forces its consequence.

theorem Complexity.SAT.head_off (α : Assignment) (steps P : ℕ) (hheadOne : CNF.eval α (Tableau.oneHotHeads 1 steps P) = true) (t : ℕ) (ht : t ≤ steps) (tp : ℕ) (htp : tp < 3) (ha : ℕ) (hal : ha ≤ P) (hat : α.get (Tableau.vHead t tp ha) = true) (pos : ℕ) (hpos : pos ≤ P) (hne : pos ≠ ha) : α.get (Tableau.vHead t tp pos) = false

Head-uniqueness: if α satisfies the head one-hot clauses and a head sits at ha, then every other position's head variable is false (the frame's hypothesis).

theorem Complexity.SAT.represents_step (N : NTM 1) (α : Assignment) (steps P : ℕ) (hframe : CNF.eval α (Tableau.frameClauses 1 steps P) = true) (hheadOne : CNF.eval α (Tableau.oneHotHeads 1 steps P) = true) (hactive : CNF.eval α (Tableau.activeTransitionClauses N steps P) = true) (t : ℕ) (ht : t < steps) (c : Cfg 1 N.Q) (hrep : Represents N α P t c) (hhi : c.input.head ≤ P) (hhw : (c.work 0).head ≤ P) (hho : c.output.head ≤ P) : Represents N α P (t + 1) (traceStep N c (α.get (Tableau.vChoice t)))

Backward inductive step. If α represents c at time t and satisfies the frame / head-one-hot / active-transition clauses, then it represents the next configuration traceStep N c (choice t) at time t+1.

theorem Complexity.SAT.posMove_le (pos : ℕ) (d : Dir3) : Tableau.posMove pos d ≤ pos + 1

A head move lands at most one cell to the right of where it started.

theorem Complexity.SAT.trace_heads_le (N : NTM 1) (g : ℕ → Bool) (x : List Bool) (t : ℕ) : (N.trace t (fun (i : Fin t) => g ↑i) (N.initCfg x)).input.head ≤ t ∧ ((N.trace t (fun (i : Fin t) => g ↑i) (N.initCfg x)).work 0).head ≤ t ∧ (N.trace t (fun (i : Fin t) => g ↑i) (N.initCfg x)).output.head ≤ t

After t steps each head has moved at most t cells from its start at 0.

theorem Complexity.SAT.represents_trace (N : NTM 1) (α : Assignment) (steps : ℕ) (x : List Bool) (hstart : CNF.eval α (Tableau.startClauses N steps x) = true) (hframe : CNF.eval α (Tableau.frameClauses 1 steps (steps + x.length + 1)) = true) (hheadOne : CNF.eval α (Tableau.oneHotHeads 1 steps (steps + x.length + 1)) = true) (hactive : CNF.eval α (Tableau.activeTransitionClauses N steps (steps + x.length + 1)) = true) (t : ℕ) : t ≤ steps → Represents N α (steps + x.length + 1) t (N.trace t (fun (i : Fin t) => α.get (Tableau.vChoice ↑i)) (N.initCfg x))

Backward trace correspondence. A satisfying assignment represents the whole computation: at every time t ≤ steps it represents N.trace t from the start.

theorem Complexity.SAT.symIdx_lt (s : Γ) : Tableau.symIdx s < 4

Symbol indices are below 4, the number of tape symbols.

theorem Complexity.SAT.stateIdx_lt {k : ℕ} (N : NTM k) (q : N.Q) : Tableau.stateIdx N q < Fintype.card N.Q

State indices are below the number of machine states.

theorem Complexity.SAT.oneHot_unique {α : Assignment} {vars : List ℕ} (hex : CNF.eval α (Tableau.exactlyOne vars) = true) {v w : ℕ} (hv : v ∈ vars) (hw : w ∈ vars) (hvt : α.get v = true) (hwt : α.get w = true) : v = w

The exactly-one clauses force a unique true variable: two true variables in the list must be the same.

theorem Complexity.SAT.tableau_sat_to_accepts (N : NTM 1) (steps : ℕ) (x : List Bool) (h : (tableauCNF N steps x).Satisfiable) : N.AcceptsInTime x steps

Backward direction. If the tableau formula is satisfiable, N accepts x within steps steps: a satisfying assignment's choice bits drive an accepting run.

def Complexity.SAT.assignOf (M : ℕ) (g : ℕ → Bool) : Assignment

Assignment backed by a function g, truncated to [0, M); reads back as g on that range. The forward direction builds its satisfying witness this way.

Equations

• Complexity.SAT.assignOf M g = List.map g (List.range M)

theorem Complexity.SAT.assignOf_get {M : ℕ} (g : ℕ → Bool) {v : ℕ} (h : v < M) : (assignOf M g).get v = g v

assignOf M g reads back as g on variables below M.

theorem Complexity.SAT.le_foldr_max {v : ℕ} {l : List ℕ} (h : v ∈ l) : v ≤ List.foldr max 0 l

Every element of a list is bounded by the list's foldr max 0.

def Complexity.SAT.listAssign (l : List ℕ) : Assignment

Indicator assignment for a finite list of "true" variables: every listed variable reads true, every other variable reads false. The truncation length is one past the list's maximum, so listed variables stay in range while unlisted ones are either out of range or decided false.

Equations

• Complexity.SAT.listAssign l = Complexity.SAT.assignOf (List.foldr max 0 l + 1) fun (i : ℕ) => decide (i ∈ l)

theorem Complexity.SAT.listAssign_get_true {l : List ℕ} {v : ℕ} (h : v ∈ l) : (listAssign l).get v = true

listAssign l reads true on every listed variable.

theorem Complexity.SAT.listAssign_get_false {l : List ℕ} {v : ℕ} (h : v ∉ l) : (listAssign l).get v = false

listAssign l reads false on every unlisted variable.

theorem Complexity.SAT.listAssign_mem_of_get {l : List ℕ} {v : ℕ} (h : (listAssign l).get v = true) : v ∈ l

A variable that listAssign l reads as true must be listed.

def Complexity.SAT.fcfg (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (t : ℕ) : Cfg 1 N.Q

The configuration of N after t steps under the choice function g.

Equations

• Complexity.SAT.fcfg N x g t = N.trace t (fun (i : Fin t) => g ↑i) (N.initCfg x)

def Complexity.SAT.fcellSym (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (t tp pos : ℕ) : Γ

Symbol on tape tp (0=input, 1=work, 2=output) at position pos in fcfg t.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.fheadPos (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (t tp : ℕ) : ℕ

Head position of tape tp in fcfg t.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.ftraceVars (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) : List ℕ

The variables that hold of the run fcfg (over steps steps, positions ≤ P): the one-hot state/cell/head variables and the true choice bits. The forward direction's satisfying assignment marks exactly these true.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.vState_mem_ftraceVars (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t q : ℕ} : Tableau.vState t q ∈ ftraceVars N x g steps P ↔ t ≤ steps ∧ q = Tableau.stateIdx N (fcfg N x g t).state

A state variable is in ftraceVars iff it names the run's state at an in-range time.

theorem Complexity.SAT.vChoice_mem_ftraceVars (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t : ℕ} : Tableau.vChoice t ∈ ftraceVars N x g steps P ↔ t < steps ∧ g t = true

A choice variable is in ftraceVars iff its time is in range and its choice bit is true.

theorem Complexity.SAT.vCell_mem_ftraceVars (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t tp pos s : ℕ} : Tableau.vCell t tp pos s ∈ ftraceVars N x g steps P ↔ t ≤ steps ∧ tp < 3 ∧ pos ≤ P ∧ s = Tableau.symIdx (fcellSym N x g t tp pos)

A cell variable is in ftraceVars iff it names the run's symbol at an in-range cell.

theorem Complexity.SAT.vHead_mem_ftraceVars (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t tp pos : ℕ} : Tableau.vHead t tp pos ∈ ftraceVars N x g steps P ↔ t ≤ steps ∧ tp < 3 ∧ pos = fheadPos N x g t tp

A head variable is in ftraceVars iff it names the run's head position at an in-range time and tape.

noncomputable def Complexity.SAT.fassign (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) : Assignment

The forward direction's satisfying assignment: mark exactly the run's variables.

Equations

• Complexity.SAT.fassign N x g steps P = Complexity.SAT.listAssign (Complexity.SAT.ftraceVars N x g steps P)

theorem Complexity.SAT.fassign_get_vState (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t q : ℕ} : (fassign N x g steps P).get (Tableau.vState t q) = true ↔ t ≤ steps ∧ q = Tableau.stateIdx N (fcfg N x g t).state

fassign sets a state variable true iff it names the run's state (in range).

theorem Complexity.SAT.fassign_get_vChoice (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t : ℕ} : (fassign N x g steps P).get (Tableau.vChoice t) = true ↔ t < steps ∧ g t = true

fassign sets a choice variable true iff its time is in range and its bit is true.

theorem Complexity.SAT.fassign_get_vCell (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t tp pos s : ℕ} : (fassign N x g steps P).get (Tableau.vCell t tp pos s) = true ↔ t ≤ steps ∧ tp < 3 ∧ pos ≤ P ∧ s = Tableau.symIdx (fcellSym N x g t tp pos)

fassign sets a cell variable true iff it names the run's symbol (in range).

theorem Complexity.SAT.fassign_get_vHead (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t tp pos : ℕ} : (fassign N x g steps P).get (Tableau.vHead t tp pos) = true ↔ t ≤ steps ∧ tp < 3 ∧ pos = fheadPos N x g t tp

fassign sets a head variable true iff it names the run's head position (in range).

theorem Complexity.SAT.exactlyOne_of_unique {α : Assignment} {n : ℕ} {f : ℕ → ℕ} {k : ℕ} (hk : k < n) (htrue : α.get (f k) = true) (huniq : ∀ (j : ℕ), α.get (f j) = true → j = k) : CNF.eval α (Tableau.exactlyOne (List.map f (List.range n))) = true

A one-hot constraint over (range n).map f is satisfied when exactly variable f k is true (k < n, and f j true forces j = k).

theorem Complexity.SAT.fheadPos_le (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (t tp : ℕ) : fheadPos N x g t tp ≤ t

After t steps every head position is at most t.

theorem Complexity.SAT.fassign_oneHotStates (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) : CNF.eval (fassign N x g steps P) (Tableau.oneHotStates N steps) = true

fassign satisfies the state one-hot clauses.

theorem Complexity.SAT.fassign_oneHotCells (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) : CNF.eval (fassign N x g steps P) (Tableau.oneHotCells 1 steps P) = true

fassign satisfies the cell one-hot clauses.

theorem Complexity.SAT.fassign_oneHotHeads (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) (hP : steps ≤ P) : CNF.eval (fassign N x g steps P) (Tableau.oneHotHeads 1 steps P) = true

fassign satisfies the head one-hot clauses (positions stay within P ≥ steps).

theorem Complexity.SAT.fheadPos_zero (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (tp : ℕ) : fheadPos N x g 0 tp = 0

At time 0 every head is at cell 0.

theorem Complexity.SAT.fcellSym_zero (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (tp pos : ℕ) : fcellSym N x g 0 tp pos = Tableau.initCellSym x tp pos

At time 0 every cell of the run holds its initCellSym value.

theorem Complexity.SAT.fassign_startClauses (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) (hP : steps + x.length + 1 = P) : CNF.eval (fassign N x g steps P) (Tableau.startClauses N steps x) = true

fassign satisfies the start clauses (with P = steps + |x| + 1).

theorem Complexity.SAT.fcfg_succ (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (t : ℕ) : fcfg N x g (t + 1) = traceStep N (fcfg N x g t) (g t)

Peel the last step: fcfg (t + 1) is one traceStep from fcfg t.

theorem Complexity.SAT.traceStep_input_cells (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) (pos : ℕ) : (traceStep N c b).input.cells pos = c.input.cells pos

traceStep never changes an input-tape cell (the input tape is read-only).

theorem Complexity.SAT.traceStep_work_cells_ne (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) {pos : ℕ} (h : pos ≠ (c.work 0).head) : ((traceStep N c b).work 0).cells pos = (c.work 0).cells pos

traceStep leaves every work-tape cell other than the work head's unchanged.

theorem Complexity.SAT.traceStep_output_cells_ne (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) {pos : ℕ} (h : pos ≠ c.output.head) : (traceStep N c b).output.cells pos = c.output.cells pos

traceStep leaves every output-tape cell other than the output head's unchanged.

theorem Complexity.SAT.traceStep_state (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : (traceStep N c b).state = if c.state = N.qhalt then c.state else (N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read).1

The state after traceStep: unchanged when halted, otherwise N.δ's next state.

theorem Complexity.SAT.traceStep_input_head (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : (traceStep N c b).input.head = if c.state = N.qhalt then c.input.head else Tableau.posMove c.input.head (N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read).2.2.2.1

The input head after traceStep: unchanged when halted, otherwise moved per N.δ (posMove).

theorem Complexity.SAT.traceStep_work_head (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : ((traceStep N c b).work 0).head = if c.state = N.qhalt then (c.work 0).head else Tableau.posMove (c.work 0).head ((N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read).2.2.2.2.1 0)

The work head after traceStep: unchanged when halted, otherwise moved per N.δ (posMove).

theorem Complexity.SAT.traceStep_output_head (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : (traceStep N c b).output.head = if c.state = N.qhalt then c.output.head else Tableau.posMove c.output.head (N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read).2.2.2.2.2

The output head after traceStep: unchanged when halted, otherwise moved per N.δ (posMove).

theorem Complexity.SAT.traceStep_work_cells_self (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : ((traceStep N c b).work 0).cells (c.work 0).head = if c.state = N.qhalt then (c.work 0).read else if (c.work 0).head = 0 then (c.work 0).read else ((N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read).2.1 0).toΓ

The work cell under the head after traceStep: unchanged when halted or at cell 0 (writes there are no-ops), otherwise the symbol N.δ writes.

theorem Complexity.SAT.traceStep_output_cells_self (N : NTM 1) (c : Cfg 1 N.Q) (b : Bool) : (traceStep N c b).output.cells c.output.head = if c.state = N.qhalt then c.output.read else if c.output.head = 0 then c.output.read else (N.δ b c.state c.input.read (fun (x : Fin 1) => (c.work 0).read) c.output.read).2.2.1.toΓ

The output cell under the head after traceStep: unchanged when halted or at cell 0 (writes there are no-ops), otherwise the symbol N.δ writes.

theorem Complexity.SAT.fcellSym_succ_ne (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (t tp pos : ℕ) (h : pos ≠ fheadPos N x g t tp) : fcellSym N x g (t + 1) tp pos = fcellSym N x g t tp pos

In the run, a cell not under its tape's head keeps its symbol from time t to t+1.

theorem Complexity.SAT.fassign_acceptClauses (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) (hP : 1 ≤ P) (hhalt : (fcfg N x g steps).state = N.qhalt) (hout : (fcfg N x g steps).output.cells 1 = Γ.one) : CNF.eval (fassign N x g steps P) (Tableau.acceptClauses N steps) = true

fassign satisfies the acceptance clauses when the run halts at time steps with output cell 1 holding 1.

theorem Complexity.SAT.fassign_get_vCell_eq (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t tp pos s : ℕ} (ht : t ≤ steps) (htp : tp < 3) (hpos : pos ≤ P) : (fassign N x g steps P).get (Tableau.vCell t tp pos s) = decide (s = Tableau.symIdx (fcellSym N x g t tp pos))

On in-range cell variables, fassign reads true exactly when the symbol index is the run's symbol at that cell.

theorem Complexity.SAT.fassign_frameClauses (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) : CNF.eval (fassign N x g steps P) (Tableau.frameClauses 1 steps P) = true

fassign satisfies the frame clauses: in the run, off-head cells keep their symbols.

theorem Complexity.SAT.fassign_get_vChoice_eq (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) {t : ℕ} (ht : t < steps) : (fassign N x g steps P).get (Tableau.vChoice t) = g t

On in-range choice variables, fassign reads back the choice function g.

theorem Complexity.SAT.fassign_activeClausesAt (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P t : ℕ) (ht : t < steps) (q : N.Q) (pi : ℕ) (hpi : pi ≤ P) (si : Γ) (pw : ℕ) (hpw : pw ≤ P) (sw : Γ) (po : ℕ) (hpo : po ≤ P) (so : Γ) (b : Bool) : CNF.eval (fassign N x g steps P) (Tableau.activeClausesAt N t q pi si pw sw po so b) = true

fassign satisfies each activeClausesAt block: either the read-config does not match the run (some condition literal is true), or it does and the consequence variables hold because the run takes exactly that traceStep.

theorem Complexity.SAT.fassign_activeTransitionClauses (N : NTM 1) (x : List Bool) (g : ℕ → Bool) (steps P : ℕ) : CNF.eval (fassign N x g steps P) (Tableau.activeTransitionClauses N steps P) = true

fassign satisfies the active transition clauses.

theorem Complexity.SAT.accepts_to_tableau_sat (N : NTM 1) (steps : ℕ) (x : List Bool) (h : N.AcceptsInTime x steps) : (tableauCNF N steps x).Satisfiable

Forward direction. If N accepts x within steps steps, the tableau is satisfiable: the assignment marking exactly the accepting run's variables.

theorem Complexity.SAT.tableauCNF_satisfiable_iff (N : NTM 1) (steps : ℕ) (x : List Bool) : (tableauCNF N steps x).Satisfiable ↔ N.AcceptsInTime x steps

Tableau correctness (core). The tableau formula is satisfiable iff N accepts x within steps steps.

theorem Complexity.SAT.encode_mem_LSAT_iff (φ : CNF) : φ.encode ∈ language ↔ φ.Satisfiable

An encoded CNF is in language iff it is satisfiable (CNF.encode is injective, via CNF.decode?_encode).

Flat variable re-indexing

The enc-based variable indices are Nat.pair towers — convenient for the injectivity bookkeeping of the correctness proof, but a Turing machine computing them would need comparison-and-branch arithmetic. The flat mixed-radix scheme below needs only multiplication and addition (unary machine-trivial), and transports satisfiability along the injective re-encoding flatToEnc (SAT.CNF.satisfiable_mapVar_iff). The reduction emits the flat formula.

def Complexity.SAT.Tableau.flatVar (A B C D tag a b c d : ℕ) : ℕ

Mixed-radix flat variable index: tag at the top, then components (a, b, c, d) with radices (A, B, C, D).

Equations

• Complexity.SAT.Tableau.flatVar A B C D tag a b c d = (((tag * A + a) * B + b) * C + c) * D + d

theorem Complexity.SAT.Tableau.flatVar_decode {A B C D tag a b c d : ℕ} (ha : a < A) (hb : b < B) (hc : c < C) (hd : d < D) : flatVar A B C D tag a b c d % D = d ∧ flatVar A B C D tag a b c d / D % C = c ∧ flatVar A B C D tag a b c d / D / C % B = b ∧ flatVar A B C D tag a b c d / D / C / B % A = a ∧ flatVar A B C D tag a b c d / D / C / B / A = tag

The flat components decode by iterated division and remainder.

theorem Complexity.SAT.Tableau.flatVar_recompose (A B C D v : ℕ) : flatVar A B C D (v / D / C / B / A) (v / D / C / B % A) (v / D / C % B) (v / D % C) (v % D) = v

Mixed-radix re-composition is the identity (unconditionally — the div/mod identity at each layer).

def Complexity.SAT.Tableau.flatToEnc (A B C D v : ℕ) : ℕ

The injective re-encoding from flat indices to the Nat.pair-based enc indices: decode the mixed-radix components, re-encode per tag (tag 2 — the cell variables — pairs its position and symbol, matching vCell).

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.Tableau.flatToEnc_injective (A B C D : ℕ) : Function.Injective (flatToEnc A B C D)

flatToEnc is injective: the mixed-radix components recompose the flat index.

def Complexity.SAT.Tableau.vStateF (Qc steps P t q : ℕ) : ℕ

Flat tableau variables: same roles as vState/vChoice/vCell/vHead, mixed-radix indices.

Equations

• Complexity.SAT.Tableau.vStateF Qc steps P t q = Complexity.SAT.Tableau.flatVar (steps + 1) (max Qc 3) (P + 2) 4 0 t q 0 0

def Complexity.SAT.Tableau.vChoiceF (Qc steps P t : ℕ) : ℕ

Flat tableau variables: same roles as vState/vChoice/vCell/vHead, mixed-radix indices.

Equations

• Complexity.SAT.Tableau.vChoiceF Qc steps P t = Complexity.SAT.Tableau.flatVar (steps + 1) (max Qc 3) (P + 2) 4 1 t 0 0 0

def Complexity.SAT.Tableau.vCellF (Qc steps P t tp pos s : ℕ) : ℕ

Flat tableau variables: same roles as vState/vChoice/vCell/vHead, mixed-radix indices.

Equations

• Complexity.SAT.Tableau.vCellF Qc steps P t tp pos s = Complexity.SAT.Tableau.flatVar (steps + 1) (max Qc 3) (P + 2) 4 2 t tp pos s

def Complexity.SAT.Tableau.vHeadF (Qc steps P t tp pos : ℕ) : ℕ

Flat tableau variables: same roles as vState/vChoice/vCell/vHead, mixed-radix indices.

Equations

• Complexity.SAT.Tableau.vHeadF Qc steps P t tp pos = Complexity.SAT.Tableau.flatVar (steps + 1) (max Qc 3) (P + 2) 4 3 t tp pos 0

theorem Complexity.SAT.Tableau.flatToEnc_vStateF (Qc steps P : ℕ) {t q : ℕ} (ht : t ≤ steps) (hq : q < Qc) : flatToEnc (steps + 1) (max Qc 3) (P + 2) 4 (vStateF Qc steps P t q) = vState t q

flatToEnc carries each in-range flat variable to its enc counterpart.

theorem Complexity.SAT.Tableau.flatToEnc_vChoiceF (Qc steps P : ℕ) {t : ℕ} (ht : t ≤ steps) : flatToEnc (steps + 1) (max Qc 3) (P + 2) 4 (vChoiceF Qc steps P t) = vChoice t

flatToEnc carries each in-range flat variable to its enc counterpart.

theorem Complexity.SAT.Tableau.flatToEnc_vCellF (Qc steps P : ℕ) {t tp pos s : ℕ} (ht : t ≤ steps) (htp : tp < 3) (hpos : pos < P + 2) (hs : s < 4) : flatToEnc (steps + 1) (max Qc 3) (P + 2) 4 (vCellF Qc steps P t tp pos s) = vCell t tp pos s

flatToEnc carries each in-range flat variable to its enc counterpart.

theorem Complexity.SAT.Tableau.flatToEnc_vHeadF (Qc steps P : ℕ) {t tp pos : ℕ} (ht : t ≤ steps) (htp : tp < 3) (hpos : pos < P + 2) : flatToEnc (steps + 1) (max Qc 3) (P + 2) 4 (vHeadF Qc steps P t tp pos) = vHead t tp pos

flatToEnc carries each in-range flat variable to its enc counterpart.

theorem Complexity.SAT.Tableau.mapVar_flatMap {α : Type u_1} (f : ℕ → ℕ) (l : List α) (g : α → CNF) : CNF.mapVar f (List.flatMap g l) = List.flatMap (fun (a : α) => CNF.mapVar f (g a)) l

CNF.mapVar distributes over flatMap.

theorem Complexity.SAT.Tableau.mapVar_atLeastOne (f : ℕ → ℕ) (vars : List ℕ) : Clause.mapVar f (atLeastOne vars) = atLeastOne (List.map f vars)

Variable renaming commutes with atLeastOne.

theorem Complexity.SAT.Tableau.mapVar_atMostOne (f : ℕ → ℕ) (vars : List ℕ) : CNF.mapVar f (atMostOne vars) = atMostOne (List.map f vars)

Variable renaming commutes with atMostOne.

theorem Complexity.SAT.Tableau.mapVar_exactlyOne (f : ℕ → ℕ) (vars : List ℕ) : CNF.mapVar f (exactlyOne vars) = exactlyOne (List.map f vars)

Variable renaming commutes with exactlyOne.

theorem Complexity.SAT.Tableau.posMove_le_succ (pos : ℕ) (d : Dir3) : posMove pos d ≤ pos + 1

A head move lands within one cell of where it started.

noncomputable def Complexity.SAT.Tableau.oneHotStatesF (N : NTM 1) (steps P : ℕ) : List Clause

Flat-variable mirror of oneHotStates.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tableau.oneHotCellsF (Qc steps P : ℕ) : List Clause

Flat-variable mirror of oneHotCells (at k = 1).

Equations

• One or more equations did not get rendered due to their size.

def Complexity.SAT.Tableau.oneHotHeadsF (Qc steps P : ℕ) : List Clause

Flat-variable mirror of oneHotHeads (at k = 1).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.startClausesF (N : NTM 1) (steps : ℕ) (x : List Bool) : List Clause

Flat-variable mirror of startClauses (at k = 1).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.acceptClausesF (N : NTM 1) (steps P : ℕ) : List Clause

Flat-variable mirror of acceptClauses (at k = 1).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.encOf (N : NTM 1) (steps P : ℕ) : ℕ → ℕ

The re-encoding at this tableau's moduli.

Equations

• Complexity.SAT.Tableau.encOf N steps P = Complexity.SAT.Tableau.flatToEnc (steps + 1) (max (Fintype.card N.Q) 3) (P + 2) 4

theorem Complexity.SAT.Tableau.encOf_injective (N : NTM 1) (steps P : ℕ) : Function.Injective (encOf N steps P)

encOf is injective (it is flatToEnc at fixed moduli).

theorem Complexity.SAT.Tableau.mapVar_oneHotStatesF (N : NTM 1) (steps P : ℕ) : CNF.mapVar (encOf N steps P) (oneHotStatesF N steps P) = oneHotStates N steps

Re-indexing by encOf carries oneHotStatesF to oneHotStates.

theorem Complexity.SAT.Tableau.mapVar_oneHotCellsF (N : NTM 1) (steps P : ℕ) : CNF.mapVar (encOf N steps P) (oneHotCellsF (Fintype.card N.Q) steps P) = oneHotCells 1 steps P

Re-indexing by encOf carries oneHotCellsF to oneHotCells.

theorem Complexity.SAT.Tableau.mapVar_oneHotHeadsF (N : NTM 1) (steps P : ℕ) : CNF.mapVar (encOf N steps P) (oneHotHeadsF (Fintype.card N.Q) steps P) = oneHotHeads 1 steps P

Re-indexing by encOf carries oneHotHeadsF to oneHotHeads.

theorem Complexity.SAT.Tableau.mapVar_acceptClausesF (N : NTM 1) (steps P : ℕ) : CNF.mapVar (encOf N steps P) (acceptClausesF N steps P) = acceptClauses N steps

Re-indexing by encOf carries acceptClausesF to acceptClauses.

def Complexity.SAT.Tableau.frameClausesF (Qc steps P : ℕ) : List Clause

Flat-variable mirror of frameClauses (at k = 1).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.activeCondF (N : NTM 1) (steps P t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) : Clause

Flat-variable mirror of activeCond.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.activeClausesAtF (N : NTM 1) (steps P t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) : List Clause

Flat-variable mirror of activeClausesAt.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.SAT.Tableau.activeTransitionClausesF (N : NTM 1) (steps P : ℕ) : List Clause

Flat-variable mirror of activeTransitionClauses.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.Tableau.mapVar_startClausesF (N : NTM 1) (steps : ℕ) (x : List Bool) : CNF.mapVar (encOf N steps (steps + x.length + 1)) (startClausesF N steps x) = startClauses N steps x

Re-indexing by encOf carries startClausesF to startClauses.

theorem Complexity.SAT.Tableau.mapVar_frameClausesF (N : NTM 1) (steps P : ℕ) : CNF.mapVar (encOf N steps P) (frameClausesF (Fintype.card N.Q) steps P) = frameClauses 1 steps P

Re-indexing by encOf carries frameClausesF to frameClauses.

theorem Complexity.SAT.Tableau.mapVar_activeCondF (N : NTM 1) (steps P t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) (ht : t < steps) (hpi : pi ≤ P) (hpw : pw ≤ P) (hpo : po ≤ P) : Clause.mapVar (encOf N steps P) (activeCondF N steps P t q pi si pw sw po so b) = activeCond N t q pi si pw sw po so b

Re-indexing by encOf carries activeCondF to activeCond (for in-range tuples).

theorem Complexity.SAT.Tableau.mapVar_activeClausesAtF (N : NTM 1) (steps P t : ℕ) (q : N.Q) (pi : ℕ) (si : Γ) (pw : ℕ) (sw : Γ) (po : ℕ) (so : Γ) (b : Bool) (ht : t < steps) (hpi : pi ≤ P) (hpw : pw ≤ P) (hpo : po ≤ P) : CNF.mapVar (encOf N steps P) (activeClausesAtF N steps P t q pi si pw sw po so b) = activeClausesAt N t q pi si pw sw po so b

Re-indexing by encOf carries activeClausesAtF to activeClausesAt (for in-range tuples).

theorem Complexity.SAT.Tableau.mapVar_activeTransitionClausesF (N : NTM 1) (steps P : ℕ) : CNF.mapVar (encOf N steps P) (activeTransitionClausesF N steps P) = activeTransitionClauses N steps P

Re-indexing by encOf carries activeTransitionClausesF to activeTransitionClauses.

noncomputable def Complexity.SAT.tableauCNFFlat (N : NTM 1) (steps : ℕ) (x : List Bool) : CNF

The flat computation-tableau formula: tableauCNF with mixed-radix variable indices in place of the Nat.pair-based ones. Satisfiability is identical (tableauCNFFlat_satisfiable_iff); this is the formula the reduction machine emits, since its indices need only multiplication and addition.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.SAT.tableauCNFFlat_mapVar (N : NTM 1) (steps : ℕ) (x : List Bool) : CNF.mapVar (Tableau.encOf N steps (steps + x.length + 1)) (tableauCNFFlat N steps x) = tableauCNF N steps x

The flat tableau is the enc tableau, re-indexed.

theorem Complexity.SAT.tableauCNFFlat_satisfiable_iff (N : NTM 1) (steps : ℕ) (x : List Bool) : (tableauCNFFlat N steps x).Satisfiable ↔ N.AcceptsInTime x steps

Flat-tableau correctness: satisfiability transports along the injective re-indexing to the proved tableauCNF_satisfiable_iff.

noncomputable def Complexity.SAT.reductionFn (N : NTM 1) (T : ℕ → ℕ) : List Bool → List Bool

The Cook–Levin reduction function: map each input to the encoding of its (flat-variable) computation-tableau formula.

Equations

• Complexity.SAT.reductionFn N T x = (Complexity.SAT.tableauCNFFlat N (T x.length) x).encode

theorem Complexity.SAT.tableauCNF_correct {L : Language} (N : NTM 1) (T : ℕ → ℕ) (hdec : N.DecidesInTime L T) (x : List Bool) : x ∈ L ↔ reductionFn N T x ∈ language

The reduction is correct. x ∈ L iff the reduction output is in language, combining the tableau characterization with N deciding L.

The reduction machine, its polynomial running time, and the headline theorems reductionFn_mem_FP, cookLevin_reduction, NPHard_language, and NPComplete_language live in Complexitylib.SAT.CookLevin.Assembly, built on the emitter development under Complexitylib.SAT.CookLevin/.