Option completion in the orthonormalization argument

The auxiliary algebra used when the orthonormalization theorem is applied to the completion of a submeasurement by a fresh failure outcome, comparing the completed measurement with the restriction obtained by discarding this outcome: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MakingMeasurementsProjective/Orthonormalization/Completion.lean in the port of planning/c6b-plan.md (milestone M8, section "Port conventions").

Both lemmas take a symmetric model S : SymModel 𝔓 K and a local submeasurement in 𝔓. The vendored hypotheses hperm : PermInvState ψ and hψ : ψ.IsNormalized of optionCompletion_bipartiteSSCRel are dropped: the swap step is S.ev_L_eq_ev_R and S.ev 1 = 1 is a theorem. The vendored A.liftLeft is A.map S.L. The vendored proof bounds the overlap of the totals through Preliminaries.qBipartiteSSCDefect_postprocess_le at the constant readout; here the same bound, ∑ₐ ⟨Ψ, (Aₐ ⊗ Aₐ) Ψ⟩ ≤ ⟨Ψ, (T ⊗ T) Ψ⟩ for the total T, is the positivity of the off-diagonal overlaps, as in step 2 of SymModel.one_sub_sum_norm_sq_completion_le (Co/Doubling/Orthonormalization.lean).

Not ported

Every declaration of the vendored file has a counterpart here.

theorem MIPRE.LIDT.Co.MakingMeasurementsProjective.Orthonormalization.Completion.optionCompletion_bipartiteSSCRel {𝔓 : 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 : SubMeas Outcome 𝔓) (ζ : ℝ) : S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) ζ → S.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (optionCompletion A).toSubMeas) (2 * ζ)

Completing a submeasurement by a fresh failure outcome preserves bipartite strong self-consistency up to the paper's factor 2: the original diagonal gap controls the original outcomes, and the same gap controls the residual none outcome after applying the swap symmetry of the model.

theorem MIPRE.LIDT.Co.MakingMeasurementsProjective.Orthonormalization.Completion.qSDD_liftLeft_restrictSomeProjSubMeas_le {𝔓 : 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 : SubMeas Outcome 𝔓) (P : ProjSubMeas (Option Outcome) 𝔓) : S.qSDD (SubMeas.map S.L A) (SubMeas.map S.L (restrictSomeProjSubMeas P).toSubMeas) ≤ S.qSDD (SubMeas.map S.L (optionCompletion A).toSubMeas) (SubMeas.map S.L P.toSubMeas)

Discarding the extra none outcome from the option-completed measurement can only decrease the qSDD sum: one simply drops a nonnegative summand.