Preliminary comparison theorems: projective converse

Projective-case converse of prop:simeq-to-approx: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/ComparisonProjective.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions"). As in the vendored file, the lemma lives in a sibling module of ComparisonCore, and imports ComparisonCore, ConsistencyBridges and SwitchSandwichPrep.Core explicitly.

As in Co/Preliminaries/Defs.lean, the declarations live in MIPRE.LIDT.Co.Preliminaries and take the symmetric model S : SymModel 𝔓 K as an ordinary explicit argument in place of the vendored state ψ; the projective measurements are local, with operators in 𝔓.

For projective A, B the per-outcome square (A_a ⊗ I - I ⊗ B_a)² is A_a ⊗ I + I ⊗ B_a - 2 A_a ⊗ B_a, because the two placements commute (SymModel.L_comm_R) and each placement is idempotent; summing over outcomes gives qSDD = 2 (⟨1⟩ - qMatchMass) = 2 qConsDefect. The vendored proof instead obtains ev (B ⊗ … · A ⊗ …) = ev (A ⊗ … · B ⊗ …) from ev_mul_comm_of_psd, and the diagonal masses from projSubMeas_diagMass_eq_mass on two auxiliary projective submeasurements; here the commutation is an operator identity and the diagonal masses are the placed totals.

In the symmetric model both tensor factors are 𝔓, and the general placements leftPlacedSubMeas, rightPlacedSubMeas, IdxSubMeas.placeLeft, placeRight are the lifts by rfl (Co/Basic/SubMeasurementFamilies.lean). So the _heterogeneous statements, whose measurements act on the same algebra 𝔓, follow from the same-space ones by definitional unfolding.

Not ported

Every declaration of the vendored file has a counterpart here.

theorem MIPRE.LIDT.Co.Preliminaries.two_questionConsistency_eq_questionSDD_of_projective {𝔓 : 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 : ProjMeas Outcome 𝔓) : 2 * S.qConsDefect (SubMeas.liftLeft S A.toSubMeas) (SubMeas.liftRight S B.toSubMeas) = S.qSDD (SubMeas.liftLeft S A.toSubMeas) (SubMeas.liftRight S B.toSubMeas)

For projective measurements A, B, twice the consistency defect of the lifts A_a ⊗ I and I ⊗ B_a equals their squared state-dependent distance.

theorem MIPRE.LIDT.Co.Preliminaries.approxToSimeq {𝔓 : 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 B : IdxProjMeas Question Outcome 𝔓) (δ : ℝ) : BipartiteSDDRel S 𝒟 A.toIdxSubMeas B.toIdxSubMeas (2 * δ) → S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ

Projective converse of prop:simeq-to-approx (Proposition 4.9 of references/ldt-paper/preliminaries.tex in LionSR/MIPStarRE, lines 426--455).

For projective measurements A, B, the ≈ relation at strength 2·δ implies the ≃ relation at strength δ, making the paper's implication an iff in the projective case (the forward direction is simeqToApprox).

theorem MIPRE.LIDT.Co.Preliminaries.two_questionConsistency_eq_questionSDD_of_projective_heterogeneous {𝔓 : 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 : ProjMeas Outcome 𝔓) : 2 * S.qConsDefect (S.leftPlacedSubMeas A.toSubMeas) (S.rightPlacedSubMeas B.toSubMeas) = S.qSDD (S.leftPlacedSubMeas A.toSubMeas) (S.rightPlacedSubMeas B.toSubMeas)

For projective measurements A, B, twice the consistency defect of the placed families A_a ⊗ I and I ⊗ B_a equals their squared state-dependent distance. In the symmetric model the placements are the lifts, so this is two_questionConsistency_eq_questionSDD_of_projective.

theorem MIPRE.LIDT.Co.Preliminaries.approxToSimeq_heterogeneous {𝔓 : 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 B : IdxProjMeas Question Outcome 𝔓) (δ : ℝ) : S.SDDRel 𝒟 (IdxSubMeas.placeLeft S A.toIdxSubMeas) (IdxSubMeas.placeRight S B.toIdxSubMeas) (2 * δ) → S.ConsRel 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ

Heterogeneous projective converse of prop:simeq-to-approx.

For projective measurements acting on different tensor factors, a state-dependent-distance estimate at strength 2·δ for the placed families implies the corresponding bipartite consistency statement at strength δ.