Introspection, as a hypothesis

Blueprint thm:introspection (paper introspection.tex, thm:introspection; ledger nodes 1.2, 1.2.3.8), stated as the data the theorem provides: the structure Introspection ℓ. Its inhabitation is the theorem — the rigidity argument of the paper's Section 8 through the Pauli basis test thm:qld — and nothing here proves it. The composition MIPRE.GapCompression.ofPipeline consumes an instance at ℓ = 7.

The reading of the paper's statement in the vocabulary of MIPRE.Verifier:

• ComputeIntroVerifier takes (𝒱, λ, ℓ); with ℓ a parameter of the structure, the procedure is a polynomial-time function compute of ((S̄, D̄), λ) returning the program of the introspective decider, and the introspective sampler 𝒮^intro_λ depends only on λ (paper lem:intro-sampler-complexity), with its program computable from λ (samplerProg). On every input, well-formed or not, the output is a 5-level normal form verifier (output).
• The ambient complexity clauses hold for every input and every index: TIME_𝒮(n) ≤ (λn + 1)^C, TIME_𝒟(n) ≤ 2^{(λn + 1)^C} and |𝒟^intro| ≤ C(λ+1)^C. The polynomial exponent is an explicit adaptation of the paper's absolute-time bound 2^{Cλn}: IsBounded λ permits input-size degree λ, which introduces a quadratic exponent in λ on legal answers of length (2^n)^λ. The running times carry the fixed degree C in the size of the output verifier's input, and the decider rejects every answer longer than its bound (Budget.B). Answer reduction consumes the same polynomial-exponent budget, and the proved compression composition still has polynomial output bounds. The introspective decider keeps 𝒟 within its own description only up to λ bits (paper lem:intro-decider-complexity), which is why the size bound does not depend on the input.
• For a λ-bounded ℓ-level input: a value-1 PCC strategy for 𝒱_{2^n} gives one for 𝒱^intro_n (completeness), and val*(𝒱^intro_n) > 1 - ε gives val*(𝒱_{2^n}) ≥ 1 - δ(ε, n) with δ(ε, n) = a((λn)^a ε^b + (λn)^{-b}) (soundness), the constants a, b depending on ℓ only. Soundness requires 1 ≤ n, as in the construction's indexing convention: the original input is bounded only at 2 ≤ 2^n. At zero the displayed error would vanish and assert an unintended exact conclusion. The paper has a > 0; a ≥ 1 is assumed here, which only weakens the clause and is what the proof of thm:compression uses.

Answer alphabets follow MIPRE.GapCompression: 𝒱_{2^n} is read with answers of length at most (2^n)^λ, and 𝒱^intro_n with answers of length at most its time bound, beyond which its decider rejects.

@[reducible, inline]

abbrev MIPRE.Introspection.ansBound (C lam n : ℕ) : ℕ

The answer bound of the introspective verifier at level λ and index n: its decider's running-time coefficient 2^{(λn + 1)^C}.

Equations

• MIPRE.Introspection.ansBound C lam n = 2 ^ (lam * n + 1) ^ C

def MIPRE.Introspection.budget (C lam n : ℕ) : Budget

The budget of the introspective verifier at level λ and index n: sampler within (λn + 1)^C, questions of dimension at most (λn + 1)^C, decider within 2^{(λn + 1)^C}, both at degree C, and no answer longer than 2^{(λn + 1)^C} accepted.

Equations

• MIPRE.Introspection.budget C lam n = { S := (lam * n + 1) ^ C, d := (lam * n + 1) ^ C, D := MIPRE.Introspection.ansBound C lam n, k := C, B := MIPRE.Introspection.ansBound C lam n }

noncomputable def MIPRE.Introspection.delta (a b : ℝ) (lam n : ℕ) (ε : ℝ) : ℝ

The soundness loss δ(ε, n) = a((λn)^a ε^b + (λn)^{-b}).

Equations

• MIPRE.Introspection.delta a b lam n ε = a * ((↑lam * ↑n) ^ a * ε ^ b + (↑lam * ↑n) ^ (-b))

theorem MIPRE.Introspection.delta_zero_index (a b : ℝ) (lam : ℕ) (ε : ℝ) (ha : a ≠ 0) (hb : b ≠ 0) : delta a b lam 0 ε = 0

At index zero the displayed error vanishes, so soundness cannot use this index.

theorem MIPRE.Introspection.two_le_exp_index_iff (n : ℕ) : 2 ≤ 2 ^ n ↔ 1 ≤ n

Positive introspection indices are exactly the range where the original budget applies.

structure MIPRE.Introspection (ℓ : ℕ) : Type

Introspection (blueprint thm:introspection) for ℓ-level inputs: the data of the procedure ComputeIntroVerifier together with the guarantees of the theorem. An instance of this structure is the theorem.

• a : ℝ

  The constant a of the soundness loss, normalized to a ≥ 1.

• b : ℝ

  The exponent b of the soundness loss, 0 < b ≤ 1.

• one_le_a : 1 ≤ self.a
• b_pos : 0 < self.b
• b_le_one : self.b ≤ 1
• C : ℕ

  The complexity constant C_intro.

• sampler : ℕ → CL.Sampler 5

  The introspective sampler 𝒮^intro_λ, depending only on λ.

• samplerProg : Cost.PolyTimeFun ℕ Cost.Prog

  Its program, computable from λ in polynomial time.

• samplerProg_eq (lam : ℕ) : self.samplerProg.toFun lam = (self.sampler lam).prog
• compute : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × ℕ) Cost.Prog

  ComputeIntroVerifier: from the programs of a verifier and λ, the program of the introspective decider, in polynomial time.

• output : Cost.Prog × Cost.Prog → ℕ → Verifier 5

  The output on any input is a 5-level normal form verifier, with the introspective sampler and the introspective decider.

• output_sampler (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).sampler = self.sampler lam
• output_decider (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).decider.prog = self.compute.toFun (V, lam)
• within (V : Cost.Prog × Cost.Prog) (lam n : ℕ) : (self.output V lam).Within n (budget self.C lam n)

  The complexity clauses, for every input and index.

• decider_size (V : Cost.Prog × Cost.Prog) (lam : ℕ) : (self.output V lam).decider.size ≤ self.C * (lam + 1) ^ self.C

  |𝒟^intro| ≤ C λ^C, for every input.

• completeness (V : Verifier ℓ) (lam n : ℕ) : V.IsBounded lam → V.HasPerfectPCC (2 ^ n) ((2 ^ n) ^ lam) → (self.output (V.sampler.prog, V.decider.prog) lam).HasPerfectPCC n (ansBound self.C lam n)

  Completeness. For a λ-bounded input: a value-1 PCC strategy for 𝒱_{2^n} gives one for 𝒱^intro_n.

• soundness (V : Verifier ℓ) (lam n : ℕ) (ε : ℝ) : V.IsBounded lam → 1 ≤ n → 0 < ε → 1 - ε < (self.output (V.sampler.prog, V.decider.prog) lam).valStar n (ansBound self.C lam n) → 1 - delta self.a self.b lam n ε ≤ V.valStar (2 ^ n) ((2 ^ n) ^ lam)

  Soundness. For a λ-bounded input and n ≥ 1: val*(𝒱^intro_n) > 1 - ε gives val*(𝒱_{2^n}) ≥ 1 - δ(ε, n).

def MIPRE.Introspection.SoundIn {ℓ : ℕ} (I : Introspection ℓ) (ω : ValueModel) : Prop

The soundness clause of introspection in a value model: the field soundness with the value val* replaced by the model's. The field is the tensor-product case (Introspection.soundIn_tensor); for the compiler of the main theorem, the commuting-operator case follows from the soundness of the Pauli basis test in the commuting-operator model (Introspection.seven_soundIn_commuting, Phase 4 of planning/mipco-track.md).

Equations

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

theorem MIPRE.Introspection.soundIn_tensor {ℓ : ℕ} (I : Introspection ℓ) : I.SoundIn ValueModel.tensor

The soundness clause of introspection is soundness in the tensor-product model.