Canonical parameters absorb the actual QLD error tails

At degree one, the QLD loss is a*m^a*(ε^b+q^(-b)+2^(-b*m)). The field size and dyadic point dimension chosen by the executable sampler make both residual terms polynomially small in λ*n, with uniform constants.

noncomputable def MIPRE.Introspection.PauliErrorParameters.qldError (a b m q ε : ℝ) : ℝ

The degree-one specialization of the external QLD error profile.

Equations

• MIPRE.Introspection.PauliErrorParameters.qldError a b m q ε = a * m ^ a * (ε ^ b + q ^ (-b) + 2 ^ (-b * m))

noncomputable def MIPRE.Introspection.PauliErrorParameters.profileCoefficient (a c : ℝ) : ℝ

A coefficient covering the dimension factor and both residual tails.

Equations

• MIPRE.Introspection.PauliErrorParameters.profileCoefficient a c = max 1 (max a (2 * a * (c + 1) ^ a))

theorem MIPRE.Introspection.PauliErrorParameters.profileCoefficient_one_le (a c : ℝ) : 1 ≤ profileCoefficient a c

theorem MIPRE.Introspection.PauliErrorParameters.qldError_le_profile {a b c x m q ε : ℝ} (ha : 1 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) (hc : 1 ≤ c) (hcb : 2 * a + 2 ≤ c * b) (hx : 1 ≤ x) (hm : 0 ≤ m) (hε : 0 ≤ ε) (hmx : m ≤ (c + 1) * x) (hqx : x ^ c ≤ q) (h2x : x ^ c ≤ 2 ^ (2 * m)) : qldError a b m q ε ≤ errorProfile (profileCoefficient a c) b x ε

The two QLD tails are absorbed from elementary lower bounds on q and 2^(2m). These bounds are discharged for the executable parameters below.

theorem MIPRE.Introspection.PauliErrorParameters.canonical_field_lower (c lam n : ℕ) (hx : 2 ≤ lam * n) : (lam * n) ^ c ≤ 2 ^ SourceCompiler.fieldBits c lam n

The executable field has at least (λ*n)^c elements.

theorem MIPRE.Introspection.PauliErrorParameters.canonical_register_lower (c lam n : ℕ) (hx : 2 ≤ lam * n) : c * (lam * n) ≤ 2 * SourceCompiler.registerPower c lam n

The lower dyadic rounding of c*λ*n+1 loses at most a factor of two.

theorem MIPRE.Introspection.PauliErrorParameters.canonical_exponential_lower (c lam n : ℕ) (hx : 2 ≤ lam * n) : (lam * n) ^ c ≤ 2 ^ (2 * SourceCompiler.registerPower c lam n)

The actual 2^(-b*m) tail is controlled by taking half the power of this inequality; the exponent is not replaced by 2^(-2*b*m).

theorem MIPRE.Introspection.PauliErrorParameters.canonical_register_upper (c lam n : ℕ) (hx : 2 ≤ lam * n) : SourceCompiler.registerPower c lam n ≤ (c + 1) * (lam * n)

The canonical point dimension has a fixed linear bound.

theorem MIPRE.Introspection.PauliErrorParameters.canonical_qldError_le_profile {a b : ℝ} (ha : 1 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) (c : ℕ) (hc : 2 ≤ c) (hcb : 2 * a + 2 ≤ ↑c * b) (lam n : ℕ) (hx : 2 ≤ lam * n) (ε : ℝ) (hε : 0 ≤ ε) : qldError a b (↑(SourceCompiler.registerPower c lam n)) (↑(2 ^ SourceCompiler.fieldBits c lam n)) ε ≤ errorProfile (profileCoefficient a ↑c) b (↑lam * ↑n) ε

The QLD profile for the parameters computed by the sampler has the uniform introspection shape, including both residual terms.

theorem MIPRE.Introspection.PauliErrorParameters.exists_even_constant (a : ℝ) {b : ℝ} (hb0 : 0 < b) : ∃ (c : ℕ), 2 ≤ c ∧ Even c ∧ 2 * a + 2 ≤ ↑c * b

The executable sampler can use one even constant meeting the required tail exponent, independently of the verifier and its index.