The running time of the wrapper, at one index

Prog.wrapCore_cost' (Halting/WrapperCost.lean) bounds the wrapper of Verifier.ofSamplerDecider explicitly, but asks for the sampler's time bound at every index, while λ-boundedness — of a normal form verifier, or of a tailored one — supplies it only for n ≥ 2. The wrapper calls the sampler at one index only, the index n of its own input (the dimension query (n, dimension) of Prog.wrapHead), so the bound at that index is all the proof uses. This file restates the three stages with the hypothesis at n alone:

• wrapHead_cost_at, wrapPre_cost_at, wrapCore_cost_at: wrapHead_cost', wrapPre_cost', wrapCore_cost' for a sampler with S.TimeBoundAt n Cs kf, at the constant cost function fun _ => Cs — so the bound is the same wrapCoreCost, and the existing accounting applies unchanged;
• esize_wrapCore: the wrapper's description is that of the sampler program plus that of the decider datum plus a constant depending on the universal machine alone.

theorem MIPRE.Cost.Prog.wrapHead_cost_at {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) {n Cs kf : ℕ} (hf : S.TimeBoundAt n Cs kf) (c : Prog) (d r : Data) (t : ℕ) : Eval (wrapHeadEnv S n d) c r t → ∃ t' ≤ t + 60 * wrapHeadZ U S (fun (x : ℕ) => Cs) kf n ^ 2, Eval [(encode n).cons d] (U.univ.wrapHead S.prog c) r t'

The head, at one index: wrapHead_cost' from the sampler's time bound at the index of the input only.

theorem MIPRE.Cost.Prog.wrapPre_cost_at {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) {n Cs kf : ℕ} (hf : S.TimeBoundAt n Cs kf) : (∀ (c : Prog) (A B C r : Data) (t : ℕ), Eval (wrapPreEnvD S n A B C) c r t → ∃ t' ≤ t + (60 * wrapHeadZ U S (fun (x : ℕ) => Cs) kf n ^ 2 + 4), Eval [(encode n).cons (A.cons (B.cons C))] (U.univ.wrapPre S.prog c) r t') ∧ ∀ (c : Prog) (d : Data), d.spine ≤ 1 → ∃ t ≤ 60 * wrapHeadZ U S (fun (x : ℕ) => Cs) kf n ^ 2 + 4, Eval [(encode n).cons d] (U.univ.wrapPre S.prog c) Data.nil t

The prefix, at one index: wrapPre_cost' from the sampler's time bound at the index of the input only.

theorem MIPRE.Cost.Prog.wrapCore_cost_at {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (dec : Prog) {n Cs kf : ℕ} (hf : S.TimeBoundAt n Cs kf) (Td : ℕ → ℕ) (hdec : ∀ (d : Data), ∃ (r : Data), ∃ t ≤ Td d.size, dec.Runs ((encode n).cons d) r t) (d : Data) : ∃ (r : Data), ∃ t ≤ wrapCoreCost U S dec (fun (x : ℕ) => Cs) kf n (Td d.size) d.size, (U.univ.wrapCore S.prog (encode dec)).Runs ((encode n).cons d) r t

The wrapper halts within the explicit wrapCoreCost on every input of index n, from the sampler's time bound at n alone and a bound Td |d| on the string's decider at n.

theorem MIPRE.Cost.Prog.esize_wrapCore (univ sampProg : Prog) (decD : Data) : esize (univ.wrapCore sampProg decD) + esize nil + Data.nil.size = esize (univ.wrapCore nil Data.nil) + esize sampProg + decD.size

The wrapper's description: that of the sampler program, plus that of the decider datum, plus a constant depending on the universal machine alone.