Assembling the succinct Cook–Levin theorem

MIPRE.SAT.succinctCookLevin inhabits SuccinctCookLevin, which is blueprint thm:succinct-sat. Everything mathematical is already proved; what is left is to discharge, from the validity hypotheses, the side conditions the describer's theorems carry at e = eOf T σ, and to name the two parameter functions.

• T ≤ Sof (eOf T σ), T + 3 < 2 ^ W (eOf T σ) and FixedLen: the five fixed tapes are shorter than the tableau, since |𝒟| ≤ σ < 2 ^ ⌈log σ⌉ and 2 ⌈log n⌉ ≤ T, |x|, |y| ≤ Q ≤ T, and eOf has 5 ⌈log T⌉ + 5 ⌈log σ⌉ + 24 in the exponent.
• 4 T ≤ 2 ^ m: an answer index is below 2 ^ flagOff, and flagOff < m.
• The gate bound: the time bound of the program, evaluated at a linear majorant of the size of its input. To make it computable from the parameters in time polynomial in their bit lengths (item 5) it is rounded up to a power of two, s = 2 ^ (k · r + c) with r = ⌈log ⌈log n⌉⌉ + ⌈log ⌈log T⌉⌉ + ⌈log Q⌉ + ⌈log σ⌉: that needs no arithmetic on numbers, only pow2P on a unary exponent, and it is squeezed between the true gate count and a polynomial in ⌈log n⌉ + ⌈log T⌉ + Q + σ (planning/succinct-cook-levin.md, S4).

Sizes of encodings

theorem MIPRE.TM.CookLevin.Desc.size_le_self (k : ℕ) : k.size ≤ k

The tableau is long enough

theorem MIPRE.TM.CookLevin.Desc.two_pow_le_Sof (T σ k : ℕ) (h : k ≤ eOf T σ) : 2 ^ k ≤ Sof (eOf T σ)

theorem MIPRE.TM.CookLevin.Desc.T_le_Sof (T σ : ℕ) : T ≤ Sof (eOf T σ)

theorem MIPRE.TM.CookLevin.Desc.four_T_add_one_le_Sof (T σ : ℕ) : 4 * T + 1 ≤ Sof (eOf T σ)

theorem MIPRE.TM.CookLevin.Desc.sigma_le_Sof (T σ : ℕ) : σ ≤ Sof (eOf T σ)

theorem MIPRE.TM.CookLevin.Desc.T_add_three_lt (T σ : ℕ) : T + 3 < 2 ^ W (eOf T σ)

theorem MIPRE.TM.CookLevin.Desc.fixedLen_of_valid (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : FixedLen (eOf T σ) D n T x y

The five fixed input tapes are shorter than the tableau.

theorem MIPRE.TM.CookLevin.Desc.four_T_le_m (T σ : ℕ) : 4 * T ≤ 2 ^ mOf (eOf T σ) Gc

An answer index is below 2 ^ m.

The describer in the order the structure asks for

noncomputable def MIPRE.TM.CookLevin.Desc.toPInp : Cost.PolyTimeFun SAT.DescInput PInp

((𝒟, n, T, Q, σ), x, y) reordered to ((T, σ), (𝒟, n), (x, y)).

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.toPInp_apply (inp : SAT.DescInput) : toPInp.toFun inp = ((inp.1.2.2.1, inp.1.2.2.2.2), (inp.1.1, inp.1.2.1), inp.2.1, inp.2.2)

noncomputable def MIPRE.TM.CookLevin.Desc.describeCirc : Cost.PolyTimeFun SAT.DescInput SAT.Circuit

The describer, in the structure's argument order.

Equations

• MIPRE.TM.CookLevin.Desc.describeCirc = MIPRE.TM.CookLevin.Desc.describeP.comp MIPRE.TM.CookLevin.Desc.toPInp

theorem MIPRE.TM.CookLevin.Desc.describeCirc_apply (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) : describeCirc.toFun ((D, n, T, Q, σ), x, y) = descCirc (eOf T σ) T D n x y

The size of the describer's input

def MIPRE.TM.CookLevin.Desc.LOf (n T Q σ : ℕ) : ℕ

The parameter the gate bound is a polynomial in.

Equations

• MIPRE.TM.CookLevin.Desc.LOf n T Q σ = n.size + T.size + Q + σ

theorem MIPRE.TM.CookLevin.Desc.esize_toPInp_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : Cost.esize (toPInp.toFun ((D, n, T, Q, σ), x, y)) ≤ 21 * LOf n T Q σ + 10

The two parameter functions

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

The variable-count exponent m(T, σ).

Equations

• MIPRE.TM.CookLevin.Desc.mParam T σ = MIPRE.TM.CookLevin.Desc.mOf (MIPRE.TM.CookLevin.Desc.eOf T σ) MIPRE.TM.CookLevin.Desc.Gc

theorem MIPRE.TM.CookLevin.Desc.mParam_eq (T σ : ℕ) : mParam T σ = 431 + Qb + Gb Gc + 75 * T.size + 75 * σ.size

theorem MIPRE.TM.CookLevin.Desc.mParam_le (T σ : ℕ) : mParam T σ ≤ (431 + Qb + Gb Gc + 75) * (T.size + σ.size + 1)

def MIPRE.TM.CookLevin.Desc.rParam (n T Q σ : ℕ) : ℕ

The bit lengths of the parameters: the exponent of the gate bound is a multiple of this, which is why the bound is computable without any arithmetic on numbers.

Equations

• MIPRE.TM.CookLevin.Desc.rParam n T Q σ = n.size.size + T.size.size + Q.size + σ.size

Rounding a polynomial bound up to a power of two

Item 5 asks for the gate bound to be computable in time polynomial in the bit lengths of the parameters, while item 3 lets it grow polynomially in Q and σ themselves. So the bound is a number of about log Q + log σ bits that depends polynomially on Q, and computing it looks as though it needs binary multiplication, which the ambient model does not have. roundUp P is the way out: a power of two whose exponent is a multiple of rParam, so that the exponent is unary and the value is pow2P on it. It is squeezed between P and a polynomial, which is le_roundUp and roundUp_le.

noncomputable def MIPRE.TM.CookLevin.Desc.roundK (P : Polynomial ℕ) : ℕ

The degree of a polynomial bound.

Equations

• MIPRE.TM.CookLevin.Desc.roundK P = P.natDegree

noncomputable def MIPRE.TM.CookLevin.Desc.roundA (P : Polynomial ℕ) : ℕ

The coefficient sum of a polynomial bound.

Equations

• MIPRE.TM.CookLevin.Desc.roundA P = ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i

noncomputable def MIPRE.TM.CookLevin.Desc.roundC (P : Polynomial ℕ) : ℕ

The additive constant of the rounded bound.

Equations

• MIPRE.TM.CookLevin.Desc.roundC P = (MIPRE.TM.CookLevin.Desc.roundA P * 5 ^ MIPRE.TM.CookLevin.Desc.roundK P).size

noncomputable def MIPRE.TM.CookLevin.Desc.roundUp (P : Polynomial ℕ) (n T Q σ : ℕ) : ℕ

A polynomial bound, rounded up to a power of two whose exponent is a multiple of the bit lengths of the parameters.

Equations

• MIPRE.TM.CookLevin.Desc.roundUp P n T Q σ = 2 ^ (MIPRE.TM.CookLevin.Desc.roundK P * MIPRE.TM.CookLevin.Desc.rParam n T Q σ + MIPRE.TM.CookLevin.Desc.roundC P)

theorem MIPRE.TM.CookLevin.Desc.L_lt (n T Q σ : ℕ) : LOf n T Q σ + 1 ≤ 5 * 2 ^ rParam n T Q σ

theorem MIPRE.TM.CookLevin.Desc.le_roundUp (P : Polynomial ℕ) (n T Q σ : ℕ) : Polynomial.eval (LOf n T Q σ) P ≤ roundUp P n T Q σ

The rounded bound dominates the polynomial.

theorem MIPRE.TM.CookLevin.Desc.two_pow_rParam_le (n T Q σ : ℕ) : 2 ^ rParam n T Q σ ≤ (2 * LOf n T Q σ + 1) ^ 4

noncomputable def MIPRE.TM.CookLevin.Desc.roundPoly (P : Polynomial ℕ) : Polynomial ℕ

The polynomial the rounded bound stays inside.

Equations

• MIPRE.TM.CookLevin.Desc.roundPoly P = Polynomial.C (2 ^ MIPRE.TM.CookLevin.Desc.roundC P) * (Polynomial.C 2 * Polynomial.X + Polynomial.C 1) ^ (4 * MIPRE.TM.CookLevin.Desc.roundK P)

theorem MIPRE.TM.CookLevin.Desc.roundUp_le (P : Polynomial ℕ) (n T Q σ : ℕ) : roundUp P n T Q σ ≤ Polynomial.eval (LOf n T Q σ) (roundPoly P)

The rounded bound is still polynomial.

The gate bound of the describer

noncomputable def MIPRE.TM.CookLevin.Desc.gatePoly : Polynomial ℕ

The time bound of the describer at a linear majorant of the size of its input.

Equations

• MIPRE.TM.CookLevin.Desc.gatePoly = MIPRE.TM.CookLevin.Desc.describeSize.comp (Polynomial.C 21 * Polynomial.X + Polynomial.C 10)

noncomputable def MIPRE.TM.CookLevin.Desc.sParam (n T Q σ : ℕ) : ℕ

The gate bound s(n, T, Q, σ), rounded up to a power of two.

Equations

• MIPRE.TM.CookLevin.Desc.sParam n T Q σ = MIPRE.TM.CookLevin.Desc.roundUp MIPRE.TM.CookLevin.Desc.gatePoly n T Q σ

theorem MIPRE.TM.CookLevin.Desc.sParam_le (n T Q σ : ℕ) : sParam n T Q σ ≤ Polynomial.eval (LOf n T Q σ) (roundPoly gatePoly)

theorem MIPRE.TM.CookLevin.Desc.describeCirc_size_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : (describeCirc.toFun ((D, n, T, Q, σ), x, y)).size ≤ sParam n T Q σ

The describer has at most s gates (item 3).

The parameters as programs (item 5)

noncomputable def MIPRE.TM.CookLevin.Desc.sizeN : Cost.PolyTimeFun ℕ ℕ

Nat.size.

Equations

• MIPRE.TM.CookLevin.Desc.sizeN = MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ MIPRE.TM.CookLevin.Desc.sizeU

@[simp]

theorem MIPRE.TM.CookLevin.Desc.sizeN_apply (k : ℕ) : sizeN.toFun k = k.size

noncomputable def MIPRE.TM.CookLevin.Desc.rProg : Cost.PolyTimeFun (ℕ × ℕ × ℕ × ℕ) Cost.Unary

rParam, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_rProg (p : ℕ × ℕ × ℕ × ℕ) : List.length (rProg.toFun p) = rParam p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Desc.roundUpProg (P : Polynomial ℕ) : Cost.PolyTimeFun (ℕ × ℕ × ℕ × ℕ) ℕ

A rounded bound, as a program: a power of two whose exponent is unary, so no arithmetic on numbers is needed.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.roundUpProg_apply (P : Polynomial ℕ) (p : ℕ × ℕ × ℕ × ℕ) : (roundUpProg P).toFun p = roundUp P p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Desc.sProg : Cost.PolyTimeFun (ℕ × ℕ × ℕ × ℕ) ℕ

sParam, as a program.

Equations

• MIPRE.TM.CookLevin.Desc.sProg = MIPRE.TM.CookLevin.Desc.roundUpProg MIPRE.TM.CookLevin.Desc.gatePoly

theorem MIPRE.TM.CookLevin.Desc.sProg_apply (p : ℕ × ℕ × ℕ × ℕ) : sProg.toFun p = sParam p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.SAT.succinctCookLevin : SuccinctCookLevin

The succinct Cook–Levin theorem (blueprint thm:succinct-sat; the paper's prop:standard-succinct-sat): the structure is inhabited.

Equations

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