Section 11 commutativity: scalar approximation core

Upstream scalar-approximation lemmas that do not depend on the later averaged commutation proof, so they can be shared by both ProcessedG and Pointwise without creating import cycles.

References

• references/ldt-paper/commutativity-G.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPStarRE.LDT.Commutativity.qBipartiteSSCDefect_eq_half_qSDD_of_proj {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (P : ProjSubMeas α ι) : qBipartiteSSCDefect ψ P.toSubMeas = 1 / 2 * qSDD ψ P.liftLeft P.liftRight

For a projective submeasurement on a permutation-invariant bipartite state, the bipartite SSC defect is exactly half of the left/right SDD defect.