Section 9 — final-stage numerical threshold absorptions #
This module contains the final-stage arithmetic comparisons which absorb the natural
projective-output error terms into the literal selfImprovementError threshold.
The estimates formalize the exponent-monotonicity bookkeeping in
references/ldt-paper/self_improvement.tex, lines 803--810, and are used by the
final-field construction theorems in the self-improvement theorem.
The helper-stage estimates, including the square-root bound on the global-variance
error, are in Thresholds.Helper.
Final-stage threshold: 30 ζ̂ ≤ ζ #
For ε, δ, d/q ∈ [0, 1], the helper-stage error is dominated by
selfImprovementError / 30. This is the exponent-monotonicity step in the
paper's chained absorption (self_improvement.tex, lines 803--810): for
unit-interval x and 0 ≤ z ≤ y, x^y ≤ x^z.
The three-term power sum used in the final-stage self-improvement threshold bookkeeping.
For exponent p, this is the Lean counterpart of
ε^p + δ^p + (d/q)^p. Keeping this expression named makes the nested
absorptions in self_improvement.tex, lines 772--810, insensitive to future
constant adjustments.
Equations
Instances For
The final-stage power sum is nonnegative when its base parameters are nonnegative.
This is the positivity fact used when multiplying coefficient comparisons by
ε^p + δ^p + (d/q)^p.
Exponent monotonicity for the final-stage power sum on the unit interval.
If ε, δ, and d/q all lie in [0, 1], then increasing the exponent
decreases each term of the power sum. This is the formal arithmetic step behind
the final threshold comparison in self_improvement.tex, lines 803--810.
The square root of a final-stage power sum is bounded by the power sum with half the exponent.
The proof is the elementary estimate
sqrt (x + y + z) ≤ sqrt x + sqrt y + sqrt z, applied to the three powers
ε^p, δ^p, and (d/q)^p.
The helper-stage threshold as the final-stage power sum with exponent
1/2.
This is definitionally equal to selfImprovementHelperError; the named lemma is
used to avoid unfolding the error definition inside later absorptions.
The final self-improvement threshold as the final-stage power sum with
exponent 1/32.
This records the literal error parameter appearing in the formal statement of the self-improvement theorem.
The orthogonalization threshold written as an iterated square root of the helper threshold.
The paper writes the corresponding quantity as
100 * \widehat{\zeta}^{1/4}. This lemma gives the equivalent square-root
form used by the estimates which follow orthonormalization.
The data-processing threshold written with an ordinary square root.
This is the displayed expression used after projecting the helper output:
8\widehat{\zeta} + 8\sqrt{\widehat{\zeta}_{\mathrm{ortho}}}.
The data-processing threshold contains the term 8 * selfImprovementHelperError.
This lower bound is the scalar source of the alphabet-size obstruction in the
older total-gap point-consistency transport: once the total-overlap estimate contributes
sqrt (#F_q * selfImprovementDataProcessingError), this positive summand carries
the cardinality of the alphabet into the final-stage error.
The alphabet-size square-root term is bounded below by the corresponding
term coming from 8 * selfImprovementHelperError.
This records that, in the older total-gap final-fields transport, the cardinality
factor cannot be removed by lower-bounding
selfImprovementDataProcessingError through 8 * selfImprovementHelperError.
The structural obstruction is the surrounding estimate carrying
sqrt (#F_q * selfImprovementDataProcessingError) into a final threshold
which has no corresponding alphabet-size term.
Final projective-residual threshold absorption (self_improvement.tex,
lines 803--810).
The natural error emitted by the projective residual construction is
ζ̂ + √ζ̂_dataprocess. Under the standard unit-interval hypotheses for
ε, δ, and d/q, this theorem absorbs that natural error into the literal
selfImprovementError threshold used by SelfImprovementConclusion. Lean
records the third unit-interval hypothesis as d ≤ q, equivalently d/q ≤ 1
because q is positive.
Final point-consistency threshold absorption from a total-difference bound.
The fallback submeasurement-total route contributes the natural error
2 * ζ̂ + √ζ̂_dataprocess + 2 * √ζ̂_ortho.
Under the standard unit-interval hypotheses for ε, δ, and d/q, this is
still absorbed by the literal selfImprovementError threshold.
Final completeness threshold absorption (self_improvement.tex,
lines 803--810).
The natural error emitted by the projective completeness transport is
2ζ̂ + 2 sqrt ζ̂_ortho. Under the standard unit-interval hypotheses for
ε, δ, and d/q, this theorem absorbs that natural error into the literal
selfImprovementError threshold used by SelfImprovementFinalFields. Lean
records the third unit-interval hypothesis as d ≤ q, equivalently d/q ≤ 1
because q is positive.
Final self-closeness threshold absorption (self_improvement.tex,
lines 803--810).
The natural error emitted by the projective self-closeness transport is
3 * (ζ̂_ortho + 2ζ̂ + ζ̂_ortho). Under the standard unit-interval hypotheses
for ε, δ, and d/q, this theorem absorbs that natural error into the
literal selfImprovementError threshold used by SelfImprovementFinalFields.
Lean records the third unit-interval hypothesis as d ≤ q, equivalently
d/q ≤ 1 because q is positive.