Actual QLD soundness witnesses in the introspection interface

QLD reads all wrongly formatted Pauli answers as zero. The interface used by introspection instead records the genuine full-register answer effects. Legal Pauli support identifies those effects exactly, including at the zero register.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the Pauli basis test enters as the hypothesis that it is sound in the model of the strategy (QLD.SoundIn ω M), in the shape and at the error qldErr of thm:qld. Its universal constants are those of qldErr in closed form (QLD.exists_qldErr_le), a fact about that function alone, so they are fixed once for every model. The ancilla of the conclusion is an abstract ancilla model, which needs no numbering.

def MIPRE.Introspection.RestrictedSoundness.PauliSupported {F : Type} [Fintype F] {m d : ℕ} {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : QLD.Question F m → POVMIn (QLD.Answer F m d) R) : Prop

Only the two full-register measurements require legal support.

Equations

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

theorem MIPRE.Introspection.RestrictedSoundness.rdPauliVec_op_of_supported {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (P : QLD.Question F m → POVMIn (QLD.Answer F m d) R) (hP : PauliSupported P) (W : QLD.Bas) (x : QLD.Honest.Register F m) : (POVMIn.map QLD.rdPauliVec (P (QLD.Question.pauli W))).op x = (P (QLD.Question.pauli W)).op (QLD.Answer.pauliAns x)

def MIPRE.Introspection.RestrictedSoundness.ParsedPauliSupported {F : Type} [Fintype F] {m d : ℕ} {V : Type u_1} {A : Type u_2} {J : Type u_3} {R : Type u_4} [Fintype V] [Fintype A] [Fintype J] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {ℓ : ℕ} (M : QuestionType QLD.Ty ℓ × (J → ZMod 2) → POVMIn (ParsedAnswer V A (QLD.Answer F m d)) R) : Prop

The stronger parsed support property furnished by the executable decoder.

Equations

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

theorem MIPRE.Introspection.RestrictedSoundness.completePauliPOVM_invalid_of_supported {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {V : Type u_1} {A : Type u_2} {R : Type u_3} [Fintype V] [Fintype A] [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (M : POVMIn (ParsedAnswer V A (QLD.Answer F m d)) R) (hM : ∀ (a : ParsedAnswer V A (QLD.Answer F m d)), M.op a ≠ 0 → ∃ (x : (Fin m → Bool) → F), a = ParsedAnswer.pauli (QLD.Answer.pauliAns x)) (W : QLD.Bas) (a : QLD.Answer F m d) (ha : (QLD.Question.pauli W).fmtOk a = false) : (completePauliPOVM (QLD.Answer.val 0) M).op a = 0

Scalar completion has no malformed mass when the parsed measurement only has genuine full-register outcomes.

noncomputable def MIPRE.Introspection.RestrictedSoundness.qldCoefficient : ℝ

Fix the universal QLD constants once, before any verifier parameters: those of the closed form of qldErr (QLD.exists_qldErr_le).

Equations

• MIPRE.Introspection.RestrictedSoundness.qldCoefficient = MIPRE.QLD.exists_qldErr_le.choose

noncomputable def MIPRE.Introspection.RestrictedSoundness.qldExponent : ℝ

Equations

• MIPRE.Introspection.RestrictedSoundness.qldExponent = MIPRE.Introspection.RestrictedSoundness.qldExponent._proof_1.choose

theorem MIPRE.Introspection.RestrictedSoundness.qldCoefficient_one_le : 1 ≤ qldCoefficient

theorem MIPRE.Introspection.RestrictedSoundness.qldExponent_pos : 0 < qldExponent

theorem MIPRE.Introspection.RestrictedSoundness.qldExponent_lt_one : qldExponent < 1

theorem MIPRE.Introspection.RestrictedSoundness.qldErr_le_errShape (ε : ℝ) (m d q : ℕ) (hε : 0 ≤ ε) (hm : 1 ≤ m) (hd : 1 ≤ d) (hq : 2 ≤ q) : QLD.qldErr (min ε 1) m d q ≤ QLD.errShape qldCoefficient qldExponent ε m d q

def MIPRE.Introspection.RestrictedSoundness.FieldExtraction.ofQLD {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {hm : m ∣ Fintype.card F} {R : M.ProjStrat (QLD.qldGame hm)} {δ : ℝ} (E : QLD.Extraction M hm R δ) (hA : PauliSupported R.PA) (hB : PauliSupported R.PB) : FieldExtraction M hm R δ

The Pauli basis test's conclusion, read at the genuine full-register answers.

Equations

• MIPRE.Introspection.RestrictedSoundness.FieldExtraction.ofQLD E hA hB = { N := E.N, Φ := E.Φ, state_error := ⋯, X_error := ⋯, Z_error := ⋯ }

theorem MIPRE.Introspection.RestrictedSoundness.fieldExtraction_exists {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {ω : ValueModel} {M : BipartiteModel 𝒞 𝒜 ℬ} (hQ : QLD.SoundIn ω M) (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (R : M.ProjStrat (QLD.qldGame hm)) (hA : PauliSupported R.PA) (hB : PauliSupported R.PB) {ε : ℝ} (hε : 0 ≤ ε) (hfail : 1 - R.value ≤ ε) : ∃ (w : FieldExtraction M hm R (QLD.errShape qldCoefficient qldExponent ε m d (Fintype.card F))), ω.DominatesPOVM w.N.N

The Pauli basis test in the model of the strategy yields the genuine-answer extraction, at the universal constants, for every strategy supported on correctly formatted Pauli answers; its ancilla model is dominated by the value model.

theorem MIPRE.Introspection.RestrictedSoundness.degreeOne_fieldExtraction_exists {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {ω : ValueModel} {M : BipartiteModel 𝒞 𝒜 ℬ} (hQ : QLD.SoundIn ω M) (hm : m ∣ Fintype.card F) (R : M.ProjStrat (QLD.qldGame hm)) (hA : PauliSupported R.PA) (hB : PauliSupported R.PB) {ε : ℝ} (hε : 0 ≤ ε) (hfail : 1 - R.value ≤ ε) : ∃ (w : FieldExtraction M hm R (PauliErrorParameters.qldError qldCoefficient qldExponent (↑m) (↑(Fintype.card F)) ε)), ω.DominatesPOVM w.N.N

The degree-one specialization has exactly the error used by the canonical parameter estimates, with no change to the QLD exponent or tail.

theorem MIPRE.Introspection.RestrictedSoundness.exists_extraction {F : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m d : ℕ} [NeZero m] {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {t ℓ : ℕ} {A : Type} [Fintype A] [Nonempty A] {ω : ValueModel} {M : BipartiteModel 𝒞 𝒜 ℬ} (hQ : QLD.SoundIn ω M) (hm : m ∣ Fintype.card F) (hd : 1 ≤ d) (b : Module.Basis (Fin t) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) (L : Bool → CL.CLFun (ZMod 2) (BinaryComplete.Coord m t) ℓ) (D : BinaryComplete.Seed m t → BinaryComplete.Seed m t → A → A → Bool) (S : M.ProjStrat (PauliRestriction.fullGame hm b L (BinaryComplete.project b) D)) (hA : ParsedPauliSupported S.PA) (hB : ParsedPauliSupported S.PB) {ε : ℝ} (hε : 0 ≤ ε) (hfail : 1 - S.value ≤ ε) : ∃ (E : Extraction M hm b (restriction hm b L D S) (QLD.errShape qldCoefficient qldExponent (edgeCount ℓ * ε) m d (Fintype.card F))), ω.DominatesPOVM E.N.N

The extraction for the restricted strategy (lem:intro-pauli-extraction). In a model where the Pauli basis test is sound with ω, let a projective strategy of the binary parsed introspection game fail with probability at most ε, and let its two full-register Pauli measurements have outcomes only at full-register answers. Then its restriction to the Pauli basis game has an extraction in binary coordinates at the error δ_qld(Nε, m, d, q) of the universal constants, with N the number of ordered edges of the typed graph, and its ancilla model is dominated by ω: the restriction fails with probability at most Nε (PauliRestriction.strategy_failure_le), keeps the support (completePauliPOVM_invalid_of_supported), so the test applies at the genuine answers (fieldExtraction_exists), and the register is relabelled as qubits along a self-dual basis (FieldExtraction.toBinary).