Execution cost of the canonical Pauli parameters

noncomputable def MIPRE.Introspection.PauliSamplerParameters.cost (c lam n : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.PauliSamplerParameters.prog_runs_cost (c lam n : ℕ) : ∃ time ≤ cost c lam n, (prog c).Runs (Cost.encode (lam, n)) (Cost.encode (parameters c lam n)) time

def MIPRE.Introspection.PauliSamplerParameters.unaryMajorant (v : ℕ) : ℕ

A polynomial upper bound for binary-to-unary conversion.

Equations

• MIPRE.Introspection.PauliSamplerParameters.unaryMajorant v = (v + 2) * ((v + 1) * (4 * v + 14) + 7 * (4 * v + 1) + 8 * v + 90)

theorem MIPRE.Introspection.PauliSamplerParameters.unaryCost_le {x v : ℕ} (hx : x ≤ v) : ClockArithmetic.unaryCost x ≤ unaryMajorant v

def MIPRE.Introspection.PauliSamplerParameters.widthBound (c v : ℕ) : ℕ

Equations

• MIPRE.Introspection.PauliSamplerParameters.widthBound c v = c * (v + 2) + 1

noncomputable def MIPRE.Introspection.PauliSamplerParameters.costMajorant (c v : ℕ) : ℕ

Equations

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

theorem MIPRE.Introspection.PauliSamplerParameters.parameters_le_widthBound {c lam n v : ℕ} (hc : 1 ≤ c) (hu : lam * n ≤ v) : SourceCompiler.fieldBits c lam n ≤ widthBound c v ∧ selectorBits c lam n ≤ widthBound c v ∧ SourceCompiler.registerPower c lam n ≤ widthBound c v

theorem MIPRE.Introspection.PauliSamplerParameters.parameters_size_le {c lam n v : ℕ} (hc : 1 ≤ c) (hu : lam * n ≤ v) : Cost.esize (parameters c lam n) ≤ 6 * widthBound c v + 5

theorem MIPRE.Introspection.PauliSamplerParameters.cost_le_majorant {c lam n v : ℕ} (hc : 1 ≤ c) (hl : lam ≤ v) (hn : n ≤ v) (hu : lam * n ≤ v) : cost c lam n ≤ costMajorant c v

theorem MIPRE.Introspection.PauliSamplerParameters.costMajorant_polyBounded (c : ℕ) : Cost.PolyBounded (costMajorant c)