Final-fields assembly routes

This module contains the final-fields assemblers used in the projective self-improvement theorem. It combines the already isolated completeness, point-consistency, self-closeness, and projective-residual constructions into SelfImprovementFinalFields, using the total-difference route for the point-consistency field.

theorem MIPStarRE.LDT.SelfImprovement.final_fields_of_helper_outputs_of_total_difference {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta nu η : Error) (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 (Polynomial params) ι} {Hhat : SubMeas (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} {Z : Quantum.Op ι} (hhelper : SelfImprovementHelperConclusion params strategy T Hhat Z eps delta) (hhelperCompleteness : CompletenessAtLeast strategy.state Hhat.liftLeft (1 - nu - selfImprovementHelperError params eps delta)) (hhelperSSC : BipartiteSSCRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Hhat) (selfImprovementHelperError params eps delta)) (hpointSSC : BipartiteSSCRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas delta) (hslack : ∀ (h : Polynomial params), T.outcome h * averagedPointOperator params strategy h = T.outcome h * Z) (htransfer : |addInULeftQuantity params strategy strategy.pointMeasurement.toIdxSubMeas Hhat (pointConsistencyAddInUSelection params) - addInURightQuantity params strategy strategy.pointMeasurement.toIdxSubMeas T.toSubMeas (pointConsistencyAddInUSelection params)| ≤ addInUError params eps delta) (horth : SDDRel strategy.state (uniformDistribution Unit) (constSubMeasFamily Hhat.liftLeft) (constSubMeasFamily H.liftLeft) (selfImprovementOrthogonalizationError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotal : |ev strategy.state (rightTensor H.total) - ev strategy.state (rightTensor Hhat.total)| ≤ η) (habsorb : selfImprovementHelperError params eps delta + √(selfImprovementDataProcessingError params eps delta) + η ≤ 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 monotonicity ⟨ψ, I ⊗ H.total⟩ ≤ ⟨ψ, I ⊗ Hhat.total⟩, the point-consistency field is assembled through final_fields_point_consistency_totalGap_of_total_difference. The remaining fields are unchanged.