The uniform profile constants of conditional soundness

The ordered-edge loss of the complete introspection type graph and the uniform coefficient after restriction and the finite soundness argument. The numbered source theorem (NumberedSoundness.quantumValue_ge_of_errorProfile) absorbs a two-term QLD error profile with them.

Phase 4 of planning/mipco-track.md removed the callback forms of conditional soundness that followed here, which had no consumer; the numbered theorem takes an extraction for its specific restricted strategy instead.

def MIPRE.Introspection.RestrictedSoundness.edgeCount (ℓ : ℕ) : ℝ

Ordered-edge loss in the complete introspection type graph.

Equations

• MIPRE.Introspection.RestrictedSoundness.edgeCount ℓ = ↑(MIPRE.Introspection.TypeGraph.edges MIPRE.QLD.adj (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.X) (MIPRE.QLD.Ty.pauli MIPRE.QLD.Bas.Z) ℓ).card

theorem MIPRE.Introspection.RestrictedSoundness.edgeCount_one_le (ℓ : ℕ) : 1 ≤ edgeCount ℓ

noncomputable def MIPRE.Introspection.RestrictedSoundness.profileCoefficient (ℓ : ℕ) (a b : ℝ) : ℝ

Uniform coefficient after restriction and the finite soundness argument.

Equations

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

theorem MIPRE.Introspection.RestrictedSoundness.profileCoefficient_one_le (ℓ : ℕ) (a b : ℝ) : 1 ≤ profileCoefficient ℓ a b