Preliminary comparison theorems: bipartite self-consistency (completion)

Completion-transfer lemmas for bipartite self-consistency: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/BipartiteSelfConsistency/Completion.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions"). The constant Unit-family reductions identify sddError and sscError with their pointwise forms, and the later lemmas compare a submeasurement with its completion.

The vendored state of constFamily_sdd_unit, constFamily_ssc_unit and completion_self_distance is a state on one space, so they take a vector state V : VecState K and submeasurements of joint operators in K →L[ℂ] K. evaluateAt_completeAtOutcome mentions no state and is generic over the ordered ⋆-ring of evaluateAt and completeAtOutcome. qBipartiteConsDefect_completeAtOutcome_right_le is stated over ψ : QuantumState (ιA × ιB) with local measurements on two different spaces; it takes a symmetric model S : SymModel 𝔓 K, with both measurements in 𝔓, as every bipartite defect of the port does (section "Port conventions", same-space and bipartite quantities). Its proof bounds the matching mass of the completion below by monotonicity of S.opTensor, where the vendored proof computes it exactly.

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.constFamily_sdd_unit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B : SubMeas Outcome (K →L[ℂ] K)) : V.sddError (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) (constSubMeasFamily B) = V.qSDD A B

For a constant Unit-indexed family, sddError reduces to qSDD.

theorem MIPRE.LIDT.Co.Preliminaries.constFamily_ssc_unit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A : SubMeas Outcome (K →L[ℂ] K)) : V.sscError (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) = V.qSSCDefect A

For a constant Unit-indexed family, sscError reduces to qSSCDefect.

theorem MIPRE.LIDT.Co.Preliminaries.completion_self_distance {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (B : SubMeas Outcome (K →L[ℂ] K)) (a0 : Outcome) : V.qSDD B (completeAtOutcome B a0).toSubMeas = V.ev ((1 - B.total) * (1 - B.total))

Completing B at a0 changes only the missing mass, so the self-distance is exactly the squared residual mass.

theorem MIPRE.LIDT.Co.Preliminaries.evaluateAt_completeAtOutcome {R : Type u_1} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (H : SubMeas (MIPStarRE.LDT.Polynomial params) R) (h0 : MIPStarRE.LDT.Polynomial params) (u : MIPStarRE.LDT.Point params) : evaluateAt params u (completeAtOutcome H h0).toSubMeas = (completeAtOutcome (evaluateAt params u H) (h0.toFun u)).toSubMeas

Evaluating a completed polynomial submeasurement at a point is the same as completing the evaluated submeasurement at the induced outcome.

theorem MIPRE.LIDT.Co.Preliminaries.qBipartiteConsDefect_completeAtOutcome_right_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 : Measurement Outcome 𝔓) (B : SubMeas Outcome 𝔓) (a0 : Outcome) : S.qBipartiteConsDefect A.toSubMeas (completeAtOutcome B a0).toSubMeas ≤ S.qBipartiteConsDefect A.toSubMeas B + S.ev (S.R (1 - B.total))

Completing the right submeasurement can increase the bipartite consistency defect by at most the residual completion mass 1 - B.total.