Section 6 — Main-Induction Error Bounds

This file is one leaf of InductionParameterBounds. It contains the scalar consequences of the non-vacuous hypothesis mainInductionError < 1, including the bounds eps ≤ 1, delta ≤ 1, gamma ≤ 1, params.d ≤ params.q, and mainInductionNu < 1.

References

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

theorem MIPStarRE.LDT.MainInductionStep.one_le_k_of_mainInductionError_lt_one (params : Parameters) (k : ℕ) (eps delta gamma : Error) (hsmall : mainInductionError params k eps delta gamma < 1) : 1 ≤ k

In the nontrivial main-induction branch, the integer parameter k is positive.

Paper origin: references/ldt-paper/inductive_step.tex:441-551, where the successor proof is reduced to the nontrivial small-error regime before the slice estimates are used. The implication mainInductionError < 1 → 1 ≤ k is a formalization-only scalar consequence: if k = 0, then the main-induction error is at least m^2, hence at least 1.

theorem MIPStarRE.LDT.MainInductionStep.mainInductionNu_lt_one_of_mainInductionError_lt_one (params : Parameters) (k : ℕ) (eps delta gamma : Error) (hsmall : mainInductionError params k eps delta gamma < 1) : mainInductionNu params k eps delta gamma < 1

Internal helper: mainInductionNu < 1 follows from mainInductionError < 1.

Exposed for cross-module use in MainTheorems.

theorem MIPStarRE.LDT.MainInductionStep.eps_le_one_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : eps ≤ 1

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

Exposed for cross-module use in MainTheorems.

theorem MIPStarRE.LDT.MainInductionStep.delta_le_one_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : delta ≤ 1

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

Exposed for cross-module use in MainTheorems.

theorem MIPStarRE.LDT.MainInductionStep.three_le_k_sq_mul_next_m_of_hsmall {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : 3 ≤ ↑k ^ 2 * ↑params.next.m

Internal helper: 3 ≤ k² · m_next in the small-parameter regime.

Exposed for cross-module use in AvgSliceErrors.

theorem MIPStarRE.LDT.MainInductionStep.gamma_le_one_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : gamma ≤ 1

Internal helper: under mainInductionError < 1, the diagonal error gamma ≤ 1.

Exposed for cross-module use in MainTheorems.

theorem MIPStarRE.LDT.MainInductionStep.dq_le_q_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : params.d ≤ params.q

Internal helper: under mainInductionError < 1, params.d ≤ params.q.

Exposed for cross-module use in MainTheorems.

Answer-valued small-error scalar consequences

theorem MIPStarRE.LDT.MainInductionStep.answer_eps_le_one_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : eps ≤ 1

Answer-valued analogue of eps_le_one_of_mainInductionError_lt_one.

theorem MIPStarRE.LDT.MainInductionStep.answer_delta_le_one_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : delta ≤ 1

Answer-valued analogue of delta_le_one_of_mainInductionError_lt_one.

theorem MIPStarRE.LDT.MainInductionStep.answer_gamma_le_one_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : gamma ≤ 1

Answer-valued analogue of gamma_le_one_of_mainInductionError_lt_one.

theorem MIPStarRE.LDT.MainInductionStep.answer_dq_le_q_of_mainInductionError_lt_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : params.d ≤ params.q

Answer-valued analogue of dq_le_q_of_mainInductionError_lt_one.

theorem MIPStarRE.LDT.MainInductionStep.answer_three_le_k_sq_mul_next_m_of_hsmall {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : AnswerSymStrat params.next ι) {eps delta gamma : Error} {k : ℕ} (hgood : strategy.IsGood eps delta gamma) (hsmall : mainInductionError params.next k eps delta gamma < 1) : 3 ≤ ↑k ^ 2 * ↑params.next.m

Answer-valued analogue of three_le_k_sq_mul_next_m_of_hsmall.

theorem MIPStarRE.LDT.MainInductionStep.mainInductionSuccessorBound_pred (params : Parameters) {k : ℕ} (hk : 400 * params.next.m * params.next.d ≤ k) : 400 * params.m * params.d ≤ k

The successor large-k hypothesis implies the predecessor large-k hypothesis used by recursive slice calls.

This is the elementary arithmetic comparison between the successor dimension params.m + 1 and the predecessor dimension params.m.