Helper strong self-consistency bounds: residual assembly #
Residual lower-bound reductions, scalar-chain bound constructors, and the final helper-stage strong self-consistency assembly theorems.
References #
references/ldt-paper/self_improvement.texblueprint/src/chapter/ch07_self_improvement.tex
Reduce the residual lower bound to the off-diagonal residual scalar bound.
For the actual helper output, the equality
Hhat = E_u A^u_{h(u)} T_h A^u_{h(u)} identifies the left-hand side of
HelperStrongSelfConsistencyBounds.residualLowerBound with the
off-diagonal quantity isolated by
helper_mass_sub_release_eq_polynomial_off_diagonal. Thus the remaining
analytic work may be stated as a bound on that concrete polynomial-pair sum,
rather than as a direct bound on the record field itself.
Reduce the residual lower bound to the paper-shaped residual-chain bound.
After eq:release-the-kraken, eq:threw-in-h-prime, eq:delete-an-A, and
eq:move-over-v, the paper bounds the expanded residual by
7√ζ_variance + √(2δ) + md/q. Since
addInUError = 4√ζ_variance, this is exactly the pre-absorption bound
11√ζ_variance + √(2δ) + md/q - addInUError.
Paper line eq:move-over-v yields a lower bound on the moved quantity in
terms of the helper mass and the explicit A-consistency defect.
This is the algebraic/slackness part of self_improvement.tex:579-589: average
over v, replace T_h · E_v A^v_{h(v)} by T_h · Z using complementary
slackness, collapse the T-sum to Z, compare Z to the averaged point
operator by dual feasibility, and then subtract the off-diagonal helper
agreement defect controlled by the point-consistency add-in-u transfer.
Assemble the paper's final residual-chain estimate from the displayed scalar transport bounds.
The first two hypotheses are the two variance swaps used to pass from
eq:added-indicator to the Schwartz--Zippel endpoint. The next two hypotheses
are the transports from eq:delete-an-A to eq:move-over-v. The final
hypothesis is the lower bound on the move-over-v endpoint obtained after
substituting the averaged operator Z and using the explicit point-consistency
bound for the point measurement.
Construct the helper-stage bounds from local variance and a named off-diagonal residual estimate.
This produces the same named bounds as
helper_strong_self_consistency_bounds_of_selfConsistency_localVariance,
but its final input is the concrete off-diagonal polynomial-pair bound obtained
after expanding the released residual.
Construct the helper-stage bounds from the paper's final residual chain estimate.
This variant lets downstream work target the paper's natural bound
7√ζ_variance + √(2δ) + md/q on the expanded off-diagonal residual. The
conversion to the record's 11√ζ_variance + √(2δ) + md/q - addInUError
form is performed internally.
Construct the helper-stage bounds directly from the scalar transport estimates appearing in the paper.
Compared with
helper_strong_self_consistency_bounds_of_selfConsistency_localVariance_paperChain,
this version does not ask for the already assembled residual-chain estimate.
It consumes the two off-diagonal variance swaps, the two post-delete-an-A
transports, and the final lower bound on the move-over-v endpoint, then
assembles the residual estimate internally.
Construct the helper-stage bounds from the paper's scalar transports and
the point-consistency add-in-u transfer.
This is the same residual-chain constructor as
helper_strong_self_consistency_bounds_of_selfConsistency_localVariance_scalarTransports,
but it discharges the two off-diagonal variance swaps from local variance and
the final move-over-v lower-bound input from complementary slackness, dual
feasibility, and the point-consistency transfer. It packages the paper lines
after eq:move-over-v together with the two post-delete-an-A scalar
transports.
Produce the helper-stage strong self-consistency conclusion from the actual
helper construction together with the named add-in-u/variance transports.
The theorem consumes the reduced helper output
SelfImprovementHelperConclusion params strategy T Hhat Z eps delta and the
four named scalar chain bounds together with the final lower bound on the
released right-hand side. It then assembles the diagonal transfer
using add_in_u_simplified_transfer_of_cs_chain_sqrt_form, upgrades it to the
paper's released right-hand side via
selfConsistencyDiagonalAddInU_of_simplifiedTransfer, and applies the closing
arithmetic absorption
helper_strong_self_consistency_error_le_selfImprovementHelperError.
This is the complete route from the actual helper construction and the named
scalar bounds to helper-stage strong self-consistency. The analytic work is
therefore stated as named bounds, rather than left as an
unstructured BipartiteSSCRel assumption.