The running time of the wrapper

Decider.wrap reads a string as a decider (Halting/Wrapper.lean); this file bounds its running time. That bound is what makes the verifier a string denotes λ-bounded, and so what makes the classes MIPRE.Halting.classA, classB inhabited at all: until it, every proof of Verifier.IsBounded in the repository was conditional on another time bound.

The shape throughout is Cost.Prog.HasPolyCost: cost at most C n · (|d| + 1) ^ k at index n on input d, with C polynomially bounded and k constant — what Decider.TimeBoundAt asks for after Halting/Bounded.lean, and what composes (Cost.PolyCost). Nothing here is tight: each stage is bounded by a generous square and the stages are summed, since λ-boundedness quantifies the constants away.

Everything is proved on arbitrary data. TimeBoundAt quantifies over every input at the index, well formed or not, so no stage may assume it is handed a question pair:

• Data.toSpine and Prog.lenProgD_runs: the length program on any datum, walking its right spine, not only on a list built by Data.list.
• Prog.wrapCheckEnvN and wrapCheckD_cost_of_eq, wrapCheckD_cost_of_ne: one length check, which compares Data.spine with the sampler's dimension — on encode l that is l.length, and on anything else it is what the program actually computes.
• Prog.wrapCore_hasPolyCost: the whole, by the three outcomes — the first check fails, the second fails, or both pass and the string's own decider runs through the universal machine.
• Verifier.ofSamplerDecider_isBounded: the verifier a pair denotes is n-bounded at every level from some n₀ on, by Verifier.exists_isBounded.

The hypotheses are exactly three: the sampler's program and the string's decider have polynomially bounded cost, and the sampler's dimension is polynomially bounded. For a sampler coming from MIPRE.GapCompression all three are its fields, through CL.Sampler.hasPolyCost_of_timeBound.

The right spine of a datum

def MIPRE.Cost.Data.toSpine : Data → List Data

The right spine of a datum, as a list: list (toSpine d) = d.

Equations

• MIPRE.Cost.Data.nil.toSpine = []
• (a.cons b).toSpine = a :: b.toSpine

theorem MIPRE.Cost.Data.list_toSpine (d : Data) : list d.toSpine = d

theorem MIPRE.Cost.Data.length_toSpine (d : Data) : d.toSpine.length = d.spine

theorem MIPRE.Cost.Prog.lenProgD_runs (d : Data) : ∃ t ≤ (d.spine + 2) * (d.size + 2 * d.spine + 14), lenProg.Runs d (Data.ofNat d.spine) t

The length program on arbitrary data: it walks the right spine.

The stages

def MIPRE.Cost.Prog.wrapHeadEnv {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (d : Data) : Env

The environment the head hands to its continuation.

Equations

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

noncomputable def MIPRE.Cost.Prog.wrapHeadZ {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (Cf : ℕ → ℕ) (kf n : ℕ) : ℕ

The quantity whose square bounds the head's cost at index n, for a sampler running within Cf n · (|d| + 1) ^ kf: the sizes and running times of the dimension query, its simulation, and the conversion of the dimension to unary. Explicit, so that the accounting of the compressor's output can be uniform in its parameters.

Equations

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

theorem MIPRE.Cost.Prog.polyBounded_wrapHeadZ {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) {Cf : ℕ → ℕ} (hCf : PolyBounded Cf) (kf : ℕ) (hdim : PolyBounded S.dim) : PolyBounded fun (n : ℕ) => wrapHeadZ U S Cf kf n

wrapHeadZ is polynomially bounded in the index when the sampler's cost and dimension are.

theorem MIPRE.Cost.Prog.wrapHead_cost' {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (Cf : ℕ → ℕ) (kf : ℕ) (hf : ∀ (n : ℕ) (d : Data), ∃ (r : Data), ∃ t ≤ Cf n * (d.size + 1) ^ kf, S.prog.Runs ((encode n).cons d) r t) (c : Prog) (n : ℕ) (d r : Data) (t : ℕ) : Eval (wrapHeadEnv S n d) c r t → ∃ t' ≤ t + 60 * wrapHeadZ U S Cf kf n ^ 2, Eval [(encode n).cons d] (U.univ.wrapHead S.prog c) r t'

The head, with explicit constants. For a sampler running within Cf n · (|d| + 1) ^ kf, the head costs at most 60 · wrapHeadZ n ^ 2 beyond its continuation: the dimension query runs on a fixed input, and the conversion to unary on the dimension.

The length check, on arbitrary data

def MIPRE.Cost.Prog.wrapCheckEnvN (k m : ℕ) (env : Env) : Env

The environment one length check hands to its continuation, parameterized by the spine length it measured rather than by a bit string: the wrapper is run on malformed inputs too.

Equations

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

def MIPRE.Cost.Prog.checkCost (E m : ℕ) : ℕ

A generous bound on the cost of one length check, in the size of the datum tested and the number it is compared with.

Equations

• MIPRE.Cost.Prog.checkCost E m = 60 * (E + m + 30) ^ 2

theorem MIPRE.Cost.Prog.eq_runB (p q : ℕ) : ∃ t ≤ (p + 1) * (2 * p + 2 * q + 23), eqBitsProg.Runs ((Data.ofNat p).cons (Data.ofNat q)) (encode (decide (p = q))) t

theorem MIPRE.Cost.Prog.check_mul_le {E m a b : ℕ} (ha : a ≤ E + m + 30) (hb : b ≤ 3 * (E + m + 30)) : a * b ≤ 3 * (E + m + 30) ^ 2

Every factor appearing in the check's cost is at most three times E + m + 30.

theorem MIPRE.Cost.Prog.wrapCheckD_cost_of_eq {i j : ℕ} {c : Prog} {env : Env} {v : Data} {m : ℕ} (hi : env.get i = v) (hj : env.get j = Data.ofNat m) (heq : v.spine = m) {r : Data} {t : ℕ} (hc : Eval (wrapCheckEnvN m m env) c r t) : ∃ t' ≤ t + checkCost v.size m, Eval env (wrapCheck i j c) r t'

The check passes.

theorem MIPRE.Cost.Prog.wrapCheckD_cost_of_ne {i j : ℕ} {c : Prog} {env : Env} {v : Data} {m : ℕ} (hi : env.get i = v) (hj : env.get j = Data.ofNat m) (hne : v.spine ≠ m) : ∃ t' ≤ checkCost v.size m, Eval env (wrapCheck i j c) Data.nil t'

The check fails, and the whole wrapper rejects.

The prefix

def MIPRE.Cost.Prog.wrapPreEnvD {ℓ : ℕ} (S : CL.Sampler ℓ) (n : ℕ) (A B C : Data) : Env

The environment the prefix hands to the first length check, for an input whose tail is cons A (cons B C) — the only shape on which the checks run at all.

Equations

• MIPRE.Cost.Prog.wrapPreEnvD S n A B C = B :: C :: A :: B.cons C :: MIPRE.Cost.Prog.wrapHeadEnv S n (A.cons (B.cons C))

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

The prefix, on every input, with explicit constants. On a tail of the shape cons A (cons B C) it hands the environment wrapPreEnvD to its continuation; on a shorter tail it rejects outright. Both cost 60 · wrapHeadZ n ^ 2 + 4 beyond the continuation.

The whole wrapper

theorem MIPRE.Cost.Prog.checkCost_mono {E E' m : ℕ} (h : E ≤ E') : checkCost E m ≤ checkCost E' m

noncomputable def MIPRE.Cost.Prog.wrapCoreCost {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (dec : Prog) (Cf : ℕ → ℕ) (kf n T s : ℕ) : ℕ

The wrapper's cost at index n on an input of size s, when the string's decider runs within T on it: the prefix, the two checks, the copies, and the universal machine on the string's decider.

Equations

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

theorem MIPRE.Cost.Prog.wrapCore_cost' {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (dec : Prog) (Cf : ℕ → ℕ) (kf : ℕ) (hf : ∀ (n : ℕ) (d : Data), ∃ (r : Data), ∃ t ≤ Cf n * (d.size + 1) ^ kf, S.prog.Runs ((encode n).cons d) r t) (n : ℕ) (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 Cf 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 an explicit cost on every input, well formed or not, at an index n at which the string's decider runs within Td |d| on every input d.

theorem MIPRE.Cost.Prog.wrapCore_hasPolyCost {ℓ : ℕ} (U : UniversalMachine) (S : CL.Sampler ℓ) (dec : Prog) (hS : S.prog.HasPolyCost) (hdim : PolyBounded S.dim) (hdec : dec.HasPolyCost) : (U.univ.wrapCore S.prog (encode dec)).HasPolyCost

The wrapper halts within a polynomially bounded cost on every input, well formed or not, provided the sampler and the string's own decider do. This is what inhabits Verifier.IsBounded for the verifier a string denotes.

theorem MIPRE.Verifier.ofSamplerDecider_isBounded {ℓ : ℕ} (U : Cost.UniversalMachine) (S : CL.Sampler ℓ) (dec : Cost.Prog) (hS : S.prog.HasPolyCost) (hdim : Cost.PolyBounded S.dim) (hdec : dec.HasPolyCost) : ∃ (n₀ : ℕ), ∀ (n : ℕ), n₀ ≤ n → (ofSamplerDecider U S dec).IsBounded n

The verifier a string denotes is λ-bounded, at every level from some n₀ on, provided the sampler and the string's own decider have polynomially bounded cost and the sampler's dimension is polynomially bounded. This is what inhabits Verifier.IsBounded.