The output at C λ, read at λ

The tailored presentation of Introspection.seven at λ runs seven's construction at C λ, where C is the constant of TailoredVerifier.ofTNFVT_isBounded (the input's normal form verifier is C λ-bounded). This file collects what that rescaling needs:

• λ ↦ 2^k λ as a polynomial-time function (mulPow2F), the constant being rounded up to a power of two;
• budgets at C λ are budgets at λ with the exponent multiplied by C (ansBound_scale, lenIntro_within);
• at index 0 an output whose calculator outputs 0 and whose processor outputs no constraint has a perfect ZPC strategy, the trivial one (hasPerfectZPC_of_zero).

Multiplication by a power of two

noncomputable def MIPRE.Tailored.Intro.Scale.doubleF : Cost.PolyTimeFun ℕ ℕ

n ↦ 2 n.

Equations

• MIPRE.Tailored.Intro.Scale.doubleF = MIPRE.Cost.PolyTimeFun.natBit.ap₂ (MIPRE.Cost.PolyTimeFun.const false) (MIPRE.Cost.PolyTimeFun.id ℕ)

@[simp]

theorem MIPRE.Tailored.Intro.Scale.doubleF_apply (n : ℕ) : doubleF.toFun n = 2 * n

noncomputable def MIPRE.Tailored.Intro.Scale.mulPow2F : ℕ → Cost.PolyTimeFun ℕ ℕ

n ↦ 2^k n.

Equations

• MIPRE.Tailored.Intro.Scale.mulPow2F 0 = MIPRE.Cost.PolyTimeFun.id ℕ
• MIPRE.Tailored.Intro.Scale.mulPow2F k.succ = MIPRE.Tailored.Intro.Scale.doubleF.comp (MIPRE.Tailored.Intro.Scale.mulPow2F k)

@[simp]

theorem MIPRE.Tailored.Intro.Scale.mulPow2F_apply (k n : ℕ) : (mulPow2F k).toFun n = 2 ^ k * n

Budgets at C λ

theorem MIPRE.Tailored.Intro.Scale.ansBound_scale (C C' lam n : ℕ) : Introspection.ansBound C' (C * lam) n ≤ Introspection.ansBound (C * C') lam n

2^{(C λ n + 1)^{C'}} ≤ 2^{(λ n + 1)^{C C'}}.

theorem MIPRE.Tailored.Intro.Scale.LenBound.mono {L : Decider} {n B B' : ℕ} (h : LenBound L n B) (hB : B ≤ B') : LenBound L n B'

theorem MIPRE.Tailored.Intro.Scale.lenIntro_within : ∃ (C' : ℕ), ∀ (C : ℕ), 1 ≤ C → ∀ (lam n : ℕ), (LenIntro.lenIntro (C * lam)).TimeBoundAt n (Introspection.ansBound (C * C') lam n) (C * C') ∧ LenBound (LenIntro.lenIntro (C * lam)) n (Introspection.ansBound (C * C') lam n)

The answer-length calculator at C λ is within the budget at λ, with the exponent multiplied by C.

Index zero

theorem MIPRE.Tailored.Intro.Scale.hasPerfectZPC_of_zero {ℓ : ℕ} (W : TailoredVerifier ℓ) (n : ℕ) (hlen : ∀ (x : Cost.BitStr) (κ : Bool), LenIs W.len n x κ 0) (hlp : ∀ (x y aR bR : Cost.BitStr), LpIs W.lp n x y aR bR []) : W.HasPerfectZPC n

An output that is empty at index n has a perfect ZPC strategy there: when the calculator outputs 0 and the processor no constraint, every pair of empty answers is accepted, and the trivial strategy is perfect.