The windowed describer as a program, and the structure inhabited

The program of descCirc6 (slice P4g of the Aldous–Lyons track), assembled from the readers of DecoupledProg.lean at the six-block layout: the window lengths are read in unary off the input, every offset is a unary sum, and the offset 2^ℓa of the third window is a power of two (pow2P), so no arithmetic on binary numbers is needed. The gate bound is the rounded bound of Assemble.lean at a linear majorant of the input size, which uses that the windows are no wider than the witness indices, themselves logarithmic in T and σ.

The link formula and the whole formula, as programs

noncomputable def MIPRE.TM.CookLevin.Desc.wOffU {ι : Type u_1} [Cost.SizedEncoding ι] (la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

The offset of the witness indices, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.wOffU la lb lc = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.TM.CookLevin.Desc.addU.ap₂ la lb) lc

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_wOffU {ι : Type u_1} [Cost.SizedEncoding ι] (la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((wOffU la lb lc).toFun i) = wOff (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.sgOff6U {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

The offset of the six signs, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.sgOff6U eu la lb lc = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.TM.CookLevin.Desc.wOffU la lb lc) ((MIPRE.TM.CookLevin.Desc.nsmulU 3).ap₁ (MIPRE.TM.CookLevin.Desc.mU eu))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_sgOff6U {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((sgOff6U eu la lb lc).toFun i) = sgOff6 (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

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

The k-th of the six signs.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.sg6R_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) (k : ℕ) (i : ι) : (sg6R eu la lb lc k).toFun i = t₀F (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc) k

noncomputable def MIPRE.TM.CookLevin.Desc.kR₁ {ι : Type u_1} [Cost.SizedEncoding ι] (eu la : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

The three window indices, zero-padded, and the three witness indices.

Equations

• MIPRE.TM.CookLevin.Desc.kR₁ eu la = MIPRE.TM.CookLevin.Desc.padToP.ap₂ (MIPRE.TM.CookLevin.Desc.mU eu) (MIPRE.SAT.fieldP.ap₂ (MIPRE.Cost.PolyTimeFun.const 0) la)

noncomputable def MIPRE.TM.CookLevin.Desc.kR₂ {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

Equations

• MIPRE.TM.CookLevin.Desc.kR₂ eu la lb = MIPRE.TM.CookLevin.Desc.padToP.ap₂ (MIPRE.TM.CookLevin.Desc.mU eu) (MIPRE.SAT.fieldP.ap₂ (MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ la) lb)

noncomputable def MIPRE.TM.CookLevin.Desc.kR₃ {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.kR₄ {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

Equations

• MIPRE.TM.CookLevin.Desc.kR₄ eu la lb lc = MIPRE.SAT.fieldP.ap₂ (MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ (MIPRE.TM.CookLevin.Desc.wOffU la lb lc)) (MIPRE.TM.CookLevin.Desc.mU eu)

noncomputable def MIPRE.TM.CookLevin.Desc.kR₅ {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.kR₆ {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι (List SAT.Fml)

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.kR₁_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (kR₁ eu la).toFun i = k₁F (List.length (la.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.kR₂_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (kR₂ eu la lb).toFun i = k₂F (List.length (la.toFun i)) (List.length (lb.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.kR₃_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (kR₃ eu la lb lc).toFun i = k₃F (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.kR₄_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (kR₄ eu la lb lc).toFun i = k₄F (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.kR₅_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (kR₅ eu la lb lc).toFun i = k₅F (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.kR₆_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (kR₆ eu la lb lc).toFun i = k₆F (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

noncomputable def MIPRE.TM.CookLevin.Desc.pow2aR {ι : Type u_1} [Cost.SizedEncoding ι] (eu la : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.BitStr

2^ℓa on r bits.

Equations

• MIPRE.TM.CookLevin.Desc.pow2aR eu la = MIPRE.TM.CookLevin.Desc.nbitsR (MIPRE.TM.CookLevin.Desc.mU eu) (MIPRE.Cost.PolyTimeFun.natBits.ap₁ (MIPRE.TM.CookLevin.Desc.pow2P.ap₁ la))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.pow2aR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu la : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (pow2aR eu la).toFun i = nbits (mOf (List.length (eu.toFun i)) Gc) (2 ^ List.length (la.toFun i))

noncomputable def MIPRE.TM.CookLevin.Desc.link6FmlR {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (la lb lc : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι SAT.Fml

link6Fml.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.link6FmlR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (link6FmlR eu TR la lb lc).toFun i = link6Fml (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (mOf (List.length (eu.toFun i)) Gc) (TR.toFun i)

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

candOf6.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.candR6_ev {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (la lb lc : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (candR6 eu TR la lb lc).ev i = candOf6 (wOff (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i))) (List.length (eu.toFun i)) (TR.toFun i)

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

descFml6.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.descFml6R_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (la lb lc : Cost.PolyTimeFun ι Cost.Unary) (DR : Cost.PolyTimeFun ι Cost.Prog) (nR : Cost.PolyTimeFun ι ℕ) (xR yR : Cost.PolyTimeFun ι Cost.BitStr) (i : ι) : (descFml6R eu TR la lb lc DR nR xR yR).toFun i = descFml6 (List.length (la.toFun i)) (List.length (lb.toFun i)) (List.length (lc.toFun i)) (TR.toFun i) (List.length (eu.toFun i)) (DR.toFun i) (nR.toFun i) (xR.toFun i) (yR.toFun i)

The describer in the structure's argument order

noncomputable def MIPRE.TM.CookLevin.Desc.w6a : Cost.PolyTimeFun SAT.Desc6Input Cost.Unary

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.w6b : Cost.PolyTimeFun SAT.Desc6Input Cost.Unary

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.w6c : Cost.PolyTimeFun SAT.Desc6Input Cost.Unary

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.w6a_apply (p : SAT.Desc6Input) : w6a.toFun p = p.1.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.w6b_apply (p : SAT.Desc6Input) : w6b.toFun p = p.1.2.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.w6c_apply (p : SAT.Desc6Input) : w6c.toFun p = p.1.2.2

noncomputable def MIPRE.TM.CookLevin.Desc.describe6P : Cost.PolyTimeFun SAT.Desc6Input SAT.Circuit

The windowed describer, as a program (slice P4g, item 4).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.describe6P_apply (p : SAT.Desc6Input) : describe6P.toFun p = descCirc6 (List.length p.1.1) (List.length p.1.2.1) (List.length p.1.2.2) p.2.1.2.2.1 (eOf p.2.1.2.2.1 p.2.1.2.2.2.2) p.2.1.1 p.2.1.2.1 p.2.2.1 p.2.2.2

The gate bound

@[reducible, inline]

noncomputable abbrev MIPRE.TM.CookLevin.Desc.mK : ℕ

The constant of mParam_le.

Equations

• MIPRE.TM.CookLevin.Desc.mK = 431 + MIPRE.TM.CookLevin.Desc.Qb + MIPRE.TM.CookLevin.Desc.Gb MIPRE.TM.CookLevin.Desc.Gc + 75

theorem MIPRE.TM.CookLevin.Desc.esize_desc6Input_le (ua ub uc : Cost.Unary) (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (ha : List.length ua ≤ mParam T σ) (hb : List.length ub ≤ mParam T σ) (hc : List.length uc ≤ mParam T σ) : Cost.esize ((ua, ub, uc), (D, n, T, Q, σ), x, y) ≤ (6 * mK + 25) * LOf n T Q σ + (6 * mK + 18)

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

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

Equations

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

theorem MIPRE.TM.CookLevin.Desc.describe6P_size_le (ua ub uc : Cost.Unary) (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (ha : List.length ua ≤ mParam T σ) (hb : List.length ub ≤ mParam T σ) (hc : List.length uc ≤ mParam T σ) : (describe6P.toFun ((ua, ub, uc), (D, n, T, Q, σ), x, y)).size ≤ roundUp gatePoly6 n T Q σ

The windowed describer is small (item 3).

The parameters as programs

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

Equations

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

theorem MIPRE.TM.CookLevin.Desc.params6_apply (n T Q σ : ℕ) : params6.toFun (n, T, Q, σ) = (mParam T σ, roundUp gatePoly6 n T Q σ)

noncomputable def MIPRE.SAT.windowDescriber : WindowDescriber

Succinct decoupled descriptions of deciders through three windows (slice P4g; paper II's prop:explicit-padded-succinct-deciders, whose proof the paper only sketches): the structure is inhabited.

Equations

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