Initializing hiding rigidity from the extracted Pauli-X family #
The fine Pauli-X replacement estimate is first converted to cross-party
consistency using its exact EPR mirror. Projective coarse-graining therefore
costs nothing. The actual Pauli-X/first-hiding edge then identifies the first
hiding family, with error 2 deltaX + 4 |E| epsilon on a full EPR-plus-auxiliary
state. No first-hiding rigidity hypothesis is used.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the EPR-plus-auxiliary state is
the register model Ξ.reg (ι → F) of a normalized auxiliary model, and the honest families enter
as smulKron 1 _.
theorem
MIPRE.Introspection.TypedEstimates.pauliX_firstHide_mapped
{PauliAnswer : Type u_2}
{F : Type u_3}
{ι : Type u_4}
{A : Type u_6}
[Fintype PauliAnswer]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
[Fintype ι]
[DecidableEq ι]
[Fintype A]
{ℓ : ℕ}
{R : Type u_7}
[Ring R]
[StarRing R]
[PartialOrder R]
[StarOrderedRing R]
(P : CL.CLFun F ι ℓ)
(projectPauli : PauliAnswer → ι → F)
(M : POVMIn (ParsedAnswer (ι → F) A PauliAnswer) R)
(z : Option (Honest.HideLabel F ι))
:
fibSumIn (fun (x : Option (ι → F)) => (POVMIn.map (pauliProjection projectPauli) M).op x)
(Option.map (Honest.firstHideAnswer P)) z = (POVMIn.map
(fun (a : ParsedAnswer (ι → F) A PauliAnswer) =>
Option.map (Honest.firstHideAnswer P) (pauliProjection projectPauli a))
M).op
z
theorem
MIPRE.Introspection.TypedEstimates.hiding_first_register_rigidity_cross
{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) ℬ))
{ε : ℝ}
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k = 0)
(hL : (L w).SupportedOn Finset.univ)
(qX : κ → ZMod 2)
(hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX)
(hMA : IsPVMIn (MA (Sum.inl X, qX)).op)
{δX : ℝ}
(hPauli :
∑ x : Option (ι → F),
(Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (pauliProjection projectPauli) (MA (Sum.inl X, qX))).op x)
(smulKron 1 (Honest.pauliXReadout x)) ≤ δX)
:
A cross-party extracted Pauli-X guarantee initializes the actual hiding chain. Only the Pauli-X measurement needs projectivity at this step.
theorem
MIPRE.Introspection.TypedEstimates.hiding_first_register_rigidity
{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) ℬ))
{ε : ℝ}
(hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε)
(w : Bool)
(k : Fin ℓ)
(hk : ↑k = 0)
(hL : (L w).SupportedOn Finset.univ)
(qX : κ → ZMod 2)
(hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX)
(hMA : IsPVMIn (MA (Sum.inl X, qX)).op)
{δX : ℝ}
(hPauli :
∑ x : Option (ι → F),
(Ξ.reg (ι → F)).stateSqNorm
((POVMIn.map (pauliProjection projectPauli) (MA (Sum.inl X, qX))).op x - smulKron 1 (Honest.pauliXReadout x)) ≤ δX)
:
The usual same-party extracted Pauli-X replacement estimate suffices: the ideal X projectors are exact mirrors on the EPR register, independently of the auxiliary state.