Section 6 — Self-improvement error bounds

The scalar consequences of the non-vacuous hypothesis selfImprovementInInductionError ≤ 1 for a good strategy, namely the bounds eps ≤ 1 and delta ≤ 1 used before applying self-improvement inside the induction step. This is the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/InductionParameterBounds/SelfImprovement.lean in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").

Translation

Two declarations read a strategy and are ported, for a good SymStrat params.next 𝔓 K (Co/Test/StrategyCore.lean). A strategy enters only through the nonnegativity of eps and delta that its IsGood gives (eps_nonneg_of_isGood, delta_nonneg_of_isGood of Co/Test/StrategyFailures.lean). No lemma of the file has a swap, density or normalization hypothesis, so none is dropped, and no declaration takes a new hypothesis. The other two declarations are arithmetic on the classical error function selfImprovementInInductionError: this file imports the vendored file and names them through an explicit open MIPStarRE.LDT.MainInductionStep (…) list. The vendored file's only import is the vendored InductionParameterBounds/Preliminaries, which the ported Preliminaries already imports, so importing it adds no operator content. The vendored file-wide respectTransparency false is not needed: the file sets no option.

Proofs that differ from the vendored ones

The scaled bound 3000 · m_next · x^{1/32} ≤ selfImprovementInInductionError params.next … is proved by mul_le_mul_of_nonneg_left on the unfolded error, with linarith for the summand comparison, in place of the vendored simpa with commutativity lemmas around selfImprovementInInduction_scaled_component_le.

Not ported

• selfImprovementInInduction_scaled_component_le: classical, imported.

References

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

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

theorem MIPRE.LIDT.Co.MainInductionStep.le_one_of_selfImprovementInInductionError_le_one_of_scaled_bound (params : MIPStarRE.LDT.Parameters) {eps delta gamma x : ℝ} (hzeta_le : MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError params.next eps delta gamma ≤ 1) (hscaled_le : 3000 * ↑params.next.m * x.rpow (1 / 32) ≤ MIPStarRE.LDT.MainInductionStep.selfImprovementInInductionError params.next eps delta gamma) : x ≤ 1

Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.

theorem MIPRE.LIDT.Co.MainInductionStep.eps_le_one_of_selfImprovementInInductionError_le_one {𝔓 : 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.next 𝔓 K) {eps delta gamma : ℝ} (hgood : strategy.IsGood eps delta gamma) (hzeta_le : MIPStarRE.LDT.MainInductionStep.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 MIPRE.LIDT.Co.MainInductionStep.delta_le_one_of_selfImprovementInInductionError_le_one {𝔓 : 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.next 𝔓 K) {eps delta gamma : ℝ} (hgood : strategy.IsGood eps delta gamma) (hzeta_le : MIPStarRE.LDT.MainInductionStep.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.