A tailored verifier as a bounded normal form verifier

TailoredVerifier.ofTNFV U V (MIPRE.Tailored.OfTNFV) presents a tailored verifier as a normal form verifier, its decider the canonical decider canonProg in the wrapper of Verifier.ofSamplerDecider; canonProg is bounded on encodings only. ofTNFVT U V is the same with the total parse in front, canonProgT (MIPRE.Tailored.CanonicalCost), which accepts the same inputs and is bounded on every input. So it denotes the same games, and it is λ'-bounded for a λ' linear in λ:

• ofTNFVT_accepts_iff, ofTNFVT_game: the decider accepts what that of ofTNFV accepts, so the games are equal, and valStar_ofTNFVT, hasPerfectPCC_ofTNFVT transport valStar_ofTNFV, hasPerfectPCC_ofTNFV;
• dom_wrapCoreCost: the wrapper's explicit cost Prog.wrapCoreCost, at the sampler's bound Cs and degree K, is dominated by c (W + 1)^m X^{e (K + 1)} (MIPRE.Repeat.Dom) once W is above 10^K, Cs, the dimension and the sizes of the index and of the two programs;
• ofTNFVT_isBounded: for a fixed universal machine U there is a constant C such that every λ-bounded tailored verifier V gives a (C λ)-bounded normal form verifier ofTNFVT U V. The decider's clause is the wrapper's cost at the index in question (Prog.wrapCore_cost_at, which needs the sampler's bound at that index only, n ≥ 2 being all λ-boundedness supplies) on the canonical decider's (canonProgT_timeBound), dominated with W = n^{A λ}; the size clause is esize_wrapCore and esize_canonProgT.

Arithmetic at n ≥ 2

theorem MIPRE.Tailored.le_pow_self_of_two_le {n : ℕ} (hn : 2 ≤ n) (x : ℕ) : x ≤ n ^ x

theorem MIPRE.Tailored.pow_le_pow_mul {n a b lam : ℕ} (hn : 2 ≤ n) (hab : a ≤ b) : n ^ (a * lam) ≤ n ^ (b * lam)

theorem MIPRE.Tailored.ten_pow_le {n : ℕ} (hn : 2 ≤ n) (lam : ℕ) : 10 ^ lam ≤ n ^ (4 * lam)

10^λ ≤ n^{4 λ} for n ≥ 2.

theorem MIPRE.Tailored.esize_nat_le_pow_four {n : ℕ} (hn : 2 ≤ n) : Cost.esize n ≤ n ^ 4

esize n ≤ n^4 for n ≥ 2: the binary numeral has at most n digits.

The verifier, and its games

noncomputable def MIPRE.Tailored.TailoredVerifier.ofTNFVT {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) : Verifier ℓ

A tailored verifier as a normal form verifier, with a total parse: its sampler, and the canonical decider with the parse in front (canonProgT), wrapped in the question-length check.

Equations

• V.ofTNFVT U = MIPRE.Verifier.ofSamplerDecider U V.sampler (MIPRE.Tailored.canonProgT V.len.prog V.lp.prog)

@[simp]

theorem MIPRE.Tailored.TailoredVerifier.ofTNFVT_sampler {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) : (V.ofTNFVT U).sampler = V.sampler

theorem MIPRE.Tailored.TailoredVerifier.ofTNFVT_accepts_iff_ofTNFV {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) (n : ℕ) (x y a b : Cost.BitStr) : (V.ofTNFVT U).decider.Accepts n x y a b ↔ (V.ofTNFV U).decider.Accepts n x y a b

The decider accepts exactly what that of ofTNFV accepts, on every input.

theorem MIPRE.Tailored.TailoredVerifier.ofTNFVT_accepts_iff {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) (n : ℕ) (x y : V.Questions n) (a b : Cost.BitStr) : (V.ofTNFVT U).decider.Accepts n (CL.toBits x) (CL.toBits y) a b ↔ (V.tgame n).Accepts x y a b

The normal form verifier's decider accepts exactly what the tailored game accepts.

theorem MIPRE.Tailored.TailoredVerifier.ofTNFVT_game {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) (n T : ℕ) : (V.ofTNFVT U).game n T = (V.ofTNFV U).game n T

The games are those of ofTNFV.

theorem MIPRE.Tailored.TailoredVerifier.ofTNFVT_game_D {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame n).maxLen ≤ T) (x y : V.Questions n) (a b : Verifier.Answers (V.tgame n).maxLen) : ((V.ofTNFVT U).game n T).D x y ((Verifier.Answers.castLE hT) a) ((Verifier.Answers.castLE hT) b) = (V.tgame n).toGame.D x y a b

The decision predicates agree on the answers the tailored game has, embedded in the answers of length at most T.

theorem MIPRE.Tailored.TailoredVerifier.valStar_ofTNFVT {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) (n T : ℕ) (hT : (V.tgame n).maxLen ≤ T) : (V.ofTNFVT U).valStar n T = V.valStar n

The values agree, for an answer bound above the tailored game's answer lengths.

theorem MIPRE.Tailored.TailoredVerifier.hasPerfectPCC_ofTNFVT {ℓ : ℕ} (V : TailoredVerifier ℓ) (U : Cost.UniversalMachine) {n T : ℕ} (hT : (V.tgame n).maxLen ≤ T) (h : V.HasPerfectZPC n) : (V.ofTNFVT U).HasPerfectPCC n T

A perfect ZPC strategy gives a perfect PCC strategy of ofTNFVT (lem:zpc-pcc), for an answer bound above the tailored game's answer lengths.

The wrapper's cost, dominated

theorem MIPRE.Repeat.Dom.powX {W X K : ℕ} (e : ℕ) : Dom W X K 1 0 e (X ^ (e * (K + 1)))

theorem MIPRE.Tailored.dom_wrapCoreCost (U : Cost.UniversalMachine) (cT mT eT : ℕ) : ∃ (c : ℕ) (m : ℕ) (e : ℕ), ∀ {ℓ : ℕ} (S : CL.Sampler ℓ) (dec : Cost.Prog) (W X K n Cs T s : ℕ), 1 ≤ X → 10 ^ K ≤ W → s + 1 ≤ X → Cost.esize S.prog ≤ W → Cost.esize dec ≤ W → Cost.esize n ≤ W → S.dim n ≤ W → Cs ≤ W → Repeat.Dom W X K cT mT eT T → Repeat.Dom W X K c m e (Cost.Prog.wrapCoreCost U S dec (fun (x : ℕ) => Cs) K n T s)

The wrapper's explicit cost is dominated: for every domination (cT, mT, eT) of the string's decider's time T, there are c, m, e with wrapCoreCost ≤ c (W + 1)^m X^{e (K + 1)} — the sampler's bound Cs at degree K — once W is above 10^K, Cs, the dimension and the sizes of the index and of the two programs, and X above the input's size. The constants depend on the universal machine alone.

The bound, at n ≥ 2

theorem MIPRE.Tailored.dom_le_pow {n X c m e A lam C : ℕ} (hn : 2 ≤ n) (hlam : 1 ≤ lam) (hX : 1 ≤ X) (hC1 : c + (A + 1) * m ≤ C) (hC2 : 2 * e ≤ C) : c * (n ^ (A * lam) + 1) ^ m * X ^ (e * (lam + 1)) ≤ n ^ (C * lam) * X ^ (C * lam)

The domination at W = n^{A λ}, read as a bound of the shape TimeBoundAt asks for.

theorem MIPRE.Tailored.TailoredVerifier.ofTNFVT_isBounded (U : Cost.UniversalMachine) : ∃ (C : ℕ), ∀ {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam : ℕ), V.IsBounded lam → (V.ofTNFVT U).IsBounded (C * lam)

A λ-bounded tailored verifier is a (C λ)-bounded normal form verifier, for a constant C depending on the universal machine U alone.