Source soundness with the actual finite register numbering

Coordinate relabeling is performed on the intrinsic quotient predicate. Dual answers are only canonicalized afterwards in binary coordinates. Thus no equivariance of the chosen canonical complement is used.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the strategy is a projective strategy of any model M, every transport keeps it in M, and the Pauli basis test enters as its soundness in M (QLD.SoundIn ω M); the value is that of the value model ω.

theorem MIPRE.Introspection.NumberedSoundness.reindexedGame_eq {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) : AuxiliaryQuotient.reindexedGame e QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (QLD.PauliCL.ExplicitSeed.binaryPresentation χ b) L (NumberedComplete.project e b) D (ExplicitGame.pauliCheck hm π b) = BinaryComplete.explicitQuotientGame (SourceReindex.family e L) (SourceReindex.decider e D) hm b χ π

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.NumberedSoundness.coordinateStrategy {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) : M.ProjStrat (BinaryComplete.explicitQuotientGame (SourceReindex.family e L) (SourceReindex.decider e D) hm b χ π)

Relabel all answer coordinates, in the same model.

Equations

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

theorem MIPRE.Introspection.NumberedSoundness.coordinateStrategy_failure_le {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) {ε : ℝ} (hS : 1 - S.value ≤ ε) : 1 - (coordinateStrategy e L D hm b χ π S).value ≤ ε

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.NumberedSoundness.explicitStrategy {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) : M.ProjStrat (ExplicitGame.game hm χ π b (SourceReindex.family e L) (BinaryComplete.project b) (SourceReindex.decider e D))

Decode quotient duals in binary coordinates.

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.NumberedSoundness.legacyStrategy {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) : M.ProjStrat (PauliRestriction.fullGame hm b (SourceReindex.family e L) (BinaryComplete.project b) (SourceReindex.decider e D))

Undo the explicit seed selector after decoding the quotient duals.

Equations

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

theorem MIPRE.Introspection.NumberedSoundness.legacyStrategy_failure_le {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) {ε : ℝ} (hS : 1 - S.value ≤ ε) : 1 - (legacyStrategy e L D hm b χ π S).value ≤ ε

theorem MIPRE.Introspection.NumberedSoundness.legacyStrategy_supported_A {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hS : RestrictedSoundness.ParsedPauliSupported S.PA) : RestrictedSoundness.ParsedPauliSupported (legacyStrategy e L D hm b χ π S).PA

theorem MIPRE.Introspection.NumberedSoundness.legacyStrategy_supported_B {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hS : RestrictedSoundness.ParsedPauliSupported S.PB) : RestrictedSoundness.ParsedPauliSupported (legacyStrategy e L D hm b χ π S).PB

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.NumberedSoundness.qldStrategy {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) : M.ProjStrat (QLD.qldGame hm)

The precise actual QLD strategy used by the numbered source-game theorem.

Equations

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

theorem MIPRE.Introspection.NumberedSoundness.qldStrategy_supported_A {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hS : RestrictedSoundness.ParsedPauliSupported S.PA) : RestrictedSoundness.PauliSupported (qldStrategy e L D hm b χ π S).PA

theorem MIPRE.Introspection.NumberedSoundness.qldStrategy_supported_B {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hS : RestrictedSoundness.ParsedPauliSupported S.PB) : RestrictedSoundness.PauliSupported (qldStrategy e L D hm b χ π S).PB

theorem MIPRE.Introspection.NumberedSoundness.quantumValue_ge_of_extraction {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (ω : ValueModel) (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hb : LowDegree.IsSelfDualBasis b) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) {ε δ : ℝ} (hδ : 0 ≤ δ) (hS : 1 - S.value ≤ ε) (w : RestrictedSoundness.FieldExtraction M hm (qldStrategy e L D hm b χ π S) δ) (hω : ω.DominatesPOVM w.N.N) : 1 - validSoundnessCoefficient ℓ (RestrictedSoundness.edgeCount ℓ) * iteratedRoot (6 * ℓ + 2) (max ε δ) ≤ ω.val (Honest.sourceGame L D)

A witness about the actual restricted strategy gives the source bound in the original finite coordinates, with no coordinate or quotient penalty, in every value model dominating the witness's ancilla model.

theorem MIPRE.Introspection.NumberedSoundness.quantumValue_ge_of_errorProfile {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (ω : ValueModel) (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hb : LowDegree.IsSelfDualBasis b) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) {a β x ε : ℝ} (ha : 1 ≤ a) (hβ0 : 0 < β) (hβ1 : β ≤ 1) (hx : 1 ≤ x) (hε : 0 ≤ ε) (hS : 1 - S.value ≤ ε) (w : RestrictedSoundness.FieldExtraction M hm (qldStrategy e L D hm b χ π S) (errorProfile a β x (RestrictedSoundness.edgeCount ℓ * ε))) (hω : ω.DominatesPOVM w.N.N) : 1 - errorProfile (RestrictedSoundness.profileCoefficient ℓ a β) (β * rootExponent (6 * ℓ + 2)) x ε ≤ ω.val (Honest.sourceGame L D)

Uniform profile absorption only needs a witness for this restriction, rather than an extraction hypothesis quantified over arbitrary strategies.

theorem MIPRE.Introspection.NumberedSoundness.qldStrategy_failure_le {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) {ε : ℝ} (hS : 1 - S.value ≤ ε) : 1 - (qldStrategy e L D hm b χ π S).value ≤ RestrictedSoundness.edgeCount ℓ * ε

theorem MIPRE.Introspection.NumberedSoundness.quantumValue_ge_of_qld {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} {ω : ValueModel} (hQ : QLD.SoundIn ω M) (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hd : 1 ≤ d) (hb : LowDegree.IsSelfDualBasis b) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (hA : RestrictedSoundness.ParsedPauliSupported S.PA) (hB : RestrictedSoundness.ParsedPauliSupported S.PB) {ε : ℝ} (hε : 0 ≤ ε) (hS : 1 - S.value ≤ ε) : 1 - validSoundnessCoefficient ℓ (RestrictedSoundness.edgeCount ℓ) * iteratedRoot (6 * ℓ + 2) (max ε (QLD.errShape RestrictedSoundness.qldCoefficient RestrictedSoundness.qldExponent (RestrictedSoundness.edgeCount ℓ * ε) m d (Fintype.card F))) ≤ ω.val (Honest.sourceGame L D)

The Pauli basis test, sound in the model of the strategy, supplies the extraction witness; no external extraction hypothesis remains. Only decoder-enforced Pauli support is used.

theorem MIPRE.Introspection.NumberedSoundness.canonical_neZero (c lam n : ℕ) : NeZero (SourceCompiler.registerPower c lam n)

theorem MIPRE.Introspection.NumberedSoundness.canonical_quantumValue_ge {F A I : Type} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Nonempty A] [Fintype I] [DecidableEq I] {ℓ : ℕ} {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] {M : BipartiteModel 𝒞 𝒜 ℬ} (c lam n : ℕ) (hc : 2 ≤ c) (hcb : 2 * RestrictedSoundness.qldCoefficient + 2 ≤ ↑c * RestrictedSoundness.qldExponent) (hx : 2 ≤ lam * n) (hq : Fintype.card F = 2 ^ SourceCompiler.fieldBits c lam n) (hm : SourceCompiler.registerPower c lam n ∣ Fintype.card F) (b : Module.Basis (Fin (SourceCompiler.fieldBits c lam n)) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) (e : I ≃ BinaryComplete.Coord (SourceCompiler.registerPower c lam n) (SourceCompiler.fieldBits c lam n)) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (χ : F → Fin (SourceCompiler.registerPower c lam n)) (π : F ≃ F) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) {ω : ValueModel} (hQ : QLD.SoundIn ω M) (S : M.ProjStrat (NumberedComplete.game e L D hm b χ π)) (hA : RestrictedSoundness.ParsedPauliSupported S.PA) (hB : RestrictedSoundness.ParsedPauliSupported S.PB) {ε : ℝ} (hε : 0 ≤ ε) (hS : 1 - S.value ≤ ε) : 1 - errorProfile (RestrictedSoundness.profileCoefficient ℓ (PauliErrorParameters.profileCoefficient RestrictedSoundness.qldCoefficient ↑c) RestrictedSoundness.qldExponent) (RestrictedSoundness.qldExponent * rootExponent (6 * ℓ + 2)) (↑lam * ↑n) ε ≤ ω.val (Honest.sourceGame L D)

Uniform soundness for the actual canonical field and register parameters, on the source's original coordinate type. All QLD tails are absorbed.