Building the decider 𝒟^halt from (M, λ), in polynomial time

The class verifier of the polynomial-time halting reduction runs, on input z, the verifier 𝒱^halt M λ of Paper/Decider.lean for the machine M = R z at the parameter λ = Λ₀ + 4|M|; so it must compute the description of dec M λ from M and λ. That description is a fixed tree with M's and λ's encodings at two positions (Paper/Size.lean computed its size): dec M λ = hardcode K (encode K) for K = kleeneProg univ F, and F's code holds body, M and λ as constants. decBuild assembles the tree with pair and const over Data (kleeneData, fcodeData, fixData are the three shapes) and is a PolyTimeFun (Prog × ℕ) Prog. Beside it, lamF computes the parameter Λ₀ + 4|M| and cutF K D the answer cutoff 2 ^ (K + D · |λ|) that the class decider applies before running 𝒱^halt's decider — a power of two so that it can be computed from |λ| in unary (expBits), and polynomial in λ since 2 ^ |λ| ≤ 32 λ ^ 4.

The three shapes

def MIPRE.Halting.fcodeData (bodyD MD lamD : Cost.Data) : Cost.Data

The description of F.code from those of body, M and λ.

Equations

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

theorem MIPRE.Halting.toData_F_code (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : (F G U UT S' M lam).code.toData = fcodeData (body G U UT S').toData M.toData (Cost.encode lam)

def MIPRE.Halting.kleeneData (univD fD : Cost.Data) : Cost.Data

The description of kleeneProg univ F from those of univ and F.code.

Equations

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

theorem MIPRE.Halting.toData_kleeneProg (univ : Cost.Prog) (F : Cost.PolyTimeFun Cost.Prog Cost.Prog) : (univ.kleeneProg F).toData = kleeneData univ.toData F.code.toData

def MIPRE.Halting.fixData (kD : Cost.Data) : Cost.Data

The description of hardcode K (encode K) from that of K.

Equations

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

theorem MIPRE.Halting.toData_kleeneFix (U : Cost.UniversalMachine) (F : Cost.PolyTimeFun Cost.Prog Cost.Prog) : (Cost.kleeneFix U F).toData = fixData (U.univ.kleeneProg F).toData

The shapes as polynomial-time functions

noncomputable def MIPRE.Halting.fcodeF (bodyD : Cost.Data) : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Data

fcodeData bodyD on (M, λ), as nested pairs of Data.

Equations

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

@[simp]

theorem MIPRE.Halting.fcodeF_apply (bodyD : Cost.Data) (p : Cost.Prog × ℕ) : (fcodeF bodyD).toFun p = fcodeData bodyD p.1.toData (Cost.encode p.2)

noncomputable def MIPRE.Halting.kleeneF (univD : Cost.Data) : Cost.PolyTimeFun Cost.Data Cost.Data

kleeneData univD on fD, as nested pairs of Data.

Equations

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

@[simp]

theorem MIPRE.Halting.kleeneF_apply (univD fD : Cost.Data) : (kleeneF univD).toFun fD = kleeneData univD fD

noncomputable def MIPRE.Halting.fixF : Cost.PolyTimeFun Cost.Data Cost.Data

fixData on kD, as nested pairs of Data.

Equations

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

@[simp]

theorem MIPRE.Halting.fixF_apply (kD : Cost.Data) : fixF.toFun kD = fixData kD

noncomputable def MIPRE.Halting.decBuild (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) : Cost.PolyTimeFun (Cost.Prog × ℕ) Cost.Prog

The decider's description from (M, λ), in polynomial time.

Equations

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

@[simp]

theorem MIPRE.Halting.decBuild_apply (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' : Cost.Prog) (p : Cost.Prog × ℕ) : (decBuild G U UT S').toFun p = dec G U UT S' p.1 p.2

The parameter and the cutoff

noncomputable def MIPRE.Halting.lamF (Λ₀ : ℕ) : Cost.PolyTimeFun Cost.Prog ℕ

M ↦ Λ₀ + 4|M|: the size of M in unary, four copies, plus the constant, read in binary.

Equations

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

@[simp]

theorem MIPRE.Halting.lamF_apply (Λ₀ : ℕ) (M : Cost.Prog) : (lamF Λ₀).toFun M = Λ₀ + 4 * Cost.esize M

noncomputable def MIPRE.Halting.cutF (K D : ℕ) : Cost.PolyTimeFun ℕ ℕ

λ ↦ 2 ^ (K + D · |λ|): the answer cutoff of the class decider.

Equations

• MIPRE.Halting.cutF K D = MIPRE.Cost.PolyTimeFun.expBits.comp ((MIPRE.Cost.PolyTimeFun.addConstU K).comp ((MIPRE.Cost.PolyTimeFun.unaryMul D).comp (MIPRE.Cost.PolyTimeFun.encodedSizeU ℕ)))

@[simp]

theorem MIPRE.Halting.cutF_apply (K D lam : ℕ) : (cutF K D).toFun lam = 2 ^ (K + D * Cost.esize lam)

theorem MIPRE.Halting.esize_bitStr_ge (l : Cost.BitStr) : 2 * List.length l + 1 ≤ Cost.esize l

A bit string of length k encodes to at least 2k + 1 nodes.

theorem MIPRE.Halting.esize_bitStr_le (l : Cost.BitStr) : Cost.esize l ≤ 4 * List.length l + 1

A bit string of length k encodes to at most 4k + 1 nodes.

theorem MIPRE.Halting.size_le_esize (n : ℕ) : n.size ≤ Cost.esize n

The binary length of n is at most the size of its encoding.

theorem MIPRE.Halting.polynomial_eval_le (P : Polynomial ℕ) (x : ℕ) : Polynomial.eval x P ≤ (∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i) * (x + 1) ^ P.natDegree

A polynomial with natural coefficients is at most A · (x + 1) ^ D, for A the sum of its coefficients and D its degree.

theorem MIPRE.Halting.exists_cut_ge (G : GapCompression) : ∃ (K : ℕ), ∀ (lam : ℕ), Polynomial.eval (C G + lam) G.bound ≤ 2 ^ (K + G.bound.natDegree * Cost.esize lam)

The cutoff dominates the compressor's bound: for K large enough in terms of G and C, poly(C, λ) ≤ 2 ^ (K + deg · |λ|) for every λ, where deg is the degree of G.bound.