Preliminary comparison theorems: bipartite self-consistency (local bridges)

The bridge from bipartite strong self-consistency of a local family to strong self-consistency of its left lift: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/BipartiteSelfConsistency/Local.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

bipartiteSSC_implies_localSSC_liftLeft takes a symmetric model S : SymModel 𝔓 K in place of the state ψ : QuantumState (ι × ι) and drops the vendored hypothesis hperm : PermInvState ψ. The bipartite overlap ∑ₐ ev(Aₐ ⊗ Aₐ) and the local square ∑ₐ ev(Aₐ² ⊗ I) are comparable because ev(M ⊗ I) = ev(I ⊗ M), the model's S.ev_L_eq_ev_R, which enters through ev_adjoint_self_leftTensor_sub_rightTensor (BipartiteSelfConsistency/Core.lean). The comparison is made outcome by outcome, where the vendored proof sums first.

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

theorem MIPRE.LIDT.Co.Preliminaries.bipartiteSSC_implies_localSSC_liftLeft {𝔓 : 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.SSCRel 𝒟 (IdxSubMeas.liftLeft S A) δ

Bridge lemma: bipartite strong self-consistency of a local family implies strong self-consistency of its left lift, with the same constant.

Each overlap ev(Aₐ ⊗ Aₐ) is at most the local square ev(Aₐ² ⊗ I), since 0 ≤ ev((Aₐ ⊗ I − I ⊗ Aₐ)^* (Aₐ ⊗ I − I ⊗ Aₐ)) = 2 (ev(Aₐ² ⊗ I) − ev(Aₐ ⊗ Aₐ)) by swap symmetry. The vendored lemma asks for a permutation-invariant state.