Final-fields assembly routes

The final-fields assembler of the projective self-improvement theorem: the completeness, point-consistency, self-closeness and projective-residual constructions combined into SelfImprovementFinalFields, with the total-difference route for the point-consistency field. The counterpart of the vendored SelfImprovement/Theorems/Results/SelfImprovementTop/FinalFields.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

Contents

• final_fields_of_helper_outputs_of_total_difference: SelfImprovementFinalFields from the helper outputs, the orthonormalization SDD bound, the data-processing bound and a scalar bound on the difference of the right totals.

The theorem takes the orthonormalization SDD bound as a hypothesis and calls no orthonormalization, so it carries no finite-pair, abelian-projection or ζ > 0 hypothesis.

The translation is that of BoundednessTransport/BoundednessGap.lean: a strategy is a SymStrat params 𝔓 K, Z : MIPStarRE.Quantum.Op ι is Z : 𝔓, A.liftLeft is A.liftLeft strategy.state, (F).liftLeft on a family is IdxSubMeas.liftLeft strategy.state F, ev strategy.state (rightTensor (ι₁ := ι) X) is strategy.state.ev (strategy.state.R X), the relations are read on strategy.state, and Error is ℝ. The hypothesis hslack (SDP complementary slackness, T_h A_h = T_h Z for every h) is passed through, of unchanged shape. No statement of the vendored file carries a swap, density or normalization hypothesis, so the statement changed only by the translation, and the proof is the vendored one over the ported pieces; the file sets no option, the vendored file-wide respectTransparency false not being needed. The imports mirror the vendored ones.

Not ported

Every declaration of the vendored file has a counterpart here.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_of_helper_outputs_of_total_difference {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params 𝔓 K) (eps delta nu η : ℝ) (heps : 0 ≤ eps) (heps_le_one : eps ≤ 1) (hdelta : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hd_le_q : ↑params.d ≤ ↑params.q) {T : Measurement (MIPStarRE.LDT.Polynomial params) 𝔓} {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {Z : 𝔓} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hhelperCompleteness : strategy.state.CompletenessAtLeast (SubMeas.liftLeft strategy.state Hhat) (1 - nu - MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)) (hhelperSSC : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta)) (hpointSSC : strategy.state.BipartiteSSCRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas delta) (hslack : ∀ (h : MIPStarRE.LDT.Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) (htransfer : |addInULeftQuantity params strategy strategy.pointMeasurement.toIdxSubMeas Hhat (MIPStarRE.LDT.SelfImprovement.pointConsistencyAddInUSelection params) - addInURightQuantity params strategy strategy.pointMeasurement.toIdxSubMeas T.toSubMeas (MIPStarRE.LDT.SelfImprovement.pointConsistencyAddInUSelection params)| ≤ MIPStarRE.LDT.SelfImprovement.addInUError params eps delta) (horth : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution Unit) (constSubMeasFamily (SubMeas.liftLeft strategy.state Hhat)) (constSubMeasFamily (SubMeas.liftLeft strategy.state H.toSubMeas)) (MIPStarRE.LDT.SelfImprovement.selfImprovementOrthogonalizationError params eps delta)) (hdata : strategy.state.SDDRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) (IdxSubMeas.liftLeft strategy.state (polynomialEvaluationFamily params Hhat)) (IdxSubMeas.liftLeft strategy.state (polynomialEvaluationFamily params H.toSubMeas)) (MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError params eps delta)) (hTotal : |strategy.state.ev (strategy.state.R H.total) - strategy.state.ev (strategy.state.R Hhat.total)| ≤ η) (habsorb : MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta + √(MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError params eps delta) + η ≤ MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta) : SelfImprovementFinalFields params strategy H Z eps delta nu

Final-fields construction using an explicit right-total-difference bound.

This is the submeasurement-total fallback for the point-consistency field. When the proof supplies only a scalar bound on |⟨ψ, I ⊗ H.total⟩ - ⟨ψ, I ⊗ Hhat.total⟩|, rather than the monotonicity ⟨ψ, I ⊗ H.total⟩ ≤ ⟨ψ, I ⊗ Hhat.total⟩, the point-consistency field is assembled through final_fields_point_consistency_totalGap_of_total_difference. The other fields are the completeness, self-closeness and projective-residual constructions.