Source-boundary role-register handoff: completion lemmas

The completion and line-169 transport lemmas of the two-space tail of the main theorem: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Test/MainTheorem/SourceRoleRegister/Completion.lean in the port of planning/c6b-plan.md (milestone M13, section "Port conventions").

Everything here is two-space. The vendored state is on ιA × ιB, with Alice's measurements on ιA and Bob's on ιB. Here it is a bipartite model M : MIPRE.BipartiteModel 𝒞 𝒜 ℬ with a unit vector, hψ : ‖M.ψ‖ = 1, and for the three theorems the model strategy.state of a two-space ProjStrat, with strategy.isNormalized. The translation is that of Co/Test/MainTheorem/TwoSpace.lean:

• the vendored ConsRel ψ 𝒟 A B δ is bipartiteConsError M 𝒟 A B ≤ δ (M2's two-space defect);
• SDDRel ψ 𝒟 (leftPlacedSubMeas A) … is (TwoSpace.vecState M hψ).SDDRel 𝒟 (TwoSpace.leftPlacedSubMeas M A) …, a relation of the vector state on M.H →L[ℂ] M.H;
• ev ψ (leftTensor X) is (TwoSpace.vecState M hψ).ev (TwoSpace.placeA M X), and the right forms likewise through placeB. The same-space lemmas of Co Preliminaries (completion_self_distance, constFamily_sdd_unit, questionSDD_triangle, question_easyApproxFromApproxDelta, right_match_gap_abs_le_sqrt_qSDD, stateDependentDistanceRel_triangle_three) apply to the placed families as they are, and TwoSpace.simeqToApprox_heterogeneous is the two-space simeqToApprox_heterogeneous.

The two matrix bookkeeping lemmas qSDD_leftPlaced_completeAtOutcome_eq and qSDD_rightPlaced_completeAtOutcome_eq, entrywise Kronecker computations in the vendored file, are here the fact that a placement commutes with completion (placeA M 1 = 1 and map_sub). They take any vector state V : VecState M.H, since they use only the placements.

Departure: completion takes hM : M.IsFinitePair. The vendored Preliminaries.completeAtOutcomeProj needs a C⋆-algebra, and 𝒜, ℬ are abstract star-ordered ⋆-algebras; so a projective submeasurement is completed through TwoSpace.completeAtOutcomeProjA/B, which complete in the commutant that a finite pair identifies each algebra with. The lemmas and theorems that complete therefore take hM : M.IsFinitePair (hM : strategy.state.IsFinitePair for the theorems), placed right after the state and, where it is taken, its normalization hψ. The completion's submeasurement is completeAtOutcome P a0 (TwoSpace.completeAtOutcomeProjA_toSubMeas), so nothing else changes. completedProjectiveConsistency_ofFullConsistency completes nothing and takes no hM.

Departure: imports. The vendored file imports SourceRoleRegister/Core; this one imports Co Test/MainTheorem/ProjectiveConsistency/Evaluation (with TwoSpace) and the M8 files MakingMeasurementsProjective/{Orthonormalization, ProjectivizationChain/Basic}, which bring the vendored classical constants orthonormalizationError and orthonormalizeAndCompleteError. No declaration of the vendored Core is used, so the Co Core is not imported.

The constants are the vendored ones: orthonormalizationError ζ for the orthonormalization, orthonormalizeAndCompleteError ζ after completion, ζ + √(orthonormalizationError ζ) for the repaired line-169 consistency and 6ζ + 6ζ₂ for the line-156 distance.

New here

• bipartiteConsError_constFamily_unit: the two-space defect of constant Unit-indexed families is the defect of their members (the two-space form of Preliminaries.constFamily_sdd_unit, which the vendored proofs unfold by simp at every use).

Not ported

Every declaration of the vendored file has a counterpart here.

theorem MIPRE.LIDT.Co.ProjStrat.bipartiteConsError_constFamily_unit {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [PartialOrder ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (A : SubMeas Outcome 𝒜) (B : SubMeas Outcome ℬ) : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily A) (constSubMeasFamily B) = qBipartiteConsDefect M A B

The two-space defect of constant Unit-indexed families under the uniform distribution is the defect of their members.

theorem MIPRE.LIDT.Co.ProjStrat.qSDD_leftPlaced_completeAtOutcome_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (V : VecState M.H) (A B : SubMeas Outcome 𝒜) (a0 : Outcome) : V.qSDD (TwoSpace.leftPlacedSubMeas M A) (Preliminaries.completeAtOutcome (TwoSpace.leftPlacedSubMeas M B) a0).toSubMeas = V.qSDD (TwoSpace.leftPlacedSubMeas M A) (TwoSpace.leftPlacedSubMeas M (Preliminaries.completeAtOutcome B a0).toSubMeas)

Completing after left placement agrees with left placement after completing the local submeasurement: a placement maps 1 to 1 and commutes with differences.

This is the bookkeeping needed to apply the completion-distance identity on M.H while returning the local completed projective measurement of the paper.

theorem MIPRE.LIDT.Co.ProjStrat.qSDD_rightPlaced_completeAtOutcome_eq {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (V : VecState M.H) (A B : SubMeas Outcome ℬ) (a0 : Outcome) : V.qSDD (TwoSpace.rightPlacedSubMeas M A) (Preliminaries.completeAtOutcome (TwoSpace.rightPlacedSubMeas M B) a0).toSubMeas = V.qSDD (TwoSpace.rightPlacedSubMeas M A) (TwoSpace.rightPlacedSubMeas M (Preliminaries.completeAtOutcome B a0).toSubMeas)

Completing after right placement agrees with right placement after completing the local submeasurement.

theorem MIPRE.LIDT.Co.ProjStrat.qSDD_completeAtOutcomeProj_leftPlaced_le_of_total_gap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (hM : M.IsFinitePair) (P : ProjSubMeas Outcome 𝒜) (a0 : Outcome) {ζ : ℝ} (hgap : 1 - (TwoSpace.vecState M hψ).ev ((TwoSpace.placeA M) P.total) ≤ ζ) : (TwoSpace.vecState M hψ).qSDD (TwoSpace.leftPlacedSubMeas M P.toSubMeas) (TwoSpace.leftPlacedSubMeas M (TwoSpace.completeAtOutcomeProjA hM P a0).toSubMeas) ≤ ζ

If the missing left total of a projective submeasurement is small on the state, then its completion is close to it after left placement.

theorem MIPRE.LIDT.Co.ProjStrat.qSDD_completeAtOutcomeProj_rightPlaced_le_of_total_gap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (hM : M.IsFinitePair) (P : ProjSubMeas Outcome ℬ) (a0 : Outcome) {ζ : ℝ} (hgap : 1 - (TwoSpace.vecState M hψ).ev ((TwoSpace.placeB M) P.total) ≤ ζ) : (TwoSpace.vecState M hψ).qSDD (TwoSpace.rightPlacedSubMeas M P.toSubMeas) (TwoSpace.rightPlacedSubMeas M (TwoSpace.completeAtOutcomeProjB hM P a0).toSubMeas) ≤ ζ

Right-placement counterpart of qSDD_completeAtOutcomeProj_leftPlaced_le_of_total_gap.

theorem MIPRE.LIDT.Co.ProjStrat.qBipartiteMatchMass_ge_sub_sqrt_of_left_sdd_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (G : Measurement Outcome 𝒜) (P : SubMeas Outcome 𝒜) (B : Measurement Outcome ℬ) {ε : ℝ} (hclose : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M G.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M P)) ε) : qBipartiteMatchMass M P B.toSubMeas ≥ qBipartiteMatchMass M G.toSubMeas B.toSubMeas - √ε

A left-placement distance estimate controls the loss in two-space matching mass against a complete measurement of the second player.

theorem MIPRE.LIDT.Co.ProjStrat.qBipartiteMatchMass_ge_sub_sqrt_of_right_sdd_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (A : Measurement Outcome 𝒜) (G : Measurement Outcome ℬ) (P : SubMeas Outcome ℬ) {ε : ℝ} (hclose : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M G.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M P)) ε) : qBipartiteMatchMass M A.toSubMeas P ≥ qBipartiteMatchMass M A.toSubMeas G.toSubMeas - √ε

A right-placement distance estimate controls the loss in two-space matching mass against a complete measurement of the first player.

theorem MIPRE.LIDT.Co.ProjStrat.qBipartiteMatchMass_le_left_total_of_measurement_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (A : SubMeas Outcome 𝒜) (B : Measurement Outcome ℬ) : qBipartiteMatchMass M A B.toSubMeas ≤ (TwoSpace.vecState M hψ).ev ((TwoSpace.placeA M) A.total)

The two-space matching mass against a complete measurement of the second player is at most the expectation of the placed total of the other submeasurement.

theorem MIPRE.LIDT.Co.ProjStrat.qBipartiteMatchMass_le_right_total_of_measurement_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (A : Measurement Outcome 𝒜) (B : SubMeas Outcome ℬ) : qBipartiteMatchMass M A.toSubMeas B ≤ (TwoSpace.vecState M hψ).ev ((TwoSpace.placeB M) B.total)

The two-space matching mass against a complete measurement of the first player is at most the expectation of the placed total of the other submeasurement.

theorem MIPRE.LIDT.Co.ProjStrat.completeAtOutcomeProj_left_matchMass_ge_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hM : M.IsFinitePair) (P : ProjSubMeas Outcome 𝒜) (B : SubMeas Outcome ℬ) (a0 : Outcome) : qBipartiteMatchMass M (TwoSpace.completeAtOutcomeProjA hM P a0).toSubMeas B ≥ qBipartiteMatchMass M P.toSubMeas B

Completing a projective submeasurement of the first player can only increase its two-space matching mass against a fixed submeasurement of the second player.

theorem MIPRE.LIDT.Co.ProjStrat.completeAtOutcomeProj_right_matchMass_ge_heterogeneous {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hM : M.IsFinitePair) (A : SubMeas Outcome 𝒜) (P : ProjSubMeas Outcome ℬ) (a0 : Outcome) : qBipartiteMatchMass M A (TwoSpace.completeAtOutcomeProjB hM P a0).toSubMeas ≥ qBipartiteMatchMass M A P.toSubMeas

Completing a projective submeasurement of the second player can only increase its two-space matching mass against a fixed submeasurement of the first player.

theorem MIPRE.LIDT.Co.ProjStrat.completedCloseness_left_of_consistency_and_sdd {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (hM : M.IsFinitePair) (ζ : ℝ) (G_A : Measurement Outcome 𝒜) (G_B : Measurement Outcome ℬ) (P_A : ProjSubMeas Outcome 𝒜) (a0 : Outcome) (hpre : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (horth : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M P_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M (TwoSpace.completeAtOutcomeProjA hM P_A a0).toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)

Combine cross consistency and the first player's orthonormalization closeness into the completion estimate for the left placement.

theorem MIPRE.LIDT.Co.ProjStrat.completedCloseness_right_of_consistency_and_sdd {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (hM : M.IsFinitePair) (ζ : ℝ) (G_A : Measurement Outcome 𝒜) (G_B : Measurement Outcome ℬ) (P_B : ProjSubMeas Outcome ℬ) (a0 : Outcome) (hpre : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (horth : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M P_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M (TwoSpace.completeAtOutcomeProjB hM P_B a0).toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)

Second-player counterpart of completedCloseness_left_of_consistency_and_sdd.

theorem MIPRE.LIDT.Co.ProjStrat.completedLeftConsistency_of_consistency_and_sdd {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (hM : M.IsFinitePair) (ζ : ℝ) (G_A : Measurement Outcome 𝒜) (G_B : Measurement Outcome ℬ) (P_A : ProjSubMeas Outcome 𝒜) (a0 : Outcome) (hpre : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (horth : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas M P_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.completeAtOutcomeProjA hM P_A a0).toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ + √(MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)

The first player's repaired line-169 consistency after completing the projective submeasurement.

This is the two-space analogue of the paper's Q^A_g ⊗ I ≃ I ⊗ G^B_g step, with the checked repaired loss ζ + √(orthonormalizationError ζ).

theorem MIPRE.LIDT.Co.ProjStrat.completedRightConsistency_of_consistency_and_sdd {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) {Outcome : Type u_4} [Fintype Outcome] (hψ : ‖M.ψ‖ = 1) (hM : M.IsFinitePair) (ζ : ℝ) (G_A : Measurement Outcome 𝒜) (G_B : Measurement Outcome ℬ) (P_B : ProjSubMeas Outcome ℬ) (a0 : Outcome) (hpre : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (horth : (TwoSpace.vecState M hψ).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas M P_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) : bipartiteConsError M (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily (TwoSpace.completeAtOutcomeProjB hM P_B a0).toSubMeas) ≤ ζ + √(MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)

The second player's repaired line-169 consistency after completing the projective submeasurement: the two-space analogue of the role-reversed relation G^A_g ⊗ I ≃ I ⊗ Q^B_g.

The strategy-level theorems

theorem MIPRE.LIDT.Co.ProjStrat.completedProjectiveMeasurements_ofTwoSidedSubmeasurements {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) (G_A : Measurement (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : Measurement (MIPStarRE.LDT.Polynomial params) ℬ) (P_A : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (P_B : ProjSubMeas (MIPStarRE.LDT.Polynomial params) ℬ) (ζ : ℝ) (hfull : bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (hleft : (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state P_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) (hright : (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state P_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) : ∃ (Q_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (Q_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state Q_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ) ∧ (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state Q_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)

Complete the two projective submeasurements obtained after the line-130 cross-consistency estimate to projective measurements, with the placed state-dependent-distance estimates the paper requires.

Paper origin: references/ldt-paper/inductive_step.tex:143-149. Consistency bounds the mass missing from each projective submeasurement once the orthonormalization distance is charged by Cauchy–Schwarz, and the completion residual contributes at most that mass.

theorem MIPRE.LIDT.Co.ProjStrat.completedProjectiveMeasurementsAndLine169_ofTwoSidedSubmeasurements {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsFinitePair) (G_A : Measurement (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : Measurement (MIPStarRE.LDT.Polynomial params) ℬ) (P_A : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (P_B : ProjSubMeas (MIPStarRE.LDT.Polynomial params) ℬ) (ζ : ℝ) (hfull : bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (hleft : (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state P_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) (hright : (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state P_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)) : ∃ (Q_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (Q_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state Q_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ) ∧ (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state Q_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily Q_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ + √(MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily Q_B.toSubMeas) ≤ ζ + √(MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ)

Complete the two projective submeasurements and derive the two repaired polynomial line-169 consistency relations.

Paper origin: references/ldt-paper/inductive_step.tex:167-172. The paper applies triangle-sub after the completion estimates; the statement here is the checked repaired version, in which the replacement of G_A by Q_A and of G_B by Q_B is charged directly from the pre-completion orthonormalization distance, giving the error ζ + √(orthonormalizationError ζ).

theorem MIPRE.LIDT.Co.ProjStrat.completedProjectiveConsistency_ofFullConsistency {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (G_A : Measurement (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : Measurement (MIPStarRE.LDT.Polynomial params) ℬ) (Q_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (Q_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ) (ζ : ℝ) (hfull : bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ) (hleftComplete : (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state G_A.toSubMeas)) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state Q_A.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)) (hrightComplete : (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state G_B.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state Q_B.toSubMeas)) (MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)) : have ζ₂ := MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ; (TwoSpace.vecState strategy.state ⋯).SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (TwoSpace.leftPlacedSubMeas strategy.state Q_A.toSubMeas)) (constSubMeasFamily (TwoSpace.rightPlacedSubMeas strategy.state Q_B.toSubMeas)) (6 * ζ + 6 * ζ₂)

The line-156 projective consistency estimate after completing both polynomial submeasurements.

Paper origin: references/ldt-paper/inductive_step.tex:150-157. The consistency of G_A, G_B gives the distance 2ζ of their placements (TwoSpace.simeqToApprox_heterogeneous), which telescopes through the two completion-distance estimates for Q_A and Q_B.