Preliminary comparison theorems: bipartite self-consistency (core)

Core building blocks for bipartite self-consistency: reflexivity of the state-dependent distance, the swap of placements inside qSDDCore, and prop:two-notions-of-self-consistency. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/BipartiteSelfConsistency/Core.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The bipartite statements take a symmetric model S : SymModel 𝔓 K in place of the state ψ : QuantumState (ι × ι), and local families in 𝔓; sddError_self is about a state on one space and takes a vector state V : VecState K. Each takes the model or the vector state as an explicit first argument, in the namespace Preliminaries, as the vendored lemmas do.

The vendored swap hypotheses are dropped: hperm : PermInvState ψ from qSDDCore_rightTensor_eq_leftTensor_of_permInv and qSDD_liftLeft_liftRight_le_two_qBipartiteSSCDefect, and the conjunct PermInvState ψ of the hypothesis of twoNotionsOfSelfConsistency. Each use of PermInvState.swap_ev is the model's S.ev_L_eq_ev_R (Co/Basic/QuantumState.lean). The vendored qSDDCore_rightTensor_eq_leftTensor_of_permInv took the state implicitly, determined by hperm; with hperm gone the model is explicit.

New here

• ev_adjoint_self_leftTensor_sub_rightTensor: the expansion ev((L X - R X)^* (L X - R X)) = 2 (ev L(X²) - ev(L X R X)) for self-adjoint X, which the vendored file proves inline (h_expand) and BipartiteSelfConsistency/Local.lean repeats; here it is the case X = Y of ev_star_L_sub_R_mul_self (SwitchSandwichMain/RightTransfer) with the swap.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/preliminaries.tex, prop:two-notions-of-self-consistency

theorem MIPRE.LIDT.Co.Preliminaries.sddError_self {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) : V.sddError 𝒟 A A = 0

The self-distance sddError 𝒟 A A is zero.

theorem MIPRE.LIDT.Co.Preliminaries.qSDDCore_rightTensor_eq_leftTensor_of_permInv {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A B : Outcome → 𝔓) : (S.qSDDCore (fun (a : Outcome) => S.R (A a)) fun (a : Outcome) => S.R (B a)) = S.qSDDCore (fun (a : Outcome) => S.L (A a)) fun (a : Outcome) => S.L (B a)

The qSDDCore distance between right placements of two local operator families equals the distance between their left placements.

The vendored lemma asks for a permutation-invariant state; here swap symmetry is the model's S.ev_L_eq_ev_R, applied to (A_a - B_a)^* (A_a - B_a).

theorem MIPRE.LIDT.Co.Preliminaries.ev_adjoint_self_leftTensor_sub_rightTensor {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {X : 𝔓} (hX : IsSelfAdjoint X) : S.ev (star (S.L X - S.R X) * (S.L X - S.R X)) = 2 * (S.ev (S.L (X * X)) - S.ev (S.opTensor X X))

For a self-adjoint local operator X, ev((L X - R X)^* (L X - R X)) = 2 (ev L(X²) - ev(L X R X)): the case X = Y of ev_star_L_sub_R_mul_self (SwitchSandwichMain/RightTransfer.lean), the two squares having the same expectation by swap symmetry (S.ev_L_eq_ev_R).

theorem MIPRE.LIDT.Co.Preliminaries.qSDD_liftLeft_liftRight_le_two_qBipartiteSSCDefect {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (M : SubMeas Outcome 𝔓) : S.qSDD (SubMeas.liftLeft S M) (SubMeas.liftRight S M) ≤ 2 * S.qBipartiteSSCDefect M

The squared distance between the left and right lifts of a submeasurement is at most twice its bipartite strong self-consistency defect. The vendored lemma asks for a permutation-invariant state.

theorem MIPRE.LIDT.Co.Preliminaries.twoNotionsOfSelfConsistency {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (A : IdxSubMeas Question Outcome 𝔓) (δ : ℝ) : S.BipartiteSSCRel 𝒟 A δ → S.SDDRel 𝒟 (IdxSubMeas.liftLeft S A) (IdxSubMeas.liftRight S A) (2 * δ)

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

If A is bipartite strongly self-consistent (∑ₐ ev(Aₐ ⊗ I) − ∑ₐ ev(Aₐ ⊗ Aₐ) ≤ δ on average), then its left and right lifts are 2δ-close. The vendored hypothesis is PermInvState ψ ∧ BipartiteSSCRel ψ 𝒟 A δ; the first conjunct is a theorem of the model.