Helper strong self-consistency bounds: core reductions #
Core bound structures, the bare off-diagonal quantity, and the two variance-swap identities used in the helper strong self-consistency chain.
References #
references/ldt-paper/self_improvement.texblueprint/src/chapter/ch07_self_improvement.tex
Named intermediate bounds for the helper-stage strong self-consistency proof.
Paper origin: references/ldt-paper/self_improvement.tex:255-603
(\label{item:self-improvement-self} and the subsequent add-in-u,
self-consistency, and variance-swap chain).
This is an internal record for the helper-stage strong self-consistency proof,
tracked by #1596. It is not a hypothesis of a source-labelled theorem. Its
fields are derived from the add-in-u, self-consistency, and global-variance
estimates and are not passed across the public statement of
lem:self-improvement-helper.
These fields isolate the paper-side intermediate estimates in the proof of
item:self-improvement-self once the reduced helper conclusion is fixed:
- the four scalar transport bounds along the chain
Q₀ \to Q₁ \to Q₂ \to Q₃ \to Q₄, and - the final lower bound on the released right-hand side before the arithmetic
absorption into
selfImprovementHelperError.
This structure records the actual intermediate estimates used from the
add-in-u, self-consistency, and variance calculations, rather than restating
the final BipartiteSSCRel conclusion as an input. It is an internal assembly
record for the helper theorem, not a hypothesis of the paper-aligned helper
theorem; the full assembly of these bounds discharged the former #1514 gap.
- step01Bound : |addInUCSChainQ0 params strategy T.toSubMeas - addInUCSChainQ1 params strategy T.toSubMeas| ≤ √(2 * delta)
Paper
eq:move-one: theQ₀ \to Q₁transport bound. - step12Bound : |addInUCSChainQ1 params strategy T.toSubMeas - addInUCSChainQ2 params strategy T.toSubMeas| ≤ √(2 * delta)
Paper
eq:move-another: theQ₁ \to Q₂transport bound. - step23Bound : |addInUCSChainQ2 params strategy T.toSubMeas - addInUCSChainQ3 params strategy T.toSubMeas| ≤ √(selfImprovementVarianceError params eps delta)
Paper
eq:change-one: theQ₂ \to Q₃variance transport bound. - step34Bound : |addInUCSChainQ3 params strategy T.toSubMeas - addInUCSChainQ4 params strategy T.toSubMeas| ≤ √(selfImprovementVarianceError params eps delta)
Paper
eq:change-another: theQ₃ \to Q₄variance transport bound. - residualLowerBound : subMeasMass strategy.state Hhat.liftLeft - addInURightQuantity params strategy (sandwichedPolynomialSubMeasAt params strategy T.toSubMeas) T.toSubMeas (selfConsistencyAddInUSelection params) ≤ 11 * √(selfImprovementVarianceError params eps delta) + √(2 * delta) + ↑params.m * ↑params.d / ↑params.q - addInUError params eps delta
The released right-hand side is within the paper's pre-absorption helper SSC error of the helper mass.
Instances For
Construct the helper-stage bounds from the mathematical inputs after the
add-in-u chain has been closed.
The point self-consistency hypothesis supplies the two self-consistency moves
Q₀ → Q₁ and Q₁ → Q₂; the local-variance sum bound supplies the two
global-variance moves Q₂ → Q₃ and Q₃ → Q₄. The only additional scalar input
is the residual lower bound for the released right-hand side.
The bare off-diagonal polynomial-pair mass appearing after the released residual is expanded.
This is the right-hand side of
helper_mass_sub_release_eq_polynomial_off_diagonal, stated for an arbitrary
polynomial submeasurement T.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The bare off-diagonal polynomial-pair mass is a contraction.
For each point u, the off-diagonal sum is bounded by the full double sum
Σ_h Σ_{h'} H^u_{h'} ⊗ T_h, which is
(H^u.total) ⊗ T.total. Both factors are submeasurement totals, so the
expectation is at most 1 in the normalized strategy state.
Off-diagonal variance swaps #
The selected support for the two off-diagonal variance swaps in the helper SSC residual estimate.
At the point u, it selects precisely the ordered polynomial pairs (h', h)
with h' ≠ h and h u = h' u, matching the indicator support in
eq:swapped-u-for-v and
eq:swapped-u-for-v-this-time-it's-personal.
Equations
- MIPStarRE.LDT.SelfImprovement.helperOffDiagonalVarianceSwapSelection params u = {hh : MIPStarRE.LDT.Polynomial params × MIPStarRE.LDT.Polynomial params | hh.1 ≠ hh.2 ∧ hh.2.toFun u = hh.1.toFun u}
Instances For
The selected-chain endpoint Q₄ is the off-diagonal indicator quantity.
The selected-chain scalar Q₃ is the one-sided swapped off-diagonal
indicator quantity.
The selected-chain scalar Q₂ is the fully swapped off-diagonal indicator
quantity.
The first off-diagonal variance swap, corresponding to
eq:swapped-u-for-v in the helper SSC residual chain.
The second off-diagonal variance swap, corresponding to
eq:swapped-u-for-v-this-time-it's-personal in the helper SSC residual chain.