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: the counterpart of the vendored
SelfImprovement/Theorems/Results/HelperSSC/Assembly.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
helper_residualLowerBound_of_offDiagonal_boundandhelper_residualLowerBound_of_paper_chain_bound: the residual lower bound ofHelperStrongSelfConsistencyBoundsfrom a bound on the bare off-diagonal quantity.helperMoveOverVQuantity_lower_of_pointConsistencyAddInU_transfer: theeq:move-over-vlower bound, from complementary slackness, dual feasibility and the point-consistency transfer.helperOffDiagonalBareQuantity_le_paper_chain_of_scalar_transports: the residual chain7√ζ_variance + √(2δ) + md/qfrom the scalar transports.- The four constructors of
HelperStrongSelfConsistencyBounds(…_offDiagonal,…_paperChain,…_scalarTransports,helper_ssc_bounds_of_scalarTransports_pointTransfer), and the closinghelper_strong_self_consistency_of_helper_conclusion.
A strategy is a SymStrat params 𝔓 K; the polynomial measurement T, the helper Hhat, the
dual witness Z and the point projectors live in 𝔓, and every scalar is strategy.state.ev
of a joint operator strategy.state.opTensor X Y; rightTensor (ι₁ := ι) X is
strategy.state.R X, subMeasMass strategy.state Hhat.liftLeft is
strategy.state.subMeasMass (Hhat.liftLeft strategy.state), BipartiteSSCRel strategy.state …
and qBipartiteMatchMass strategy.state … are the SymModel declarations, and Error is ℝ.
Complementary slackness. The hypothesis hslack : ∀ h, T_h A_h = T_h Z of
helperMoveOverVQuantity_lower_of_pointConsistencyAddInU_transfer and
helper_ssc_bounds_of_scalarTransports_pointTransfer keeps its vendored shape in 𝔓. In the
eq:move-over-v computation it rewrites T_h A_h to T_h Z in the right factor of
∑_{h'} ∑_h ev(H^u_{h'} ⊗ T_h A_h), and ∑_h T_h Z = Z comes from T.total_eq_one, with
one_mul and Finset.sum_mul for the vendored Matrix.one_mul and Matrix.mul_sum.
helper_strong_self_consistency_of_helper_conclusion calls no SDP producer (its SDP witness
arrives inside SelfImprovementHelperConclusion), so it keeps its vendored hypotheses.
Swap and density uses. The vendored ev_opTensor_swap_of_density_fixed strategy.state strategy.densityFixed _ _ (vendored line 388) is the keystone's
strategy.state.ev_opTensor_swap_of_density_fixed _ _, and the vendored
strategy.permInvState.swap_ev Hhat.total (vendored line 419) is
strategy.state.ev_L_eq_ev_R Hhat.total. No statement of the vendored file carries a swap,
density or normalization hypothesis, so no statement changed beyond the translation.
Proofs that differ from the vendored ones.
- In
helperMoveOverVQuantity_lower_of_pointConsistencyAddInU_transferthe agreement average is computed per polynomial,avg_v ev(A^v_{h(v)} ⊗ H_h) = ev(A_h ⊗ H_h) = avg_u ev(A_h ⊗ H^u_h), through Coev_opTensor_averageOperatorOverDistribution_left/_right, without the vendored exchange of the two point averages (avgOver_uniform_comm); the identityE_v T_h A^v_{h(v)} = T_h A_hisFinset.mul_sumandmul_smul_common the definition. - In
helper_strong_self_consistency_of_helper_conclusionthe closingsimpathrough the defect definitions isavgOver_uniform_constonUnit, the defect beingmax 0 (mass - match)by definition. helper_residualLowerBound_of_paper_chain_boundrewritesaddInUErrorwithReal.sqrt_eq_rpowand closes bylinarith.helperOffDiagonalBareQuantity_le_paper_chain_of_scalar_transportscollects the five Co identities and bounds it needs and closes by onelinarith, without the vendored local abbreviations andsimpasteps.- The four vendored
lemmas aretheorems, and the three constructors that only apply other constructors are terms.
The file sets no option, the vendored file-wide respectTransparency false not being needed.
Not ported #
Every declaration of the vendored file has a counterpart here.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
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.