The parameters of the describer: the check circuit and the tableau length

Two constants and one choice.

• chk is the check circuit of the interpreter machine: the truth-table circuit (Fml.table) of its local check predicate checkPred U 1, of winCard 7 6 Sym Ctl inputs and at most 7 · 2 ^ winCard gates — an enormous constant, exactly as the paper's lem:pack-check-size, and formally harmless. chk_isCheckCircuit is the hypothesis of lem:correct-tableau; Gc is its gate count.
• eOf T σ = 5 (⌈log T⌉ + ⌈log σ⌉) + 24 is the exponent of the tableau length: under the validity hypotheses and |a|, |b| ≤ T, the accepting run of U is shorter than 2 ^ eOf T σ (runBound_le_two_pow), so the tableau of Sof (eOf T σ) steps is long enough. The bound comes from an explicit fifth-power majorant of runBound (runBound_le) (planning/succinct-cook-levin.md, S3).

The check circuit

noncomputable def MIPRE.TM.CookLevin.Desc.chkFun (x : Fin (winCard 7 6 Interp.Sym Interp.Ctl) → Bool) : Bool

The local check predicate of the interpreter machine as a Boolean function of the window bits, in the canonical order.

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.chk : SAT.Circuit

The check circuit of the interpreter machine: a truth-table circuit of chkFun, taken from Fml.exists_circuit. It is never unfolded: its defining term mentions Fintype.card (WinVar 7 6 Sym Ctl), whose evaluation does not terminate in practice.

Equations

• MIPRE.TM.CookLevin.Desc.chk = MIPRE.TM.CookLevin.Desc.chk._proof_1.choose

theorem MIPRE.TM.CookLevin.Desc.chk_spec : chk.WellFormed ∧ chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl ∧ chk.size ≤ 7 * 2 ^ winCard 7 6 Interp.Sym Interp.Ctl ∧ ∀ (x : Fin (winCard 7 6 Interp.Sym Interp.Ctl) → Bool), chk.evalBits (List.ofFn x) = chkFun x

noncomputable def MIPRE.TM.CookLevin.Desc.Gc : ℕ

The number of gates of the check circuit.

Equations

• MIPRE.TM.CookLevin.Desc.Gc = MIPRE.TM.CookLevin.Desc.chk.gates.length

theorem MIPRE.TM.CookLevin.Desc.chk_wellFormed : chk.WellFormed

theorem MIPRE.TM.CookLevin.Desc.chk_inputs : chk.inputs = winCard 7 6 Interp.Sym Interp.Ctl

theorem MIPRE.TM.CookLevin.Desc.chk_refsLt : chk.RefsLt

theorem MIPRE.TM.CookLevin.Desc.chk_inputsLt : chk.InputsLt

theorem MIPRE.TM.CookLevin.Desc.chk_gates_ne : chk.gates ≠ []

theorem MIPRE.TM.CookLevin.Desc.chk_isCheckCircuit : IsCheckCircuit Interp.U Interp.Sym.one chk

The check circuit computes the local check predicate: the hypothesis of the correctness of the tableau (IsCheckCircuit, lem:correct-tableau).

The tableau length

theorem MIPRE.TM.CookLevin.Desc.mul_le_mul_pow {a b c d i j M : ℕ} (ha : a ≤ c * M ^ i) (hb : b ≤ d * M ^ j) : a * b ≤ c * d * M ^ (i + j)

a ≤ c · M ^ i and b ≤ d · M ^ j give a · b ≤ c d · M ^ (i + j).

theorem MIPRE.TM.CookLevin.Desc.le_mul_pow_of_le {a c i j M : ℕ} (hM : 1 ≤ M) (h : a ≤ c * M ^ i) (hij : i ≤ j) : a ≤ c * M ^ j

Raising the exponent of a majorant.

theorem MIPRE.TM.CookLevin.Desc.runBound_le (D : Cost.Prog) (n T Q σ : ℕ) (x y a b : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (ha : List.length a ≤ T) (hb : List.length b ≤ T) : Interp.runBound D n x y a b T ≤ 400000 * (T + σ + 1) ^ 5

A fifth-power majorant of the run bound of the interpreter machine under the validity hypotheses and |a|, |b| ≤ T.

def MIPRE.TM.CookLevin.Desc.eOf (T σ : ℕ) : ℕ

The exponent of the tableau length: 5 (⌈log T⌉ + ⌈log σ⌉) + 24.

Equations

• MIPRE.TM.CookLevin.Desc.eOf T σ = 5 * T.size + 5 * σ.size + 24

theorem MIPRE.TM.CookLevin.Desc.sum_le_two_pow (T σ : ℕ) : T + σ + 1 ≤ 2 ^ (T.size + σ.size + 1)

theorem MIPRE.TM.CookLevin.Desc.runBound_le_two_pow (D : Cost.Prog) (n T Q σ : ℕ) (x y a b : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (ha : List.length a ≤ T) (hb : List.length b ≤ T) : Interp.runBound D n x y a b T ≤ Sof (eOf T σ)

The run of the interpreter machine fits in the tableau: under the validity hypotheses and |a|, |b| ≤ T, its accepting run is at most Sof (eOf T σ) steps.