Section 6 — Main-induction error bounds #
The scalar consequences of the non-vacuous hypothesis mainInductionError < 1: the bounds
eps ≤ 1, delta ≤ 1, gamma ≤ 1, params.d ≤ params.q and 3 ≤ k² · m_next for a good
strategy. This is the counterpart of
MIPRE/Background/LIDT/MIPStarRE/LDT/MainInductionStep/Theorems/InductionParameterBounds/MainError.lean
in the port of planning/c6b-plan.md (milestone M12, section "Port conventions").
Ten declarations read a strategy and are ported: the five bounds for a good
SymStrat params.next 𝔓 K and their five answer-valued analogues for a good
AnswerSymStrat params.next 𝔓 K. A strategy enters only through the nonnegativity of
eps, delta and gamma that its IsGood gives (eps_nonneg_of_isGood and its siblings of
Co/Test/StrategyFailures.lean), so each ported lemma applies one of two private scalar
theorems, le_one_of_mainInductionError_lt_one_of_nonneg and
three_le_k_sq_mul_next_m_of_nonneg, which take those three nonnegativity facts in place of the
strategy. No lemma of the file has a swap, density or normalization hypothesis.
The other six declarations are arithmetic on the classical error functions mainInductionError
and mainInductionNu: this file imports the vendored file and names them through an explicit
open MIPStarRE.LDT.MainInductionStep (…) list. Importing it adds no operator content, since the
vendored file's only import is the vendored InductionParameterBounds/Preliminaries, which the
ported Preliminaries already imports.
Not ported #
k_ne_zero_of_mainInductionError_lt_one: classical, imported.one_le_k_of_mainInductionError_lt_one: classical, imported.mainInductionNu_lt_one_of_mainInductionError_lt_one: classical, imported.mainInductionNu_scaled_component_le: classical, imported.mainInductionSuccessorBound_pred: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
blueprint/src/chapter/ch10_induction.texreferences/ldt-paper/inductive_step.tex
Under mainInductionError < 1, the axis-parallel error of a good strategy satisfies
eps ≤ 1.
Under mainInductionError < 1, the self-consistency error of a good strategy satisfies
delta ≤ 1.
3 ≤ k² · m_next in the small-parameter regime of a good strategy.
Under mainInductionError < 1, the diagonal error of a good strategy satisfies
gamma ≤ 1.
Under mainInductionError < 1 for a good strategy, params.d ≤ params.q.
Answer-valued small-error scalar consequences #
Answer-valued analogue of eps_le_one_of_mainInductionError_lt_one.
Answer-valued analogue of delta_le_one_of_mainInductionError_lt_one.
Answer-valued analogue of gamma_le_one_of_mainInductionError_lt_one.
Answer-valued analogue of dq_le_q_of_mainInductionError_lt_one.
Answer-valued analogue of three_le_k_sq_mul_next_m_of_hsmall.