Preliminary comparison theorems: bipartite self-consistency (local bridges) #
Bridge lemmas connecting the bipartite self-consistency relation on a permutation-invariant state to the single-sided local self-consistency relation after a left/right lift of the family.
References #
references/ldt-paper/preliminaries.texblueprint/src/chapter/ch03_preliminaries.tex
theorem
MIPStarRE.LDT.Preliminaries.bipartiteSSC_implies_localSSC_liftLeft
{Question : Type u_1}
{Outcome : Type u_2}
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
[Fintype Outcome]
(ψ : QuantumState (ι × ι))
(hperm : PermInvState ψ)
(𝒟 : Distribution Question)
(A : IdxSubMeas Question Outcome ι)
(δ : Error)
:
BipartiteSSCRel ψ 𝒟 A δ → SSCRel ψ 𝒟 A.liftLeft δ
Bridge lemma: for a permutation-invariant bipartite state, bipartite SSC on local families implies local SSC on the left-lifted families.
Requires PermInvState ψ because the bipartite defect
∑ ev(A_a ⊗ A_a) and local defect ∑ ev(A_a² ⊗ I) are generally
incomparable without symmetry; the permutation-invariance bridge
ev(M ⊗ I) = ev(I ⊗ M) makes the two notions equivalent.
The proof expands qSDD ψ A.liftLeft A.liftRight, uses
PermInvState.swap_ev to identify the left and right square terms, and
then reads off ∑ ev(A_a² ⊗ I) ≥ ∑ ev(A_a ⊗ A_a) from
qSDD_nonneg.