Boundedness transport literal point-consistency estimates

The literal-threshold point-consistency transports, at selfImprovementError, obtained from the natural-error estimates of BoundednessTransport/PointConsistency.lean: the counterpart of the vendored SelfImprovement/Theorems/Results/BoundednessTransport/PointConsistencyLiteral.lean (under MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10, section "Port conventions").

Contents

• final_fields_point_consistency_totalGap and …_totalGap_of_total_difference: the natural error with an explicit total-overlap displacement η, absorbed into selfImprovementError under a numerical hypothesis.
• final_fields_point_consistency_natural_of_total_le, …_of_total_expectation_le and …_of_total_operator_le: the natural error when the projective replacement has no larger right total (pointwise, as one scalar, or as an operator inequality).
• final_fields_point_consistency_of_total_expectation_le_of_small_errors, …_of_total_operator_le_of_small_errors and …_totalGap_of_data_processing: the same at selfImprovementError, through the classical absorption final_fields_projective_residual_error_le_selfImprovementError of the vendored Thresholds/Final.lean.

The translation is that of BoundednessTransport/PointConsistency.lean. The vendored sddRel_liftRight_of_liftLeft_permInv strategy.permInvState … is M8's MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv strategy.state …, and the vendored strategy.isNormalized argument of Preliminaries.triangleSub_right_subMeas_total_le is dropped, the ported lemma taking none. No statement of the vendored file carries a swap, density or normalization hypothesis, so no statement changed; the file sets no option, the vendored file-wide respectTransparency false not being needed. The error constants (selfImprovementHelperError, selfImprovementDataProcessingError, selfImprovementError) are the vendored classical ones.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/self_improvement.tex lines 747--755
• blueprint/src/chapter/ch07_self_improvement.tex

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_totalGap {𝔓 : 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 η : ℝ) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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 : (MIPStarRE.LDT.avgOver (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) fun (u : MIPStarRE.LDT.Point params) => |strategy.state.ev (strategy.state.L (strategy.pointMeasurement.toIdxSubMeas u).total * strategy.state.R (polynomialEvaluationFamily params H.toSubMeas u).total) - strategy.state.ev (strategy.state.L (strategy.pointMeasurement.toIdxSubMeas u).total * strategy.state.R (polynomialEvaluationFamily params Hhat u).total)|) ≤ η) (habsorb : MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta + √(MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError params eps delta) + η ≤ MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

Literal-threshold point-consistency transport from the helper output to the projective output.

This theorem isolates the numerical absorption needed to turn the natural error selfImprovementHelperError + sqrt selfImprovementDataProcessingError + η into the final selfImprovementError threshold. The analytic content is contained in final_fields_point_consistency_totalGap_natural.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_totalGap_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 η : ℝ) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

Literal-threshold point-consistency transport from a right-register total difference bound.

This is the selfImprovementError-absorbed companion to final_fields_point_consistency_totalGap_natural_of_total_difference.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_natural_of_total_le {𝔓 : 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 : ℝ) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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)) (hTotalLe : ∀ (u : MIPStarRE.LDT.Point params), strategy.state.ev (strategy.state.L (strategy.pointMeasurement.toIdxSubMeas u).total * strategy.state.R (polynomialEvaluationFamily params H.toSubMeas u).total) ≤ strategy.state.ev (strategy.state.L (strategy.pointMeasurement.toIdxSubMeas u).total * strategy.state.R (polynomialEvaluationFamily params Hhat u).total)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta + √(MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError params eps delta))

Natural-error point-consistency transport under monotone total overlap.

If the projective replacement has no larger right-register total overlap with the point measurement than the helper submeasurement, then the submeasurement triangle argument is at the paper-natural error threshold selfImprovementHelperError + sqrt selfImprovementDataProcessingError.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_natural_of_total_expectation_le {𝔓 : 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 : ℝ) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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)) (hTotalLe : strategy.state.ev (strategy.state.R H.total) ≤ strategy.state.ev (strategy.state.R Hhat.total)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta + √(MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError params eps delta))

Natural-error point-consistency transport from a scalar right-total monotonicity hypothesis.

Since the point measurement is complete and postprocessing preserves total operators, this monotonicity condition is equivalent to a single scalar comparison of right-register expectations.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_of_total_expectation_le_of_small_errors {𝔓 : 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 : ℝ) (heps : 0 ≤ eps) (heps_le_one : eps ≤ 1) (hdelta : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hd_le_q : ↑params.d ≤ ↑params.q) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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)) (hTotalLe : strategy.state.ev (strategy.state.R H.total) ≤ strategy.state.ev (strategy.state.R Hhat.total)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

Literal-threshold point-consistency transport from scalar right-total monotonicity and the standard small-error hypotheses.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_natural_of_total_operator_le {𝔓 : 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 : ℝ) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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)) (hTotalLe : H.total ≤ Hhat.total) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError params eps delta + √(MIPStarRE.LDT.SelfImprovement.selfImprovementDataProcessingError params eps delta))

Natural-error point-consistency transport from operator right-total monotonicity.

The operator inequality H.total ≤ Hhat.total implies the scalar right-total comparison after placing both operators on the right tensor factor and taking expectation in the shared state.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_of_total_operator_le_of_small_errors {𝔓 : 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 : ℝ) (heps : 0 ≤ eps) (heps_le_one : eps ≤ 1) (hdelta : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hd_le_q : ↑params.d ≤ ↑params.q) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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)) (hTotalLe : H.total ≤ Hhat.total) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

Literal-threshold point-consistency transport from operator right-total monotonicity and the standard small-error hypotheses.

This is the operator-order version of final_fields_point_consistency_of_total_expectation_le_of_small_errors.

theorem MIPRE.LIDT.Co.SelfImprovement.final_fields_point_consistency_totalGap_of_data_processing {𝔓 : 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 : ℝ) (heps : 0 ≤ eps) (heps_le_one : eps ≤ 1) (hdelta : 0 ≤ delta) (hdelta_le_one : delta ≤ 1) (hd_le_q : ↑params.d ≤ ↑params.q) {Hhat : SubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} {H : ProjSubMeas (MIPStarRE.LDT.Polynomial params) 𝔓} (hhelperPoint : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError 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)) (hTotalLe : strategy.state.ev (strategy.state.R H.total) ≤ strategy.state.ev (strategy.state.R Hhat.total)) : strategy.state.ConsRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (MIPStarRE.LDT.SelfImprovement.selfImprovementError params eps delta)

Literal-threshold point-consistency transport with the data-processing estimate.

This is the theorem required by upstream issue #1240. The remaining analytical route is carried by final_fields_point_consistency_natural_of_total_le and the standard small-error absorption bound; no additional sqrt (#F_q * selfImprovementDataProcessingError) term is absorbed here.