The halting verifier along the paper's route: sizes

The sizes of the descriptions the accounting of Paper/Cost.lean runs on, each an exact affine function of |M| + |λ| — the binary encodings' sizes esize M + esize lam — with a constant depending on G, U, UT and S' alone:

• the code of the map F (esize_F_code), which carries body, M and λ as constants;
• the two-argument program kleeneProg of the fixed point (esize_kleeneProg_F);
• the decider dec M λ itself, a hardcoding of kleeneProg to its own description (esize_dec), so twice the previous plus a constant — this is the 2|c| of the criterion route and the reason the parameter λ(M) of lem:lambda is Λ₀ + 4|M|;
• F applied to the decider (esize_F_dec), the program the fixed point actually runs;
• the time bound of F (F_timeBound_eval) and the overhead of the fixed point's transfer (kleeneOverhead_eq).

The constants are what Lean computes from the constructors; they are named rather than tracked, since only their existence matters downstream.

theorem MIPRE.Halting.esize_nat_le_self (n : ℕ) : Cost.esize n ≤ 4 * n + 1

esize n ≤ 4n + 1: the binary numeral of n has at most size n ≤ n digits.

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

The size of the code of F beyond |M| + |λ|.

Equations

• MIPRE.Halting.cF G U UT S' = MIPRE.Cost.esize (MIPRE.Halting.body G U UT S') + MIPRE.Cost.esize MIPRE.Cost.smnProg + 77

theorem MIPRE.Halting.esize_F_code (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.esize (F G U UT S' M lam).code = Cost.esize M + Cost.esize lam + cF G U UT S'

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

The size of kleeneProg U.univ F beyond |M| + |λ|.

Equations

• MIPRE.Halting.cK G U UT S' = MIPRE.Halting.cF G U UT S' + MIPRE.Cost.esize U.univ + MIPRE.Cost.esize MIPRE.Cost.smnProg + 136

theorem MIPRE.Halting.esize_kleeneProg_F (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.esize (U.univ.kleeneProg (F G U UT S' M lam)) = Cost.esize M + Cost.esize lam + cK G U UT S'

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

The size of the decider dec M λ beyond 2 (|M| + |λ|).

Equations

• MIPRE.Halting.cD G U UT S' = 2 * MIPRE.Halting.cK G U UT S' + 35

theorem MIPRE.Halting.esize_dec (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.esize (dec G U UT S' M lam) = 2 * (Cost.esize M + Cost.esize lam) + cD G U UT S'

theorem MIPRE.Halting.size_descData (M : Cost.Prog) (lam : ℕ) (e : Cost.Prog) : (Cost.encode (M, lam, e)).size = Cost.esize M + Cost.esize lam + Cost.esize e + 2

The description (M, (λ, e)) has size |M| + |λ| + |e| + 2.

theorem MIPRE.Halting.esize_F_apply (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) (e : Cost.Prog) : Cost.esize ((F G U UT S' M lam).toFun e) = Cost.esize (body G U UT S') + Cost.esize M + Cost.esize lam + Cost.esize e + 37

F e = hardcode body (M, (λ, e)) has size |body| + |M| + |λ| + |e| + 37.

theorem MIPRE.Halting.F_timeBound_eval (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam x : ℕ) : Polynomial.eval x (F G U UT S' M lam).timeBound = 2 * (Cost.esize (body G U UT S') + Cost.esize M + Cost.esize lam + x) + 47

The time bound of F: affine in the argument and in |body| + |M| + |λ|.

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

The overhead of the fixed point's time transfer beyond 21 (|M| + |λ|).

Equations

• MIPRE.Halting.cO G U UT S' = 7 * MIPRE.Halting.cK G U UT S' + 5 * MIPRE.Halting.cD G U UT S' + 4 * MIPRE.Cost.esize (MIPRE.Halting.body G U UT S') + 181

theorem MIPRE.Halting.kleeneOverhead_eq (G : GapCompression) (U : Cost.UniversalMachine) (UT : Cost.ClockedUniversalMachine) (S' M : Cost.Prog) (lam : ℕ) : Cost.kleeneOverhead U (F G U UT S' M lam) = 21 * (Cost.esize M + Cost.esize lam) + cO G U UT S'