The decoupled describer as a program, and ℓ₀

ℓ₀ = ⌈log 2T⌉ is pinned by its specification, 2T ≤ 2^{ℓ₀} < 4T for T ≥ 1, so it cannot be replaced by the cheaper Nat.size T + 1, which is right except at powers of two, where it gives 4T and violates the strict bound. Written with Nat.size it is one more than ⌈log T⌉ unless T is a power of two, and that shows on the bits of T as every bit but the top one being zero — which is a fold, so ℓ₀ is a program (planning/decoupled-5sat.md, A1e).

ℓ₀, the index length of the answer blocks

theorem MIPRE.TM.CookLevin.Desc.bitsVal_append_singleton (l : Cost.BitStr) (b : Bool) : Cost.bitsVal (l ++ [b]) = Cost.bitsVal l + if b = true then 2 ^ List.length l else 0

def MIPRE.TM.CookLevin.Desc.lOf (T : ℕ) : ℕ

⌈log 2T⌉, read off the bits of T.

Equations

• MIPRE.TM.CookLevin.Desc.lOf T = if T.bits.dropLast.any id = false then T.size else T.size + 1

theorem MIPRE.TM.CookLevin.Desc.lOf_spec (T : ℕ) (hT : 1 ≤ T) : 2 * T ≤ 2 ^ lOf T ∧ 2 ^ lOf T < 4 * T

ℓ₀ is the ceiling of the logarithm of 2T.

ℓ₀ as a program

noncomputable def MIPRE.TM.CookLevin.Desc.orBoolP : Cost.PolyTimeFun (Bool × Bool) Bool

Equations

• MIPRE.TM.CookLevin.Desc.orBoolP = MIPRE.Cost.PolyTimeFun.fst.ite (MIPRE.Cost.PolyTimeFun.const true) MIPRE.Cost.PolyTimeFun.snd

@[simp]

theorem MIPRE.TM.CookLevin.Desc.orBoolP_apply (p : Bool × Bool) : orBoolP.toFun p = (p.1 || p.2)

theorem MIPRE.TM.CookLevin.Desc.foldl_or_eq_any (l : Cost.BitStr) (s : Bool) : List.foldl (fun (x a : Bool) => x || a) s l = (s || List.any l id)

noncomputable def MIPRE.TM.CookLevin.Desc.anyTrueP : Cost.PolyTimeFun Cost.BitStr Bool

Whether a bit string has a set bit.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.anyTrueP_apply (l : Cost.BitStr) : anyTrueP.toFun l = List.any l id

theorem MIPRE.TM.CookLevin.Desc.length_tail_unary (n : ℕ) : (List.tail (Cost.unary n)).length = n - 1

noncomputable def MIPRE.TM.CookLevin.Desc.dropLastP {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun (List α) (List α)

Dropping the last entry of a list.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dropLastP_apply {α : Type u_1} [Cost.SizedEncoding α] (l : List α) : dropLastP.toFun l = l.dropLast

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

ℓ₀, in unary.

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_lOfU (T : ℕ) : List.length (lOfU.toFun T) = lOf T

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

ℓ₀.

Equations

• MIPRE.TM.CookLevin.Desc.lOfN = MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ MIPRE.TM.CookLevin.Desc.lOfU

@[simp]

theorem MIPRE.TM.CookLevin.Desc.lOfN_apply (T : ℕ) : lOfN.toFun T = lOf T

Padding a field, as a program

noncomputable def MIPRE.TM.CookLevin.Desc.padToP : Cost.PolyTimeFun (Cost.Unary × List SAT.Fml) (List SAT.Fml)

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.padToP_apply (p : Cost.Unary × List SAT.Fml) : padToP.toFun p = SAT.Fml.padTo (List.length p.1) p.2

The link formula as a program

noncomputable def MIPRE.TM.CookLevin.Desc.twoLU {ι : Type u_1} [Cost.SizedEncoding ι] (lu : Cost.PolyTimeFun ι Cost.Unary) : Cost.PolyTimeFun ι Cost.Unary

2 ℓ, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.twoLU lu = (MIPRE.TM.CookLevin.Desc.nsmulU 2).ap₁ lu

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_twoLU {ι : Type u_1} [Cost.SizedEncoding ι] (lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((twoLU lu).toFun i) = 2 * List.length (lu.toFun i)

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

The offset of the five signs, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.sgOffU eu lu = MIPRE.TM.CookLevin.Desc.addU.ap₂ (MIPRE.TM.CookLevin.Desc.twoLU lu) ((MIPRE.TM.CookLevin.Desc.nsmulU 3).ap₁ (MIPRE.TM.CookLevin.Desc.mU eu))

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_sgOffU {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : List.length ((sgOffU eu lu).toFun i) = sgOff (List.length (lu.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

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

The k-th of the five signs.

Equations

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

@[simp]

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

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

The two answer indices, zero-padded, and the three auxiliary indices.

Equations

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

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

Equations

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

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

Equations

• MIPRE.TM.CookLevin.Desc.jR₃ eu lu = MIPRE.SAT.fieldP.ap₂ (MIPRE.Cost.PolyTimeFun.unaryToBin.ap₁ (MIPRE.TM.CookLevin.Desc.twoLU lu)) (MIPRE.TM.CookLevin.Desc.mU eu)

noncomputable def MIPRE.TM.CookLevin.Desc.jR₄ {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : 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.jR₅ {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : 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.jR₁_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (jR₁ eu lu).toFun i = j₁F (List.length (lu.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.jR₃_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (jR₃ eu lu).toFun i = j₃F (List.length (lu.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.jR₄_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (jR₄ eu lu).toFun i = j₄F (List.length (lu.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.jR₅_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (jR₅ eu lu).toFun i = j₅F (List.length (lu.toFun i)) (mOf (List.length (eu.toFun i)) Gc)

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

2T on r bits.

Equations

• MIPRE.TM.CookLevin.Desc.twoTR eu TR = MIPRE.TM.CookLevin.Desc.nbitsR (MIPRE.TM.CookLevin.Desc.mU eu) (MIPRE.TM.CookLevin.Desc.dblR TR)

@[simp]

theorem MIPRE.TM.CookLevin.Desc.twoTR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (i : ι) : (twoTR eu TR).toFun i = nbits (mOf (List.length (eu.toFun i)) Gc) (2 * TR.toFun i)

noncomputable def MIPRE.TM.CookLevin.Desc.xorR {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) : Cost.PolyTimeFun ι SAT.Fml

xor of two readers.

Equations

• MIPRE.TM.CookLevin.Desc.xorR f g = MIPRE.SAT.xorP.ap₂ f g

@[simp]

theorem MIPRE.TM.CookLevin.Desc.xorR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (f g : Cost.PolyTimeFun ι SAT.Fml) (i : ι) : (xorR f g).toFun i = (f.toFun i).xor (g.toFun i)

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

linkFml.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.linkFmlR_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (linkFmlR eu TR lu).toFun i = linkFml (List.length (lu.toFun i)) (mOf (List.length (eu.toFun i)) Gc) (TR.toFun i)

The candidate and the whole formula

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

candOf5.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.candR5_ev {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (lu : Cost.PolyTimeFun ι Cost.Unary) (i : ι) : (candR5 eu TR lu).ev i = candOf5 (List.length (lu.toFun i)) (List.length (eu.toFun i)) (TR.toFun i)

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

descFml5.

Equations

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

theorem MIPRE.TM.CookLevin.Desc.descFml5R_apply {ι : Type u_1} [Cost.SizedEncoding ι] (eu : Cost.PolyTimeFun ι Cost.Unary) (TR : Cost.PolyTimeFun ι ℕ) (lu : Cost.PolyTimeFun ι Cost.Unary) (DR : Cost.PolyTimeFun ι Cost.Prog) (nR : Cost.PolyTimeFun ι ℕ) (xR yR : Cost.PolyTimeFun ι Cost.BitStr) (i : ι) : (descFml5R eu TR lu DR nR xR yR).toFun i = descFml5 (List.length (lu.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.dDR : Cost.PolyTimeFun SAT.DescInput Cost.Prog

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.dnR : Cost.PolyTimeFun SAT.DescInput ℕ

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.dTR : Cost.PolyTimeFun SAT.DescInput ℕ

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.dsR : Cost.PolyTimeFun SAT.DescInput ℕ

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.dxR : Cost.PolyTimeFun SAT.DescInput Cost.BitStr

Equations

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

noncomputable def MIPRE.TM.CookLevin.Desc.dyR : Cost.PolyTimeFun SAT.DescInput Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dDR_apply (p : SAT.DescInput) : dDR.toFun p = p.1.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dnR_apply (p : SAT.DescInput) : dnR.toFun p = p.1.2.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dTR_apply (p : SAT.DescInput) : dTR.toFun p = p.1.2.2.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dsR_apply (p : SAT.DescInput) : dsR.toFun p = p.1.2.2.2.2

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dxR_apply (p : SAT.DescInput) : dxR.toFun p = p.2.1

@[simp]

theorem MIPRE.TM.CookLevin.Desc.dyR_apply (p : SAT.DescInput) : dyR.toFun p = p.2.2

noncomputable def MIPRE.TM.CookLevin.Desc.dEu : Cost.PolyTimeFun SAT.DescInput Cost.Unary

e, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.dEu = MIPRE.TM.CookLevin.Desc.eP.ap₁ (MIPRE.TM.CookLevin.Desc.dTR.pair MIPRE.TM.CookLevin.Desc.dsR)

noncomputable def MIPRE.TM.CookLevin.Desc.dLu : Cost.PolyTimeFun SAT.DescInput Cost.Unary

ℓ₀, in unary.

Equations

• MIPRE.TM.CookLevin.Desc.dLu = MIPRE.TM.CookLevin.Desc.lOfU.ap₁ MIPRE.TM.CookLevin.Desc.dTR

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_dEu (p : SAT.DescInput) : List.length (dEu.toFun p) = eOf p.1.2.2.1 p.1.2.2.2.2

@[simp]

theorem MIPRE.TM.CookLevin.Desc.length_dLu (p : SAT.DescInput) : List.length (dLu.toFun p) = lOf p.1.2.2.1

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

The decoupled describer, as a program (item 4 of lem:decoupled-5sat).

Equations

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

theorem MIPRE.TM.CookLevin.Desc.describe5P_apply (p : SAT.DescInput) : describe5P.toFun p = descCirc5 (lOf p.1.2.2.1) p.1.2.2.1 (eOf p.1.2.2.1 p.1.2.2.2.2) p.1.1 p.1.2.1 p.2.1 p.2.2

The gate bound

theorem MIPRE.TM.CookLevin.Desc.lOf_le_mOf (T σ : ℕ) : lOf T ≤ mOf (eOf T σ) Gc

theorem MIPRE.TM.CookLevin.Desc.one_le_mOf (T σ : ℕ) : 1 ≤ mOf (eOf T σ) Gc

theorem MIPRE.TM.CookLevin.Desc.esize_descInput_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : Cost.esize ((D, n, T, Q, σ), x, y) ≤ 25 * LOf n T Q σ + 12

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

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

Equations

• MIPRE.TM.CookLevin.Desc.gatePoly5 = MIPRE.TM.CookLevin.Desc.describe5P.timeBound.comp (Polynomial.C 25 * Polynomial.X + Polynomial.C 12)

theorem MIPRE.TM.CookLevin.Desc.describe5P_size_le (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) : (describe5P.toFun ((D, n, T, Q, σ), x, y)).size ≤ roundUp gatePoly5 n T Q σ

The decoupled describer is small (item 3 of lem:decoupled-5sat).

The parameters as programs

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

Equations

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

theorem MIPRE.TM.CookLevin.Desc.params5_apply (n T Q σ : ℕ) : params5.toFun (n, T, Q, σ) = (lOf T, mParam T σ, roundUp gatePoly5 n T Q σ)

noncomputable def MIPRE.SAT.decoupledDescriber : DecoupledDescriber

Explicit succinct decoupled descriptions of deciders (blueprint lem:decoupled-5sat; the paper's prop:explicit-succinct-deciders): the structure is inhabited.

Equations

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