Source-boundary role-register handoff: final point consistency

The final completed-measurement and point-consistency statements of the two-space route toward thm:main-formal: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Test/MainTheorem/SourceRoleRegister/Final.lean in the port of planning/c6b-plan.md (milestone M13, section "Port conventions").

The strategy is two-space, as in Co SourceRoleRegister/Core and Completion: strategy : ProjStrat params 𝒞 𝒜 ℬ has the bipartite model strategy.state with unit vector strategy.isNormalized, and the translation is that of Co/Test/MainTheorem/TwoSpace.lean:

• the vendored ConsRel strategy.state 𝒟 A B δ is bipartiteConsError strategy.state 𝒟 A B ≤ δ;
• SDDRel strategy.state 𝒟 (leftPlacedSubMeas G) … is (TwoSpace.vecState strategy.state strategy.isNormalized).SDDRel 𝒟 (TwoSpace.leftPlacedSubMeas strategy.state G) …, and the right forms likewise;
• the vendored Preliminaries.{approxToSimeq, simeqToApprox, simeqTriangleInequality, triangleSub}_heterogeneous on the two-space state are their TwoSpace forms, and the same-space sddRel_symm, stateDependentDistanceRel_triangle and _mono are applied to TwoSpace.vecState strategy.state strategy.isNormalized with both families explicit. The measurements are Measurement, ProjSubMeas and ProjMeas of MIPStarRE.LDT.Polynomial params in 𝒜 (Alice) and ℬ (Bob). The errors σ, ζ₁, ζ₂, η, ζ₃ are the vendored ones.

Departure: new hypotheses. Every theorem takes (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) right after strategy, as Co sourceRoleRegisterCompletePolynomialSelfConsistency does: the main induction runs in the doubled model of a dyadic pair and needs 1 ≤ params.d (milestone M12's threaded hS hA hd), and the two-space orthonormalizations of Co Core need hM and ζ₁ > 0. The latter is the only other use of hd: σ ≥ 0, being an upper bound of a nonnegative defect, and m d / q > 0 when 1 ≤ d (zeta₁_pos); it replaces the vendored derivation of 0 ≤ ζ₁ inside the orthonormalization lemma. The completion of Co Completion takes hM.isFinitePair. No statement carries a swap, density or normalization hypothesis.

Departure: imports. The vendored file imports SourceRoleRegister/Completion, which imports Core; Co Completion does not import Co Core, so this file imports both.

Not ported

Every declaration of the vendored file has a counterpart here, with the new hypotheses hM and hd above.

theorem MIPRE.LIDT.Co.ProjStrat.sourceRoleRegisterLeftProjectiveSubmeasurement {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : ∃ (G_A : Measurement (MIPStarRE.LDT.Polynomial params) 𝒜) (G_B : Measurement (MIPStarRE.LDT.Polynomial params) ℬ) (P_A : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝒜), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) + 2 * √(3 * eps + 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps)) + ↑params.m * ↑params.d / ↑params.q ∧ (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 (2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) + 2 * √(3 * eps + 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps)) + ↑params.m * ↑params.d / ↑params.q))

Alice-side projective submeasurement from the source role-register route.

It combines the source role-register Step 5 theorem (sourceRoleRegisterCompletePolynomialSelfConsistency) with the two-space orthonormalization (sourceRoleRegisterLeftProjectiveSubmeasurement_ofFullConsistency), and constructs only the Alice-side projective submeasurement with its left-factor state-dependent-distance estimate.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

theorem MIPRE.LIDT.Co.ProjStrat.sourceRoleRegisterTwoSidedProjectiveSubmeasurements {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : ∃ (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) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) + 2 * √(3 * eps + 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps)) + ↑params.m * ↑params.d / ↑params.q ∧ (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 (2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) + 2 * √(3 * eps + 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps)) + ↑params.m * ↑params.d / ↑params.q)) ∧ (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 (2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps) + 2 * √(3 * eps + 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps)) + ↑params.m * ↑params.d / ↑params.q))

Two-sided projective submeasurements from the source role-register route.

It combines the source role-register Step 5 theorem with the two-space orthonormalizations on both factors, constructing the projective submeasurements P_A, P_B and the two state-dependent-distance estimates; completion and the line-169 transport come after.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

theorem MIPRE.LIDT.Co.ProjStrat.sourceRoleRegisterCompletedProjectiveMeasurements {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : have σ := 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps); have ζ₁ := σ + 2 * √(3 * eps + σ) + ↑params.m * ↑params.d / ↑params.q; ∃ (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) ℬ) (Q_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (Q_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params G_B.toSubMeas) ≤ σ ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params G_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ σ ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily G_A.toSubMeas) (constSubMeasFamily G_B.toSubMeas) ≤ ζ₁ ∧ (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 ζ₁) ∧ (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 ζ₁) ∧ (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 ζ₁)

Completed projective measurements from the source role-register route.

Paper origin: references/ldt-paper/inductive_step.tex:143-149. From the two-space strategy it constructs the complete polynomial measurements G_A, G_B, the projective submeasurements P_A, P_B and the completed projective measurements Q_A, Q_B (completedProjectiveMeasurementsAndLine169_ofTwoSidedSubmeasurements), with the two state-dependent-distance estimates at the orthonormalize-and-complete error and the repaired line-169 polynomial consistencies.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.

theorem MIPRE.LIDT.Co.ProjStrat.sourceRoleRegisterFinalPointConsistency {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] {ℬ : Type u_3} [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : ProjStrat params 𝒞 𝒜 ℬ) (hM : strategy.state.IsDyadicPair) (hd : 1 ≤ params.d) (eps : ℝ) (hpass : strategy.PassesLowIndividualDegreeTest eps) (k : ℕ) (hk : 400 * params.m * params.d ≤ k) : have σ := 2 * MIPStarRE.LDT.MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps); have ζ₁ := σ + 2 * √(3 * eps + σ) + ↑params.m * ↑params.d / ↑params.q; have ζ₂ := MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizeAndCompleteError ζ₁; have η := ζ₁ + √(MIPStarRE.LDT.MakingMeasurementsProjective.orthonormalizationError ζ₁); have ζ₃ := 6 * ζ₁ + 6 * ζ₂; ∃ (Q_A : ProjMeas (MIPStarRE.LDT.Polynomial params) 𝒜) (Q_B : ProjMeas (MIPStarRE.LDT.Polynomial params) ℬ), bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurementA.toIdxSubMeas (polynomialEvaluationFamily params Q_B.toSubMeas) ≤ σ + 2 * √(η + ζ₃ / 2) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params Q_A.toSubMeas) strategy.pointMeasurementB.toIdxSubMeas ≤ σ + 2 * √(η + ζ₃ / 2) ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (polynomialEvaluationFamily params Q_A.toSubMeas) (polynomialEvaluationFamily params Q_B.toSubMeas) ≤ ζ₃ / 2 ∧ bipartiteConsError strategy.state (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily Q_A.toSubMeas) (constSubMeasFamily Q_B.toSubMeas) ≤ ζ₃ / 2

Final point-consistency estimates of the source role-register route, before scalar absorption.

Paper origin: references/ldt-paper/inductive_step.tex:158-185. No point-consistency estimate is assumed: the line-169 polynomial consistencies of (Q_A, G_B) and (G_A, Q_B) are evaluated at the sampled point (Test.consRel_constPolynomialEvaluation_heterogeneous), the (Q_A, Q_B) consistency comes from the line-156 distance ζ₃ (completedProjectiveConsistency_ofFullConsistency, then Test.projectiveEvaluationConsistency_ofFullPolynomialConsistency_heterogeneous and TwoSpace.approxToSimeq_heterogeneous), and the two point estimates are the two-space triangle inequalities TwoSpace.simeqTriangleInequality_heterogeneous (Alice) and TwoSpace.triangleSub_heterogeneous (Bob). The errors are the literal ones these produce.

Departure: the hypotheses hM : strategy.state.IsDyadicPair and hd : 1 ≤ params.d are new.