Preliminary comparison theorems: bipartite self-consistency (core)

Core building blocks for bipartite self-consistency: reflexivity of the question-level state-dependent distance qSDD and its lift to the family-level sddError.

References

• references/ldt-paper/preliminaries.tex
• blueprint/src/chapter/ch03_preliminaries.tex

theorem MIPStarRE.LDT.Preliminaries.sddError_self {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) : sddError ψ 𝒟 A A = 0

The self-distance sddError ψ 𝒟 A A is zero.

theorem MIPStarRE.LDT.Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] {ψ : QuantumState (ι × ι)} (hperm : PermInvState ψ) (A B : Outcome → Quantum.Op ι) : (qSDDCore ψ (fun (a : Outcome) => rightTensor (A a)) fun (a : Outcome) => rightTensor (B a)) = qSDDCore ψ (fun (a : Outcome) => leftTensor (A a)) fun (a : Outcome) => leftTensor (B a)

On a permutation-invariant bipartite state, the qSDDCore distance between right-tensor placements of two local operator families equals the corresponding left-tensor distance.

This is a shared tensor-placement helper for Bob/right-register variants of ≈_δ arguments. The proof expands each squared-difference term and applies PermInvState.swap_ev to (A_a-B_a)^†(A_a-B_a).

theorem MIPStarRE.LDT.Preliminaries.twoNotionsOfSelfConsistency {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A : IdxSubMeas Question Outcome ι) (δ : Error) : PermInvState ψ ∧ BipartiteSSCRel ψ 𝒟 A δ → SDDRel ψ 𝒟 A.liftLeft A.liftRight (2 * δ)

prop:two-notions-of-self-consistency.

If the indexed sub-measurement A is bipartite-strongly-self-consistent on the permutation-invariant state ψ (i.e., BipartiteSSCRel ψ 𝒟 A δ, meaning ∑ₐ ev ψ (Aₐ ⊗ I) − ∑ₐ ev ψ (Aₐ ⊗ Aₐ) ≤ δ), then the left and right lifts are close: SDDRel ψ 𝒟 (liftLeft A) (liftRight A) (2 * δ).

Paper proof sketch:

1. Expand ∑ₐ ev ψ ((Aₐ⊗I − I⊗Aₐ)² ).
2. Using Kronecker mixed-product rule and PermInvState.swap_ev, this equals 2 · (∑ₐ ev ψ (Aₐ²⊗I) − ∑ₐ ev ψ (Aₐ⊗Aₐ)).
3. Since Aₐ² ≤ Aₐ (sub-measurement bound), we get ≤ 2 · (∑ₐ ev ψ (Aₐ⊗I) − ∑ₐ ev ψ (Aₐ⊗Aₐ)) = 2 · bipartiteSSCDefect.
4. Average over 𝒟 and apply the BipartiteSSCRel hypothesis.