Soundness of the Cook–Levin tableau

A satisfying assignment of the tableau formula comes from an accepting run (acceptsIn_of_tableau_sat), and the equivalence tableau_sat_iff (planning/succinct-cook-levin.md, S1).

• The successor part of a locally consistent window is a function of its time-t part (post_of_pre): two locally consistent local configurations with the same cells, heads and state at time t, one of them with at most one head per tape, agree on the cell and head at time t + 1 of every tape whose head is far, and on everything when every head is in the window.
• The free input strings are read off the time-0 rows (freeString): the symbols from cell 3 up to the first blank, which the free-tape clauses make well defined (FreeFacts.cell_eq).
• The rows encode the run (rows_of_sat), by induction on time: the window centered at a cell, with the other windows centered at the heads, determines the cell and head at the next time; the window centered at every head determines the state and the emission bits.

The successor part of a window is determined

theorem MIPRE.TM.CookLevin.LocalCfg.HeadAt.unique {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {L : LocalCfg i w Symbol State} {d : Tape i w} {δ δ' : Fin 5} (h : L.HeadAt d δ) (h' : L.HeadAt d δ') : δ = δ'

theorem MIPRE.TM.CookLevin.fullStep_post_eq {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {L L' : LocalCfg i w Symbol State} (δ : Tape i w → Fin 5) (hL : FullStep M acc L δ) (hL' : FullStep M acc L' δ) (hc : L.cellPre = L'.cellPre) (hh : L.headPre = L'.headPre) (hs : L.statePre = L'.statePre) : L.cellPost = L'.cellPost ∧ L.headPost = L'.headPost ∧ L.statePost = L'.statePost ∧ L.emitOne = L'.emitOne ∧ L.emitBad = L'.emitBad

Two windows satisfying the full-step check at the same offsets, with the same time-t part, have the same time-t + 1 part.

theorem MIPRE.TM.CookLevin.post_of_pre {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {L L' : LocalCfg i w Symbol State} (hL : LocallyConsistent M acc L) (hL' : LocallyConsistent M acc L') (hno : ∀ (d : Tape i w), ¬L'.TwoHeads d) (hc : L.cellPre = L'.cellPre) (hh : L.headPre = L'.headPre) (hs : L.statePre = L'.statePre) : (∀ (d : Tape i w), L'.HeadFar d → L.cellPost d = L'.cellPost d ∧ L.headPost d = L'.headPost d) ∧ ((∀ (d : Tape i w), ∃ (δ : Fin 5), 1 ≤ ↑δ ∧ ↑δ ≤ 3 ∧ L'.HeadAt d δ) → L.cellPost = L'.cellPost ∧ L.headPost = L'.headPost ∧ L.statePost = L'.statePost ∧ L.emitOne = L'.emitOne ∧ L.emitBad = L'.emitBad)

The successor part of a locally consistent window is determined by its time-t part. For every tape whose head is far the cell and head at time t + 1, and when every head is in the window everything.

The free input strings

def MIPRE.TM.CookLevin.blankBit {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) (k : ℕ) : Bool

The blank bit of cell k + 3 of input tape j at time 0 (true past the last cell).

Equations

• MIPRE.TM.CookLevin.blankBit a j k = if h : k + 3 < MIPRE.TM.CookLevin.numCells S then a (MIPRE.TM.CookLevin.TabVar.cell 0 (Sum.inl j) ⟨k + 3, h⟩ MIPRE.TM.CookLevin.CellVal.blank) else true

def MIPRE.TM.CookLevin.symBit {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) (s : Symbol) (k : ℕ) : Bool

The s bit of cell k + 3 of input tape j at time 0.

Equations

• MIPRE.TM.CookLevin.symBit a j s k = if h : k + 3 < MIPRE.TM.CookLevin.numCells S then a (MIPRE.TM.CookLevin.TabVar.cell 0 (Sum.inl j) ⟨k + 3, h⟩ (MIPRE.TM.CookLevin.CellVal.sym s)) else false

theorem MIPRE.TM.CookLevin.freeLen_exists {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) : ∃ (k : ℕ), blankBit a j k = true ∨ numCells S ≤ k + 5

noncomputable def MIPRE.TM.CookLevin.freeLen {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) : ℕ

The length of the string on a free tape: the first cell, from cell 3, that is blank or a boundary cell.

Equations

• MIPRE.TM.CookLevin.freeLen a j = Nat.find ⋯

theorem MIPRE.TM.CookLevin.freeLen_spec {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) : blankBit a j (freeLen a j) = true ∨ numCells S ≤ freeLen a j + 5

theorem MIPRE.TM.CookLevin.freeLen_min {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) {k : ℕ} (hk : k < freeLen a j) : ¬(blankBit a j k = true ∨ numCells S ≤ k + 5)

noncomputable def MIPRE.TM.CookLevin.freeString {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) (s₀ s₁ : Symbol) : List Symbol

The string on free tape j, read off row 0: s₀ where the s₀ bit is set, else s₁, up to the first blank.

Equations

• MIPRE.TM.CookLevin.freeString a j s₀ s₁ = List.ofFn fun (k : Fin (MIPRE.TM.CookLevin.freeLen a j)) => if MIPRE.TM.CookLevin.symBit a j s₀ ↑k = true then s₀ else s₁

theorem MIPRE.TM.CookLevin.freeString_mem {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) (s₀ s₁ s : Symbol) : s ∈ freeString a j s₀ s₁ → s = s₀ ∨ s = s₁

theorem MIPRE.TM.CookLevin.length_freeString {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S G : ℕ} (a : TabVar i w Symbol State S G → Bool) (j : Fin i) (s₀ s₁ : Symbol) : (freeString a j s₀ s₁).length = freeLen a j

structure MIPRE.TM.CookLevin.FreeFacts {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S G : ℕ} (s₀ s₁ : Symbol) (a : TabVar i w Symbol State S G → Bool) (j : Fin i) : Prop

What the free-tape clauses say about tape j at time 0.

• bdry (p : Pos S) (v : CellVal Symbol) : p.IsBdry → a (TabVar.cell 0 (Sum.inl j) p v) = decide (v = CellVal.bdry)
• other (p : Pos S) (v : CellVal Symbol) : ¬p.IsBdry → v ≠ CellVal.sym s₀ → v ≠ CellVal.sym s₁ → v ≠ CellVal.blank → a (TabVar.cell 0 (Sum.inl j) p v) = false
• two (v : CellVal Symbol) : a (TabVar.cell 0 (Sum.inl j) ⟨2, ⋯⟩ v) = decide (v = CellVal.blank)
• some (p : Pos S) : ¬p.IsBdry → a (TabVar.cell 0 (Sum.inl j) p (CellVal.sym s₀)) = true ∨ a (TabVar.cell 0 (Sum.inl j) p (CellVal.sym s₁)) = true ∨ a (TabVar.cell 0 (Sum.inl j) p CellVal.blank) = true
• once (p : Pos S) (v v' : CellVal Symbol) : ¬p.IsBdry → v ≠ v' → ¬(a (TabVar.cell 0 (Sum.inl j) p v) = true ∧ a (TabVar.cell 0 (Sum.inl j) p v') = true)
• mono (p p' : Pos S) : 2 < ↑p → ¬p'.IsBdry → p < p' → a (TabVar.cell 0 (Sum.inl j) p CellVal.blank) = true → a (TabVar.cell 0 (Sum.inl j) p' CellVal.blank) = true

theorem MIPRE.TM.CookLevin.freeFacts {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S G : ℕ} {s₀ s₁ : Symbol} (fixed : Fin i → Option (List Symbol)) (a : TabVar i w Symbol State S G → Bool) (hSat : (freeClauses S G s₀ s₁ fixed).Sat a) (j : Fin i) (hj : fixed j = none) : FreeFacts s₀ s₁ a j

theorem MIPRE.TM.CookLevin.FreeFacts.onehot {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S G : ℕ} {s₀ s₁ : Symbol} {a : TabVar i w Symbol State S G → Bool} {j : Fin i} (F : FreeFacts s₀ s₁ a j) (p : Pos S) (hnb : ¬p.IsBdry) (u : CellVal Symbol) (hu : a (TabVar.cell 0 (Sum.inl j) p u) = true) (v : CellVal Symbol) : a (TabVar.cell 0 (Sum.inl j) p v) = decide (v = u)

An interior cell carrying one value carries no other.

theorem MIPRE.TM.CookLevin.FreeFacts.cell_eq {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S G : ℕ} {s₀ s₁ : Symbol} {a : TabVar i w Symbol State S G → Bool} {j : Fin i} (F : FreeFacts s₀ s₁ a j) (p : Pos S) (v : CellVal Symbol) : a (TabVar.cell 0 (Sum.inl j) p v) = decide (v = inputCellVal (freeString a j s₀ s₁) p)

The time-0 row of a free tape is the encoding of the string read off it.

The rows encode the run

structure MIPRE.TM.CookLevin.RowOk {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] {S G : ℕ} {input : Fin i → List Symbol} (a : TabVar i w Symbol State S G → Bool) (t : Fin (S + 1)) (c : Turing.MultiInputTM.Cfg i w Symbol State input) : Prop

Row t of the assignment a encodes the configuration c.

• cell (d : Tape i w) (p : Pos S) (v : CellVal Symbol) : a (TabVar.cell t d p v) = decide (cellValAt c d p = v)
• head (d : Tape i w) (p : Pos S) : a (TabVar.head t d p) = decide (headCell c d = ↑↑p)
• state (q : Option State) : a (TabVar.state t q) = decide (c.state = q)

theorem MIPRE.TM.CookLevin.window_of_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] {S G : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (a : TabVar i w Symbol State S G → Bool) (t : Fin S) (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hrow : RowOk a t.castSucc c) (js : Tape i w → Center S) (hwin : checkPred M acc fun (v : WinVar i w Symbol State) => a (winVarOf t js v)) : ∃ (L : LocalCfg i w Symbol State), LocallyConsistent M acc L ∧ (∀ (v : WinVar i w Symbol State), L.encode v = a (winVarOf t js v)) ∧ L.cellPre = (localCfgOf M acc c js).cellPre ∧ L.headPre = (localCfgOf M acc c js).headPre ∧ L.statePre = (localCfgOf M acc c js).statePre

A locally consistent window of a at step t whose time-t part is that of c.

Windows centered at the heads and at a cell

theorem MIPRE.TM.CookLevin.headCell_sub_two_toNat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (d : Tape i w) : ↑(headCell c d - 2).toNat = headCell c d - 2

def MIPRE.TM.CookLevin.headCenter {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (d : Tape i w) : Center S

The center putting the head of d at offset 2.

Equations

• MIPRE.TM.CookLevin.headCenter c hin d = ⟨(MIPRE.TM.CookLevin.headCell c d - 2).toNat, ⋯⟩

theorem MIPRE.TM.CookLevin.headAt_headCenter {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (js : Tape i w → Center S) (d : Tape i w) (hd : js d = headCenter c hin d) : (localCfgOf M acc c js).HeadAt d 2

def MIPRE.TM.CookLevin.cellCenter {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (d : Tape i w) (p : Pos S) (hnb : ¬p.IsBdry) : Tape i w → Center S

The centers putting the cell p of tape d at the middle of its window and the head of every other tape at offset 2.

Equations

• MIPRE.TM.CookLevin.cellCenter c hin d p hnb d' = if d' = d then ⟨↑p - 2, ⋯⟩ else MIPRE.TM.CookLevin.headCenter c hin d'

theorem MIPRE.TM.CookLevin.center_cellCenter {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (d : Tape i w) (p : Pos S) (hnb : ¬p.IsBdry) : center (cellCenter c hin d p hnb d) = p

theorem MIPRE.TM.CookLevin.allIn_headCenter {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (d : Tape i w) : ∃ (δ : Fin 5), 1 ≤ ↑δ ∧ ↑δ ≤ 3 ∧ (localCfgOf M acc c (headCenter c hin)).HeadAt d δ

Every head is in its window when the windows are centered at the heads.

theorem MIPRE.TM.CookLevin.cellCenter_cases {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hin : HeadsIn c S) (d : Tape i w) (p : Pos S) (hnb : ¬p.IsBdry) : (∀ (d' : Tape i w), ∃ (δ : Fin 5), 1 ≤ ↑δ ∧ ↑δ ≤ 3 ∧ (localCfgOf M acc c (cellCenter c hin d p hnb)).HeadAt d' δ) ∨ (localCfgOf M acc c (cellCenter c hin d p hnb)).HeadFar d

At the window of a cell, either every head is in its window or the head of the cell's tape is far.

The step

theorem MIPRE.TM.CookLevin.rowOk_step {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [DecidableEq Symbol] [DecidableEq State] {S G : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc : Symbol) {input : Fin i → List Symbol} (a : TabVar i w Symbol State S G → Bool) (t : Fin S) (c : Turing.MultiInputTM.Cfg i w Symbol State input) (hrow : RowOk a t.castSucc c) (hin : HeadsIn c S) (hin' : HeadsIn (Turing.MultiInputTM.step c) S) (hwin : ∀ (js : Tape i w → Center S), checkPred M acc fun (v : WinVar i w Symbol State) => a (winVarOf t js v)) (hbdry : ∀ (d : Tape i w) (p : Pos S) (v : CellVal Symbol), p.IsBdry → a (TabVar.cell t.succ d p v) = decide (v = CellVal.bdry)) (hbdryh : ∀ (d : Tape i w) (p : Pos S), p.IsBdry → a (TabVar.head t.succ d p) = false) : RowOk a t.succ (Turing.MultiInputTM.step c) ∧ a (TabVar.emitOne t) = decide (Turing.MultiInputTM.outputSymbol c = some acc) ∧ a (TabVar.emitBad t) = decide (Turing.MultiInputTM.outputSymbol c ≠ none ∧ Turing.MultiInputTM.outputSymbol c ≠ some acc)

A row encoding c is followed by a row encoding M.step c, when every window is locally consistent; the emission bits of the step are those of c.

theorem MIPRE.TM.CookLevin.eq_singleton_of_length_le_one {α : Type u_1} {l : List α} {x : α} (hne : l ≠ []) (hlen : l.length ≤ 1) (hall : ∀ s ∈ l, s = x) : l = [x]

From a satisfying assignment to an accepting run

noncomputable def MIPRE.TM.CookLevin.inputOf {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) : Fin i → List Symbol

The inputs read off a satisfying assignment: the fixed strings, and on the free tapes the strings on the time-0 rows.

Equations

• MIPRE.TM.CookLevin.inputOf s₀ s₁ fixed chk a j = (fixed j).getD (MIPRE.TM.CookLevin.freeString a j s₀ s₁)

theorem MIPRE.TM.CookLevin.inputOf_fixed {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (j : Fin i) (x : List Symbol) (hx : fixed j = some x) : inputOf s₀ s₁ fixed chk a j = x

theorem MIPRE.TM.CookLevin.inputOf_free {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (j : Fin i) (hx : fixed j = none) : inputOf s₀ s₁ fixed chk a j = freeString a j s₀ s₁

theorem MIPRE.TM.CookLevin.headCell_initCfg_iff {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (input : Fin i → List Symbol) (d : Tape i w) (p : Pos S) : headCell (Turing.MultiInputTM.initCfg input) d = ↑↑p ↔ p = startCell S d

theorem MIPRE.TM.CookLevin.cellValAt_initCfg_inr {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (input : Fin i → List Symbol) (j : Fin w) (p : Pos S) : cellValAt (Turing.MultiInputTM.initCfg input) (Sum.inr j) p = workCellVal₀ p

theorem MIPRE.TM.CookLevin.sat_start {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) : (startClauses S chk.gates.length M fixed).Sat a

theorem MIPRE.TM.CookLevin.sat_free {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) : (freeClauses S chk.gates.length s₀ s₁ fixed).Sat a

theorem MIPRE.TM.CookLevin.sat_bdry_cell {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin (S + 1)) (d : Tape i w) (p : Pos S) (v : CellVal Symbol) (hb : p.IsBdry) : a (TabVar.cell t d p v) = decide (v = CellVal.bdry)

theorem MIPRE.TM.CookLevin.sat_bdry_head {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin (S + 1)) (d : Tape i w) (p : Pos S) (hb : p.IsBdry) : a (TabVar.head t d p) = false

theorem MIPRE.TM.CookLevin.sat_emitted_zero {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) : a (TabVar.emitted 0) = false

theorem MIPRE.TM.CookLevin.sat_emitted_succ {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin S) : a (TabVar.emitted t.succ) = true → a (TabVar.emitted t.castSucc) = true ∨ a (TabVar.emitOne t) = true

theorem MIPRE.TM.CookLevin.sat_emitted_mono {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin S) : a (TabVar.emitted t.castSucc) = true → a (TabVar.emitted t.succ) = true

theorem MIPRE.TM.CookLevin.sat_emitOne_emitted {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin S) : a (TabVar.emitOne t) = true → a (TabVar.emitted t.succ) = true

theorem MIPRE.TM.CookLevin.sat_emitOne_once {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin S) : ¬(a (TabVar.emitOne t) = true ∧ a (TabVar.emitted t.castSucc) = true)

theorem MIPRE.TM.CookLevin.sat_emitBad {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (t : Fin S) : a (TabVar.emitBad t) = false

theorem MIPRE.TM.CookLevin.sat_final_state {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) : a (TabVar.state (Fin.last S) none) = true

theorem MIPRE.TM.CookLevin.sat_final_emitted {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) : a (TabVar.emitted (Fin.last S)) = true

theorem MIPRE.TM.CookLevin.sat_window {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (hchk : IsCheckCircuit M acc chk) (hC : chk.RefsLt) (hin : chk.InputsLt) (hne : chk.gates ≠ []) (t : Fin S) (js : Tape i w → Center S) : checkPred M acc fun (v : WinVar i w Symbol State) => a (winVarOf t js v)

The window clauses force, through the check circuit, local consistency of every window.

theorem MIPRE.TM.CookLevin.rowOk_zero {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) : RowOk a 0 (Turing.MultiInputTM.initCfg (inputOf s₀ s₁ fixed chk a))

Row 0 encodes the initial configuration on the inputs read off the assignment.

theorem MIPRE.TM.CookLevin.rows_of_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (hchk : IsCheckCircuit M acc chk) (hC : chk.RefsLt) (hin : chk.InputsLt) (hne : chk.gates ≠ []) (t : ℕ) (ht : t ≤ S) : RowOk a ⟨t, ⋯⟩ (cfgAt M t) ∧ a (TabVar.emitted ⟨t, ⋯⟩) = decide (M.outputString (Turing.MultiInputTM.initCfg (inputOf s₀ s₁ fixed chk a)) t ≠ []) ∧ (M.outputString (Turing.MultiInputTM.initCfg (inputOf s₀ s₁ fixed chk a)) t).length ≤ 1 ∧ ∀ s ∈ M.outputString (Turing.MultiInputTM.initCfg (inputOf s₀ s₁ fixed chk a)) t, s = acc

The rows of a satisfying assignment encode the run on the inputs read off it, with the emission bookkeeping: emitted t iff something was output before time t, at most one symbol, and only acc.

theorem MIPRE.TM.CookLevin.acceptsIn_of_tableau_sat {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (a : TabVar i w Symbol State S chk.gates.length → Bool) (hSat : (tableau M s₀ s₁ S fixed chk).Sat a) (hchk : IsCheckCircuit M acc chk) (hC : chk.RefsLt) (hin : chk.InputsLt) (hne : chk.gates ≠ []) : (∀ (j : Fin i) (x : List Symbol), fixed j = some x → inputOf s₀ s₁ fixed chk a j = x) ∧ (∀ (j : Fin i), fixed j = none → ∀ s ∈ inputOf s₀ s₁ fixed chk a j, s = s₀ ∨ s = s₁) ∧ (∀ (j : Fin i) (p : Pos S) (v : CellVal Symbol), a (TabVar.cell 0 (Sum.inl j) p v) = decide (v = inputCellVal (inputOf s₀ s₁ fixed chk a j) p)) ∧ AcceptsIn M acc (inputOf s₀ s₁ fixed chk a) S

Soundness of the tableau. A satisfying assignment reads, on its time-0 rows, the inputs inputOf, which extend the fixed strings by strings over {s₀, s₁}, and M accepts them within S steps.

The equivalence

theorem MIPRE.TM.CookLevin.tableau_sat_iff {i w : ℕ} {Symbol : Type u_1} {State : Type u_2} [Fintype Symbol] [DecidableEq Symbol] [Fintype State] [DecidableEq State] {S : ℕ} (M : Turing.MultiInputTM i w Symbol State) (acc s₀ s₁ : Symbol) (fixed : Fin i → Option (List Symbol)) (chk : SAT.Circuit) (hchk : IsCheckCircuit M acc chk) (hC : chk.RefsLt) (hin : chk.InputsLt) (hne : chk.gates ≠ []) : (∃ (a : TabVar i w Symbol State S chk.gates.length → Bool), (tableau M s₀ s₁ S fixed chk).Sat a) ↔ ∃ (input : Fin i → List Symbol), (∀ (j : Fin i) (x : List Symbol), fixed j = some x → input j = x) ∧ (∀ (j : Fin i), fixed j = none → ∀ s ∈ input j, s = s₀ ∨ s = s₁) ∧ AcceptsIn M acc input S

Correctness of the Cook–Levin tableau (lem:correct-tableau): the tableau formula of S steps is satisfiable iff M accepts, within S steps, some inputs that extend the fixed strings by strings over {s₀, s₁} on the free tapes.