Section 9 — helper-stage numerical threshold absorptions

Reusable arithmetic threshold lemmas that compare the natural paper sums of errors emitted by the helper-stage self-improvement constructions against the literal selfImprovementHelperError threshold used by the final-field statements (SelfImprovementFinalFields in Statements.lean).

The helper-stage absorptions formalize the displayed paper inequalities:

• references/ldt-paper/self_improvement.tex, lines 438--443 — point consistency: 4 √ζ_var ≤ ζ̂.
• references/ldt-paper/self_improvement.tex, lines 595--603 — strong self-consistency: 11 √ζ_var + √(2δ) + md/q ≤ ζ̂.
• references/ldt-paper/self_improvement.tex, lines 403--414 — completeness: 3 √δ ≤ ζ̂.
• references/ldt-paper/self_improvement.tex, lines 614--624 — boundedness: 3 √δ + 4 √ζ_var ≤ ζ̂.

The final-stage comparisons with selfImprovementError are collected in Thresholds.Final.

Blueprint mirrors:

• blueprint/src/chapter/ch07_self_improvement.tex, lines 161--168 (point consistency) and 256--279 (strong self-consistency / boundedness).

Parameter convenience facts

theorem MIPStarRE.LDT.SelfImprovement.one_le_m_cast (params : Parameters) : 1 ≤ ↑params.m

The parameter m is at least one, viewed in the error scalar field.

theorem MIPStarRE.LDT.SelfImprovement.m_cast_nonneg (params : Parameters) : 0 ≤ ↑params.m

The parameter m, viewed in the error scalar field, is nonnegative.

theorem MIPStarRE.LDT.SelfImprovement.d_q_ratio_nonneg (params : Parameters) : 0 ≤ ↑params.d / ↑params.q

The ratio d/q, viewed in the error scalar field, is nonnegative.

theorem MIPStarRE.LDT.SelfImprovement.d_q_ratio_le_one_of_d_le_q (params : Parameters) (hd_le_q : ↑params.d ≤ ↑params.q) : ↑params.d / ↑params.q ≤ 1

If d ≤ q, then the ratio d/q is at most one.

theorem MIPStarRE.LDT.SelfImprovement.sqrt_100m_le_10m (params : Parameters) : √(100 * ↑params.m) ≤ 10 * ↑params.m

For m ≥ 1, √(100m) ≤ 10m.

theorem MIPStarRE.LDT.SelfImprovement.sqrt_10m_le_4m (params : Parameters) : √(10 * ↑params.m) ≤ 4 * ↑params.m

For m ≥ 1, √(10m) ≤ 4m.

theorem MIPStarRE.LDT.SelfImprovement.sqrt_400m_le_20m (params : Parameters) : √(400 * ↑params.m) ≤ 20 * ↑params.m

For m ≥ 1, √(400m) ≤ 20m.

theorem MIPStarRE.LDT.SelfImprovement.sqrt_960m_le_31m (params : Parameters) : √(960 * ↑params.m) ≤ 31 * ↑params.m

For m ≥ 1, √(960m) ≤ 31m.

Subroutine: square-root bound on globalVarianceOfPointsError

The paper's central arithmetic step (self_improvement.tex, line 441) is

√(24 m (ε + δ + md/q)) ≤ 20 m (ε^{1/2} + δ^{1/2} + (d/q)^{1/2}).

We separate the constant 5 from the multipliers 4/11/3 used downstream and prove a single reusable bound.

theorem MIPStarRE.LDT.SelfImprovement.selfImprovementVarianceError_eq (params : Parameters) [FieldModel params.q] (eps delta : Error) : selfImprovementVarianceError params eps delta = 24 * ↑params.m * (eps + delta + ↑params.m * (↑params.d / ↑params.q))

Expansion of the variance error into the three residuals appearing in the self-improvement paper.

The final summand is written as m * (d / q), rather than (m * d) / q, so that square-root estimates may split the last product directly.

theorem MIPStarRE.LDT.SelfImprovement.sqrt_selfImprovementVarianceError_le (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) : √(selfImprovementVarianceError params eps delta) ≤ 5 * ↑params.m * (√eps + √delta + √(↑params.d / ↑params.q))

Paper-faithful square-root bound on the variance error (self_improvement.tex, lines 440--442).

theorem MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError_eq (params : Parameters) [FieldModel params.q] (eps delta : Error) : selfImprovementHelperError params eps delta = 100 * ↑params.m * (√eps + √delta + √(↑params.d / ↑params.q))

Expansion of the helper-stage self-improvement error into the square-root sum used in the paper.

This form is often the convenient one for the helper-stage absorptions: it identifies selfImprovementHelperError with 100 m (√ε + √δ + √(d/q)), rather than requiring each proof to unfold the definition and convert the three rpow terms separately.

theorem MIPStarRE.LDT.SelfImprovement.selfImprovementHelperError_nonneg (params : Parameters) [FieldModel params.q] (eps delta : Error) : 0 ≤ selfImprovementHelperError params eps delta

The helper-stage threshold is nonnegative.

This is the basic positivity fact reused by the helper-stage absorption wrappers and by the final-stage comparison with selfImprovementError.

theorem MIPStarRE.LDT.SelfImprovement.helper_point_consistency_error_le_selfImprovementHelperError (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) : 4 * √(selfImprovementVarianceError params eps delta) ≤ selfImprovementHelperError params eps delta

Helper-stage point-consistency absorption (self_improvement.tex, lines 438--443).

4 √ζ_variance ≤ ζ̂.

theorem MIPStarRE.LDT.SelfImprovement.helper_strong_self_consistency_error_le_selfImprovementHelperError (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) (hd_le_q : ↑params.d ≤ ↑params.q) : 11 * √(selfImprovementVarianceError params eps delta) + √(2 * delta) + ↑params.m * ↑params.d / ↑params.q ≤ selfImprovementHelperError params eps delta

Helper-stage strong-self-consistency absorption (self_improvement.tex, lines 595--603).

11 √ζ_variance + √(2δ) + md/q ≤ ζ̂. The hypothesis hd_le_q records the small-error branch d/q ≤ 1 used in the paper, since q > 0.

theorem MIPStarRE.LDT.SelfImprovement.helper_boundedness_error_le_selfImprovementHelperError (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) : 3 * √delta + 4 * √(selfImprovementVarianceError params eps delta) ≤ selfImprovementHelperError params eps delta

Helper-stage boundedness absorption (self_improvement.tex, lines 614--624).

3 √δ + 4 √ζ_variance ≤ ζ̂.

theorem MIPStarRE.LDT.SelfImprovement.helper_completeness_error_le_selfImprovementHelperError (params : Parameters) [FieldModel params.q] (eps delta : Error) (heps : 0 ≤ eps) (hdelta : 0 ≤ delta) : 3 * √delta ≤ selfImprovementHelperError params eps delta

Helper-stage completeness absorption (self_improvement.tex, lines 403--414).

The loss 3 √δ from the Cauchy--Schwarz comparison is bounded by the helper threshold ζ̂.