Section 6 — Self-Improvement Error Bounds

This file is one leaf of InductionParameterBounds. It contains the scalar consequences of the non-vacuous hypothesis selfImprovementInInductionError ≤ 1, namely the bounds eps ≤ 1 and delta ≤ 1 used before applying self-improvement inside the induction step.

References

• blueprint/src/chapter/ch10_induction.tex
• references/ldt-paper/inductive_step.tex

theorem MIPStarRE.LDT.MainInductionStep.eps_le_one_of_selfImprovementInInductionError_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) (hzeta_le : selfImprovementInInductionError params.next eps delta gamma ≤ 1) : eps ≤ 1

Internal helper: under selfImprovementInInductionError ≤ 1, the axis-parallel error eps ≤ 1.

Exposed for cross-module use in AvgSliceErrors and PastingAssembly.

theorem MIPStarRE.LDT.MainInductionStep.delta_le_one_of_selfImprovementInInductionError_le_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} (hgood : strategy.IsGood eps delta gamma) (hzeta_le : selfImprovementInInductionError params.next eps delta gamma ≤ 1) : delta ≤ 1

Internal helper: under selfImprovementInInductionError ≤ 1, the self-consistency error delta ≤ 1.

Exposed for cross-module use in AvgSliceErrors and PastingAssembly.