Boundedness transport literal point-consistency estimates

This file contains the literal-threshold point-consistency transports obtained from the natural-error estimates in BoundednessTransport/PointConsistency.lean.

References

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

theorem MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_totalGap {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta η : Error) {Hhat : SubMeas (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotal : (avgOver (uniformDistribution (Point params)) fun (u : Point params) => |ev strategy.state (leftTensor (strategy.pointMeasurement.toIdxSubMeas u).total * rightTensor (polynomialEvaluationFamily params H.toSubMeas u).total) - ev strategy.state (leftTensor (strategy.pointMeasurement.toIdxSubMeas u).total * rightTensor (polynomialEvaluationFamily params Hhat u).total)|) ≤ η) (habsorb : selfImprovementHelperError params eps delta + √(selfImprovementDataProcessingError params eps delta) + η ≤ selfImprovementError params eps delta) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (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 MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_totalGap_of_total_difference {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta η : Error) {Hhat : SubMeas (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError 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) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (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 MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_natural_of_total_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) {Hhat : SubMeas (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotalLe : ∀ (u : Point params), ev strategy.state (leftTensor (strategy.pointMeasurement.toIdxSubMeas u).total * rightTensor (polynomialEvaluationFamily params H.toSubMeas u).total) ≤ ev strategy.state (leftTensor (strategy.pointMeasurement.toIdxSubMeas u).total * rightTensor (polynomialEvaluationFamily params Hhat u).total)) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementHelperError params eps delta + √(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 MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_natural_of_total_expectation_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) {Hhat : SubMeas (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotalLe : ev strategy.state (rightTensor H.total) ≤ ev strategy.state (rightTensor Hhat.total)) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementHelperError params eps delta + √(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 MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_of_total_expectation_le_of_small_errors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (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 (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotalLe : ev strategy.state (rightTensor H.total) ≤ ev strategy.state (rightTensor Hhat.total)) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementError params eps delta)

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

theorem MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_natural_of_total_operator_le {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) {Hhat : SubMeas (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotalLe : H.total ≤ Hhat.total) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementHelperError params eps delta + √(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 MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_of_total_operator_le_of_small_errors {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (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 (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotalLe : H.total ≤ Hhat.total) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (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 MIPStarRE.LDT.SelfImprovement.final_fields_point_consistency_totalGap_of_data_processing {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta : Error) (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 (Polynomial params) ι} {H : ProjSubMeas (Polynomial params) ι} (hhelperPoint : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params Hhat) (selfImprovementHelperError params eps delta)) (hdata : SDDRel strategy.state (uniformDistribution (Point params)) (polynomialEvaluationFamily params Hhat).liftLeft (polynomialEvaluationFamily params H.toSubMeas).liftLeft (selfImprovementDataProcessingError params eps delta)) (hTotalLe : ev strategy.state (rightTensor H.total) ≤ ev strategy.state (rightTensor Hhat.total)) : ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas (polynomialEvaluationFamily params H.toSubMeas) (selfImprovementError params eps delta)

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

This is the theorem required by #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.