The executable five-level introspection sampler

The canonical Pauli sampler extends to all introspection types and is then detyped along the actual type graph. The program is uniformly compiled from the binary boundedness parameter. Its positive-index budget includes both routers and the graph register; the final verifier handles zero separately.

@[reducible, inline]

abbrev MIPRE.Introspection.PauliSampler.graph (ℓ : ℕ) (t u : QuestionType QLD.Ty ℓ) : Prop

Equations

• MIPRE.Introspection.PauliSampler.graph ℓ = MIPRE.Introspection.TypeGraph.Adj MIPRE.QLD.adj (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.X) (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.Z)

noncomputable def MIPRE.Introspection.PauliSampler.fullSampler (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam : ℕ) : CL.Sampler 5

Equations

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

theorem MIPRE.Introspection.PauliSampler.fullSampler_dim (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam n : ℕ) : (fullSampler c hc he ℓ lam).dim n = 4 * (Fintype.card QLD.Ty + 2 * ℓ + 6) + dimension c lam n

noncomputable def MIPRE.Introspection.PauliSampler.fullCompiler (c ℓ : ℕ) : Cost.PolyTimeFun ℕ Cost.Prog

Equations

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

theorem MIPRE.Introspection.PauliSampler.fullCompiler_apply (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam : ℕ) : (fullCompiler c ℓ).toFun lam = (fullSampler c hc he ℓ lam).prog

noncomputable def MIPRE.Introspection.PauliSampler.fullDegree (ℓ : ℕ) : ℕ

Equations

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

noncomputable def MIPRE.Introspection.PauliSampler.fullCoefficient (c ℓ lam n : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.PauliSampler.fullSampler_timeBoundAt (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ lam n : ℕ) : (fullSampler c hc he ℓ lam).TimeBoundAt n (fullCoefficient c ℓ lam n) (fullDegree ℓ)

theorem MIPRE.Introspection.PauliSampler.routeCost_eval_mono (r : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (p : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (k : ℕ) {B B' x x' : ℕ} (hB : B ≤ B') (hx : x ≤ x') : Polynomial.eval x (Cost.Prog.routeCost r p B k) ≤ Polynomial.eval x' (Cost.Prog.routeCost r p B' k)

theorem MIPRE.Introspection.PauliSampler.routeCost_polyBounded (r : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)) (p : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data) (k : ℕ) {B : ℕ → ℕ} (hB : Cost.PolyBounded B) : Cost.PolyBounded fun (v : ℕ) => Polynomial.eval (4 * v + 3) (Cost.Prog.routeCost r p (B v) k)

noncomputable def MIPRE.Introspection.PauliSampler.typedMajorant (c v : ℕ) : ℕ

Equations

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

noncomputable def MIPRE.Introspection.PauliSampler.fullMajorant (c ℓ v : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.PauliSampler.fullMajorant_polyBounded (c ℓ : ℕ) : Cost.PolyBounded (fullMajorant c ℓ)

theorem MIPRE.Introspection.PauliSampler.sum_coeff_eq_eval_one (P : Polynomial ℕ) : ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i = Polynomial.eval 1 P

theorem MIPRE.Introspection.PauliSampler.fullCoefficient_le_majorant {c ℓ lam n v : ℕ} (hc : 1 ≤ c) (hl : lam ≤ v) (hn : n ≤ v) (hu : lam * n ≤ v) : fullCoefficient c ℓ lam n ≤ fullMajorant c ℓ v

theorem MIPRE.Introspection.PauliSampler.fullSampler_uniform_bound (c : ℕ) (hc : 1 ≤ c) (he : Even c) (ℓ : ℕ) : ∃ (C : ℕ), ∀ (lam n : ℕ), 1 ≤ lam → 1 ≤ n → (fullSampler c hc he ℓ lam).TimeBoundAt n ((lam * n + 1) ^ C) C ∧ (fullSampler c hc he ℓ lam).dim n ≤ (lam * n + 1) ^ C

Both routers preserve the single uniform positive-index budget.