Section 6 — Induction Parameter Bound Preliminaries

This file is one leaf of InductionParameterBounds. It contains the elementary point-line reduction for the base case, the real-variable comparison lemmas used by the small-parameter estimates, and the bound d/q ≤ 1.

References

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

theorem MIPStarRE.LDT.MainInductionStep.throughPoint_eq_zeroPoint_of_m_eq_one (params : Parameters) [FieldModel params.q] (hm1 : params.m = 1) (u : Point params) (i : Fin params.m) : AxisParallelLine.throughPoint u i = AxisParallelLine.throughPoint zeroPoint i

At m = 1, AxisParallelLine.throughPoint u i does not depend on the base point u: all axis-parallel lines in direction i are geometrically the unique line and share the same canonical representative.

theorem MIPStarRE.LDT.MainInductionStep.min_le_rpow_of_nonneg_of_exponent_le_one {x c : Error} (hx : 0 ≤ x) (hc_nonneg : 0 ≤ c) (hc_le_one : c ≤ 1) : min x 1 ≤ Real.rpow x c

theorem MIPStarRE.LDT.MainInductionStep.le_one_of_rpow_le_one {x c : Error} (hc_pos : 0 < c) (h : Real.rpow x c ≤ 1) : x ≤ 1

theorem MIPStarRE.LDT.MainInductionStep.dq_ratio_le_one (params : Parameters) (hdq_le_q : params.d ≤ params.q) : ↑params.d / ↑params.q ≤ 1

Internal helper: d/q ≤ 1 under the assumption params.d ≤ params.q.

Exposed for cross-module use in AvgSliceErrors and PastingAssembly.

theorem MIPStarRE.LDT.MainInductionStep.min_eps_one_le_mainInductionError_of_m_eq_one (params : Parameters) [FieldModel params.q] (k : ℕ) (eps delta gamma : Error) (hm1 : params.m = 1) (heps_nonneg : 0 ≤ eps) (hdelta_nonneg : 0 ≤ delta) (hgamma_nonneg : 0 ≤ gamma) : min eps 1 ≤ mainInductionError params k eps delta gamma

Internal helper: min eps 1 ≤ mainInductionError when params.m = 1.

Exposed for cross-module use in MainTheorems.