Source-Boundary Role-Register Handoff: Completion Lemmas

This module contains the completion and line-169 transport lemmas for the two-space source role-register route.

theorem MIPStarRE.LDT.ProjStrat.completedProjectiveMeasurements_ofTwoSidedSubmeasurements (params : Parameters) [FieldModel params.q] {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) (G_A : Measurement (Polynomial params) ιA) (G_B : Measurement (Polynomial params) ιB) (P_A : ProjSubMeas (Polynomial params) ιA) (P_B : ProjSubMeas (Polynomial params) ιB) (ζ : Error) (hfull : ConsRel strategy.state (uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ζ) (hleft : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas G_A.toSubMeas)) (constSubMeasFamily (leftPlacedSubMeas P_A.toSubMeas)) (MakingMeasurementsProjective.orthonormalizationError ζ)) (hright : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (rightPlacedSubMeas G_B.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas P_B.toSubMeas)) (MakingMeasurementsProjective.orthonormalizationError ζ)) : ∃ (Q_A : ProjMeas (Polynomial params) ιA) (Q_B : ProjMeas (Polynomial params) ιB), SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas G_A.toSubMeas)) (constSubMeasFamily (leftPlacedSubMeas Q_A.toSubMeas)) (MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (rightPlacedSubMeas G_B.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas Q_B.toSubMeas)) (MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)

Complete two projective submeasurements obtained after the line-130 cross-consistency estimate to projective measurements, with the tensor-factor state-dependent-distance estimates required by the paper.

Paper origin: references/ldt-paper/inductive_step.tex:143-149. The proof is the standard completion argument: consistency bounds the total mass missing from the projective submeasurement after the orthonormalization-distance loss is charged by Cauchy--Schwarz, and the completion residual then contributes at most this missing mass.

theorem MIPStarRE.LDT.ProjStrat.completedProjectiveMeasurementsAndLine169_ofTwoSidedSubmeasurements (params : Parameters) [FieldModel params.q] {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) (G_A : Measurement (Polynomial params) ιA) (G_B : Measurement (Polynomial params) ιB) (P_A : ProjSubMeas (Polynomial params) ιA) (P_B : ProjSubMeas (Polynomial params) ιB) (ζ : Error) (hfull : ConsRel strategy.state (uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ζ) (hleft : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas G_A.toSubMeas)) (constSubMeasFamily (leftPlacedSubMeas P_A.toSubMeas)) (MakingMeasurementsProjective.orthonormalizationError ζ)) (hright : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (rightPlacedSubMeas G_B.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas P_B.toSubMeas)) (MakingMeasurementsProjective.orthonormalizationError ζ)) : ∃ (Q_A : ProjMeas (Polynomial params) ιA) (Q_B : ProjMeas (Polynomial params) ιB), SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas G_A.toSubMeas)) (constSubMeasFamily (leftPlacedSubMeas Q_A.toSubMeas)) (MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ) ∧ SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (rightPlacedSubMeas G_B.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas Q_B.toSubMeas)) (MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ) ∧ ConsRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Q_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) (ζ + √(MakingMeasurementsProjective.orthonormalizationError ζ)) ∧ ConsRel strategy.state (uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily Q_B.toSubMeas) (ζ + √(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 formal statement uses the checked repaired version: 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 ζ + sqrt (orthonormalizationError ζ).

theorem MIPStarRE.LDT.ProjStrat.completedProjectiveConsistency_ofFullConsistency (params : Parameters) [FieldModel params.q] {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (strategy : ProjStrat params ιA ιB) (G_A : Measurement (Polynomial params) ιA) (G_B : Measurement (Polynomial params) ιB) (Q_A : ProjMeas (Polynomial params) ιA) (Q_B : ProjMeas (Polynomial params) ιB) (ζ : Error) (hfull : ConsRel strategy.state (uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ζ) (hleftComplete : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas G_A.toSubMeas)) (constSubMeasFamily (leftPlacedSubMeas Q_A.toSubMeas)) (MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)) (hrightComplete : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (rightPlacedSubMeas G_B.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas Q_B.toSubMeas)) (MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ)) : have ζ₂ := MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ; SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas Q_A.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas 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 proof uses the consistency-to-distance implication for G_A,G_B, then telescopes through the two completion-distance estimates for Q_A and Q_B.