Section 6 — Averaged Slice Error Bounds: Successor Outputs #
This module packages recursive answer-valued slice measurements and the final self-improvement-to-main-induction error comparisons.
Extract the recursive answer-valued slice measurements and their averaged main-induction error bound.
Paper origin: references/ldt-paper/inductive_step.tex:441-551. After the
restricted-probabilities theorem and the predecessor answer-valued induction
hypothesis are applied to the restricted slices, this theorem packages the
resulting measurements G^x and proves the displayed bound
\mathbb E_x \sigma_x \leq \sigma.
Lean-only: This is an internal construction theorem for the simultaneous answer-valued successor route tracked in issue #1507; it does not add a predecessor conclusion as an assumption to any source-facing theorem. Discharge: proved here from the restricted-probabilities theorem and the answer-valued predecessor induction hypothesis.
Apply self-improvement to the recursive answer-valued successor slices.
Paper origin: references/ldt-paper/inductive_step.tex:461-551. Starting from
the recursive answer-valued slice measurements supplied by the predecessor
induction hypothesis, this theorem constructs the projective slice
submeasurements \widehat G^x and witnesses Z^x, proves their four
self-improvement outputs, and keeps the averaged \zeta_x and \sigma_x
bounds available.
Lean-only: The ordinary carrier appears only in the domination field, where its point measurement is the same last-coordinate restriction of the ambient answer-valued point measurement. The proof invokes only the axis-parallel/self-consistency form of self-improvement, and therefore does not claim that the carrier's dummy diagonal measurement is a good diagonal realization of the answer-valued strategy. This internal construction is tracked in issue #1507. Discharge: proved here from the recursive slice measurements and the formal self-improvement theorem.
Paper's \eqref{eq:zeta-smaller-than-nu}: under the small-parameter
hypotheses, the averaged self-improvement interface error \zeta is bounded by
the next-stage induction parameter \nu.
Answer-valued analogue of
selfImprovementInInductionError_le_mainInductionNu.
This is the scalar part of the successor proof for an ambient answer-valued strategy. It uses only the answer-valued goodness bounds and does not replace the answer-valued diagonal measurement by an ordinary one.