Full Read rigidity from game success and primitive Pauli estimates #
The complete hiding theorem supplies the input of the actual hiding-to-Read chain. The resulting estimates hold for every dual prefix and both players, with one explicit bound independent of the question and answer alphabets.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the extracted register state is
the register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, the measurements are POVMs
in its algebras, and the honest readouts enter as smulKron 1 _.
noncomputable def
MIPRE.Introspection.TypedEstimates.readAliceError
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
(L : Bool → CL.CLFun F ι ℓ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(j : Fin ℓ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
MIPRE.Introspection.TypedEstimates.readBobError
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(L : Bool → CL.CLFun F ι ℓ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
(j : Fin ℓ)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
MIPRE.Introspection.TypedEstimates.read_register_rigidity_of_pauli
{PauliType : Type u_1}
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{κ : Type u_5}
{A : Type u_6}
[Fintype PauliType]
[DecidableEq PauliType]
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype κ]
[DecidableEq κ]
[Fintype A]
{ℓ : ℕ}
{𝒞 : Type u_7}
{𝒜 : Type u_8}
{ℬ : Type u_9}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[StarModule ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[StarModule ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[StarProper 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
[StarProper ℬ]
(E : PauliType → PauliType → Bool)
(X Z : PauliType)
(P : PauliType → CL.CLFun (ZMod 2) κ 3)
(L : Bool → CL.CLFun F ι ℓ)
(projectPauli : PauliAnswer → ι → F)
(D : (ι → F) → (ι → F) → A → A → Bool)
(DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool)
(Ξ : BipartiteModel 𝒞 𝒜 ℬ)
(hΞ : ‖Ξ.ψ‖ = 1)
(MA :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜))
(MB :
CL.Detyping.Question (QuestionType PauliType ℓ) κ →
POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ))
{ε δX ηZ : ℝ}
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(qX qZ : κ → ZMod 2)
(hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX)
(hqZ : ∀ (z : κ → ZMod 2), (P Z).eval z = qZ)
(hPX : IsPVMIn (MA (QuestionType.pauli X, qX)).op)
(hX :
∑ x : Option (ι → F),
(Ξ.reg (ι → F)).stateSqNorm
((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli X, qX))).op x - smulKron 1 (Honest.pauliXReadout x)) ≤ δX)
(hZ :
∑ z : Option (ι → F),
(Ξ.reg (ι → F)).snorm
((Ξ.reg (ι → F)).πB
((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli Z, qZ))).op z - smulKron 1 (readout some z))) ^ 2 ≤ ηZ)
(w : Bool)
(hL : (L w).SupportedOn Finset.univ)
(hS : IsPVMIn (MA (QuestionType.sample w, 0)).op)
(hMA : ∀ (j : Fin ℓ), IsPVMIn (MA (QuestionType.hide w j, 0)).op)
(hMB : ∀ (j : Fin ℓ), IsPVMIn (MB (QuestionType.hide w j, 0)).op)
(j : Fin ℓ)
:
readAliceError L w hL Ξ MA j ≤ (16 * ↑ℓ ^ 2 + 8) * (↑(TypeGraph.edges E X Z ℓ).card * ε) + 4 * hidingPauliBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δX ηZ ∧ readBobError L w hL Ξ MB j ≤ (32 * ↑ℓ ^ 2 + 20) * (↑(TypeGraph.edges E X Z ℓ).card * ε) + 8 * hidingPauliBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δX ηZ
Both actual Read families are rigid at every dual prefix. The inputs are game success and the extracted X/Z estimates, without a Read or hiding rigidity premise. No projectivity of either Read measurement is needed.