The describer as a program

descCircP is the describer circuit as a polynomial-time function of ((e in unary, T), (𝒟, n), (x, y)), and descCircP_apply says it is descCirc. This is item 4 of thm:succinct-sat; item 3, the gate bound, follows from it, because PolyTimeFun.esize_apply_le bounds the size of the output of a program by its time bound (planning/succinct-cook-levin.md, S3).

The candidate of the describer

noncomputable def MIPRE.TM.CookLevin.Desc.signR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) : Cost.PolyTimeFun ι SAT.Fml

The sign at the offset 3 m + k.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.signR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (signR eu k).toFun i = SAT.Fml.inp (3 * mOf (List.length (eu.toFun i)) Gc + k)

noncomputable def MIPRE.TM.CookLevin.Desc.candR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) : CandR ι

candOf: the three field records at the bases 0, m and 2 m, and the three signs.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.candR_ev {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (i : ι) : (candR eu TR).ev i = candOf (List.length (eu.toFun i)) Gc (TR.toFun i)

The fixed tapes

noncomputable def MIPRE.TM.CookLevin.Desc.codesP : Cost.PolyTimeFun Cost.Data (List ℕ)

The symbol codes of the serialization of a value.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.codesOf_S (d : Cost.Data) : codesOf (Interp.S d) = List.map (fun (b : Bool) => if b = true then symCode (CellVal.sym Interp.Sym.one) else symCode (CellVal.sym Interp.Sym.zero)) d.toBits

@[simp]

theorem MIPRE.TM.CookLevin.Desc.codesP_apply (d : Cost.Data) : codesP.toFun d = codesOf (Interp.S d)

noncomputable def MIPRE.TM.CookLevin.Desc.bitsData : Cost.PolyTimeFun Cost.BitStr Cost.Data

A bit string as its encoding.

Equations

• MIPRE.TM.CookLevin.Desc.bitsData = MIPRE.Cost.PolyTimeFun.ofEncodeEq (fun (l : MIPRE.Cost.BitStr) => MIPRE.Cost.encode l) MIPRE.TM.CookLevin.Desc.bitsData._proof_1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.bitsData_apply (l : Cost.BitStr) : bitsData.toFun l = Cost.encode l

noncomputable def MIPRE.TM.CookLevin.Desc.tabsR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (DR : Cost.PolyTimeFun ι Cost.Prog) (nR : Cost.PolyTimeFun ι ℕ) (xR yR : Cost.PolyTimeFun ι Cost.BitStr) : Cost.PolyTimeFun ι (List (ℕ × SAT.Fml))

tabsOf: the value formulas of the five fixed tapes.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.tabsR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (b : Cost.PolyTimeFun ι Cost.Unary) (DR : Cost.PolyTimeFun ι Cost.Prog) (nR : Cost.PolyTimeFun ι ℕ) (xR yR : Cost.PolyTimeFun ι Cost.BitStr) (i : ι) : (tabsR eu TR b DR nR xR yR).toFun i = tabsOf (List.length (eu.toFun i)) (TR.toFun i) (DR.toFun i) (nR.toFun i) (xR.toFun i) (yR.toFun i) (litFields (List.length (eu.toFun i)) Gc (TR.toFun i) (List.length (b.toFun i)))

The describer

@[reducible, inline]

abbrev MIPRE.TM.CookLevin.Desc.DInp : Type

The input of the describer: e in unary and the time bound, the decider and the index, the two questions.

Equations

• MIPRE.TM.CookLevin.Desc.DInp = ((MIPRE.Cost.Unary × ℕ) × (MIPRE.Cost.Prog × ℕ) × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.TM.CookLevin.Desc.euI : Cost.PolyTimeFun DInp Cost.Unary

Equations

• MIPRE.TM.CookLevin.Desc.euI = MIPRE.Cost.PolyTimeFun.fst.ap₁ MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.TM.CookLevin.Desc.TI : Cost.PolyTimeFun DInp ℕ

Equations

• MIPRE.TM.CookLevin.Desc.TI = MIPRE.Cost.PolyTimeFun.snd.ap₁ MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.TM.CookLevin.Desc.DI : Cost.PolyTimeFun DInp Cost.Prog

Equations

• MIPRE.TM.CookLevin.Desc.DI = MIPRE.Cost.PolyTimeFun.fst.ap₁ (MIPRE.Cost.PolyTimeFun.fst.ap₁ MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.TM.CookLevin.Desc.nI : Cost.PolyTimeFun DInp ℕ

Equations

• MIPRE.TM.CookLevin.Desc.nI = MIPRE.Cost.PolyTimeFun.snd.ap₁ (MIPRE.Cost.PolyTimeFun.fst.ap₁ MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.TM.CookLevin.Desc.xI : Cost.PolyTimeFun DInp Cost.BitStr

Equations

• MIPRE.TM.CookLevin.Desc.xI = MIPRE.Cost.PolyTimeFun.fst.ap₁ (MIPRE.Cost.PolyTimeFun.snd.ap₁ MIPRE.Cost.PolyTimeFun.snd)

noncomputable def MIPRE.TM.CookLevin.Desc.yI : Cost.PolyTimeFun DInp Cost.BitStr

Equations

• MIPRE.TM.CookLevin.Desc.yI = MIPRE.Cost.PolyTimeFun.snd.ap₁ (MIPRE.Cost.PolyTimeFun.snd.ap₁ MIPRE.Cost.PolyTimeFun.snd)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.euI_apply (p : DInp) : euI.toFun p = p.1.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.TI_apply (p : DInp) : TI.toFun p = p.1.2

@[simp]

theorem MIPRE.TM.CookLevin.Desc.DI_apply (p : DInp) : DI.toFun p = p.2.1.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.nI_apply (p : DInp) : nI.toFun p = p.2.1.2

@[simp]

theorem MIPRE.TM.CookLevin.Desc.xI_apply (p : DInp) : xI.toFun p = p.2.2.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.yI_apply (p : DInp) : yI.toFun p = p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Desc.descFmlP : Cost.PolyTimeFun DInp SAT.Fml

descFml, as a program.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.descFmlP_apply (p : DInp) : descFmlP.toFun p = descFml (List.length p.1.1) p.1.2 p.2.1.1 p.2.1.2 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Desc.descCircP : Cost.PolyTimeFun DInp SAT.Circuit

The describer circuit, as a program (item 4 of thm:succinct-sat): the flattening of descFml on 3 m + 3 inputs.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.descCircP_apply (p : DInp) : descCircP.toFun p = descCirc (List.length p.1.1) p.1.2 p.2.1.1 p.2.1.2 p.2.2.1 p.2.2.2

The gate bound (item 3)

Item 3 needs no separate induction over the builders: a program's output is no larger than its running time (PolyTimeFun.esize_apply_le), and a circuit's gate count is at most the size of its encoding, so the gate bound of the describer is the time bound of the program that writes it, which is an explicit polynomial.

theorem MIPRE.TM.CookLevin.Desc.size_le_esize (C : SAT.Circuit) : C.size ≤ Cost.esize C

The width e and the index width (item 5)

noncomputable def MIPRE.TM.CookLevin.Desc.sizeU : Cost.PolyTimeFun ℕ Cost.Unary

Nat.size, in unary: one unit per bit.

Equations

• MIPRE.TM.CookLevin.Desc.sizeU = (MIPRE.Cost.PolyTimeFun.const ()).map.comp MIPRE.Cost.PolyTimeFun.natBits

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_sizeU (k : ℕ) : List.length (sizeU.toFun k) = k.size

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

eOf, in unary: it is affine in Nat.size T and Nat.size σ.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_eP (p : ℕ × ℕ) : List.length (eP.toFun p) = eOf p.1 p.2

noncomputable def MIPRE.TM.CookLevin.Desc.mP : Cost.PolyTimeFun Cost.Unary ℕ

The index width m, as a program: it is affine in e, so it is an append in unary.

Equations

• MIPRE.TM.CookLevin.Desc.mP = MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ (MIPRE.TM.CookLevin.Desc.mU (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.mP_apply (u : Cost.Unary) : mP.toFun u = mOf (List.length u) Gc

The describer in the theorem's own parameters

@[reducible, inline]

abbrev MIPRE.TM.CookLevin.Desc.PInp : Type

The input of the theorem's algorithm: the time bound and the size bound, the decider and the index, the two questions. e is computed from T and σ.

Equations

• MIPRE.TM.CookLevin.Desc.PInp = ((ℕ × ℕ) × (MIPRE.Cost.Prog × ℕ) × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.TM.CookLevin.Desc.describeP : Cost.PolyTimeFun PInp SAT.Circuit

The describer, in the theorem's own parameters.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.describeP_apply (p : PInp) : describeP.toFun p = descCirc (eOf p.1.1 p.1.2) p.1.1 p.2.1.1 p.2.1.2 p.2.2.1 p.2.2.2

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

The gate-count bound of the describer, in the theorem's own parameters.

Equations

• MIPRE.TM.CookLevin.Desc.describeSize = MIPRE.TM.CookLevin.Desc.describeP.timeBound

theorem MIPRE.TM.CookLevin.Desc.describe_size_le (p : PInp) : (describeP.toFun p).size ≤ Polynomial.eval (Cost.esize p) describeSize

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

The index width, in the theorem's own parameters.

Equations

• MIPRE.TM.CookLevin.Desc.describeM = MIPRE.TM.CookLevin.Desc.mP.comp MIPRE.TM.CookLevin.Desc.eP

@[simp]

theorem MIPRE.TM.CookLevin.Desc.describeM_apply (p : ℕ × ℕ) : describeM.toFun p = mOf (eOf p.1 p.2) Gc