Canonical parameters for the executable Pauli sampler

The selector width, field width and point dimension are computed from the same canonical parameters as the source compiler. The program returns unary parameters, which are the input format of the uniform field algorithms.

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

Equations

• MIPRE.Introspection.PauliSamplerParameters.selectorBits c lam n = (c * MIPRE.Introspection.SourceCompiler.canonicalLog lam n + 1).size - 1

theorem MIPRE.Introspection.PauliSamplerParameters.registerPower_eq (c lam n : ℕ) : SourceCompiler.registerPower c lam n = 2 ^ selectorBits c lam n

theorem MIPRE.Introspection.PauliSamplerParameters.fieldBits_pos (c lam n : ℕ) : 1 ≤ SourceCompiler.fieldBits c lam n

instance MIPRE.Introspection.PauliSamplerParameters.fieldBits_neZero (c lam n : ℕ) : NeZero (SourceCompiler.fieldBits c lam n)

theorem MIPRE.Introspection.PauliSamplerParameters.fieldBits_odd {c : ℕ} (hc : Even c) (lam n : ℕ) : Odd (SourceCompiler.fieldBits c lam n)

theorem MIPRE.Introspection.PauliSamplerParameters.registerPower_pos (c lam n : ℕ) : 1 ≤ SourceCompiler.registerPower c lam n

theorem MIPRE.Introspection.PauliSamplerParameters.registerPower_le (c lam n : ℕ) : SourceCompiler.registerPower c lam n ≤ c * SourceCompiler.canonicalLog lam n + 1

theorem MIPRE.Introspection.PauliSamplerParameters.canonicalLog_lt_registerPower {c : ℕ} (hc : 2 ≤ c) (lam n : ℕ) : SourceCompiler.canonicalLog lam n < SourceCompiler.registerPower c lam n

theorem MIPRE.Introspection.PauliSamplerParameters.fieldBits_le (c lam n : ℕ) : SourceCompiler.fieldBits c lam n ≤ c * SourceCompiler.canonicalLog lam n + 1

theorem MIPRE.Introspection.PauliSamplerParameters.selectorBits_le_fieldBits {c : ℕ} (hc : 1 ≤ c) (lam n : ℕ) : selectorBits c lam n ≤ SourceCompiler.fieldBits c lam n

theorem MIPRE.Introspection.PauliSamplerParameters.four_le_registerBits {c : ℕ} (hc : 2 ≤ c) (lam n : ℕ) : 4 ≤ SourceCompiler.registerBits c lam n

theorem MIPRE.Introspection.PauliSamplerParameters.originalBound_three_le_registerBits {c : ℕ} (hc : 2 ≤ c) (lam n : ℕ) : 3 * SourceCompiler.originalBound lam n ≤ SourceCompiler.registerBits c lam n

@[reducible, inline]

abbrev MIPRE.Introspection.PauliSamplerParameters.Parameters : Type

Equations

• MIPRE.Introspection.PauliSamplerParameters.Parameters = (MIPRE.Cost.Unary × MIPRE.Cost.Unary × MIPRE.Cost.Unary)

def MIPRE.Introspection.PauliSamplerParameters.parameters (c lam n : ℕ) : Parameters

Equations

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

noncomputable def MIPRE.Introspection.PauliSamplerParameters.powerInput : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.Unary) Cost.Data

Retain the selector width while its power of two is computed.

Equations

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

noncomputable def MIPRE.Introspection.PauliSamplerParameters.powerPost : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

Equations

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

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

Equations

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

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

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