The canonical index-dependent executable Pauli sampler

The field, selector, basis and question dimension are the canonical index-dependent choices. The sampler program computes these parameters from the index and calls the uniform query router. Its semantic family uses the effective Shoup self-dual basis, and all query contracts concern the actual numbered binary vectors.

This is the canonical positive-index component. The final introspection compiler must wrap the detyped sampler with a zero-dimensional fallback at zero index (and zero boundedness parameter) to respect its all-index budget.

theorem MIPRE.Introspection.PauliSampler.registerPower_neZero (c lam n : ℕ) : NeZero (SourceCompiler.registerPower c lam n)

def MIPRE.Introspection.PauliSampler.dimension (c lam n : ℕ) : ℕ

Equations

• MIPRE.Introspection.PauliSampler.dimension c lam n = (3 * MIPRE.Introspection.SourceCompiler.registerPower c lam n + 3) * MIPRE.Introspection.SourceCompiler.fieldBits c lam n

noncomputable def MIPRE.Introspection.PauliSampler.presentation (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (T : QLD.Ty) : CL.CLFun CL.𝔽₂ (Fin (dimension c lam n)) 3

Equations

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

theorem MIPRE.Introspection.PauliSampler.presentation_exactlyOn (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (T : QLD.Ty) : (presentation c hc he lam n T).ExactlyOn Finset.univ

noncomputable def MIPRE.Introspection.PauliSampler.route : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Route the index to parameter generation and retain the complete raw query.

Equations

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

noncomputable def MIPRE.Introspection.PauliSampler.post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

• MIPRE.Introspection.PauliSampler.post = MIPRE.Cost.PolyTimeFun.treePair.ap₂ MIPRE.Cost.PolyTimeFun.snd MIPRE.Cost.PolyTimeFun.fst

noncomputable def MIPRE.Introspection.PauliSampler.prog (c lam : ℕ) : Cost.Prog

Equations

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

theorem MIPRE.Introspection.PauliSampler.prog_closed (c lam : ℕ) : Cost.Prog.WellScoped 1 (prog c lam)

theorem MIPRE.Introspection.PauliSampler.prog_runs (c lam n : ℕ) (d : Cost.Data) : ∃ (time : ℕ), (prog c lam).Runs ((Cost.encode n).cons d) (QLD.PauliCL.SamplerProgram.query.toFun (PauliSamplerParameters.parameters c lam n, d)) time

theorem MIPRE.Introspection.PauliSampler.prog_halts (c lam n : ℕ) (d : Cost.Data) : Cost.Halts (prog c lam) ((Cost.encode n).cons d)

theorem MIPRE.Introspection.PauliSampler.query_marginal (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (w : Player) (T : QLD.Ty) (r : ℕ) (z : Cost.BitStr) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (hz : List.length z = dimension c lam n) : QLD.PauliCL.SamplerProgram.query.toFun (PauliSamplerParameters.parameters c lam n, Cost.encode (CL.TypedSampler.Query.atType T (CL.Sampler.Query.marginal w r z))) = Cost.encode (CL.toBits ((CL.CLFun.truncate r (presentation c hc he lam n T)).eval (CL.ofBits (dimension c lam n) z)))

theorem MIPRE.Introspection.PauliSampler.query_linear (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (w : Player) (T : QLD.Ty) (r : ℕ) (u y : Cost.BitStr) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) (hu : List.length u = dimension c lam n) (hy : List.length y = dimension c lam n) : QLD.PauliCL.SamplerProgram.query.toFun (PauliSamplerParameters.parameters c lam n, Cost.encode (CL.TypedSampler.Query.atType T (CL.Sampler.Query.linear w r u y))) = Cost.encode (CL.toBits (((presentation c hc he lam n T).mapOfPrefix (r - 1) (CL.ofBits (dimension c lam n) u)) (CL.ofBits (dimension c lam n) y)))

theorem MIPRE.Introspection.PauliSampler.query_factor (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (w : Player) (T : QLD.Ty) (r : ℕ) (u : Cost.BitStr) (hr1 : 1 ≤ r) (hr3 : r ≤ 3) : QLD.PauliCL.SamplerProgram.query.toFun (PauliSamplerParameters.parameters c lam n, Cost.encode (CL.TypedSampler.Query.atType T (CL.Sampler.Query.factor w r u))) = Cost.encode (CL.indicatorBits ((presentation c hc he lam n T).factorOfPrefix (r - 1) (CL.ofBits (dimension c lam n) u)))

noncomputable def MIPRE.Introspection.PauliSampler.sampler (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam : ℕ) : CL.TypedSampler 3 QLD.Ty

The actual uniform three-level Pauli sampler at canonical parameters.

Equations

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

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

The compiler copies only the binary encoding of the boundedness parameter.

Equations

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