Off-diagonal add-in-u selection infrastructure for helper point consistency #
This module isolates the theorem-side add-in-u specialization with
Outcome = Fq params, M = A, and the off-diagonal selection
S_u = {(a, h) : h(u) ≠ a} used in the proof of the helper-stage
A-consistency bound (eq:explicit-bound-for-A-consistency).
It does not prove the full point-consistency estimate. Instead, it provides the missing theorem-side selection object, the associated selected scalar Cauchy--Schwarz chain, and the left/right quantity identities needed by a later transfer theorem.
The final theorem in this file also records the numerical absorption from the
natural add-in-u error 4 sqrt ζ_variance to the helper-stage error
ζ_hat. Thus the remaining analytic input is precisely the
selection-dependent transfer estimate, not an additional arithmetic comparison.
References #
references/ldt-paper/self_improvement.texlines 420–437blueprint/src/chapter/ch07_self_improvement.texlines 155–179
The off-diagonal selection used in the helper-stage A-consistency
application of lem:add-in-u.
At each point u, this selects exactly the pairs (a, h) with h u ≠ a,
matching the paper's choice S_u = {(a,h) : h(u) ≠ a} in the proof of
eq:explicit-bound-for-A-consistency.
Equations
- MIPStarRE.LDT.SelfImprovement.pointConsistencyAddInUSelection params u = {ah : MIPStarRE.LDT.Fq params × MIPStarRE.LDT.Polynomial params | ah.2.toFun u ≠ ah.1}
Instances For
Off-diagonal selected scalar chain #
The off-diagonal point-consistency specialization of the selected add-in-u
chain endpoint Q₀.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The off-diagonal point-consistency specialization of the selected add-in-u
chain scalar Q₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The off-diagonal point-consistency specialization of the selected add-in-u
chain scalar Q₂.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The off-diagonal point-consistency specialization of the selected add-in-u
chain scalar Q₃.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The off-diagonal point-consistency specialization of the selected add-in-u
chain endpoint Q₄.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The off-diagonal selected-chain endpoint Q₀ is the corresponding generic
add-in-u left quantity with the averaged sandwiched polynomial submeasurement.
The off-diagonal selected-chain endpoint Q₄ is the corresponding generic
add-in-u right quantity.
Point-consistency add-in-u transfer assembled from the four selected scalar chain estimates.
This theorem is the off-diagonal counterpart of the diagonal chain assembly:
once the four selected Cauchy--Schwarz moves are available with total error at
most addInUError, it gives the theorem-side transfer hypothesis consumed by
pointConsistencyAddInU_off_diagonal_avg_le_of_transfer.
Point-consistency add-in-u transfer with the two self-consistency moves and the two selected global-variance moves supplied by the proved Cauchy--Schwarz bounds.
This is the theorem-side form of the off-diagonal application of
lem:add-in-u: the first two selected moves use bipartite self-consistency of
the point measurement, while the last two use the global-variance sum bound for
the polynomial submeasurement T.
The left side of the helper point-consistency add-in-u application is the
averaged off-diagonal helper-agreement mass.
This is exactly the scalar quantity on the left of
eq:explicit-bound-for-A-consistency, written through the generic theorem-side
addInULeftQuantity interface for the off-diagonal selection.
The right side of the helper point-consistency add-in-u application is
identically zero by projectivity of the point measurement.
For every selected pair (a, h) with h u ≠ a, the inner sandwich contains the
factor A^u_{h(u)} A^u_a = 0, so every summand vanishes.
Any theorem-side add-in-u transfer bound for the off-diagonal selection
immediately bounds the averaged helper off-diagonal mass by addInUError.
This is the exact theorem-side wrapper needed to connect a future generic
selection-dependent transfer theorem to the helper A-consistency route.
Helper-stage point-consistency bound from the off-diagonal add-in-u
transfer estimate.
The preceding theorem gives the natural bound addInUError, which is equal to
4 * sqrt ζ_variance after rewriting by Real.sqrt_eq_rpow. This wrapper
applies the numerical
absorption from self_improvement.tex, lines 438--443, so that the resulting
off-diagonal helper mass is already bounded by the helper-stage error
selfImprovementHelperError. The only remaining analytic input is the
selection-dependent add-in-u transfer inequality for
pointConsistencyAddInUSelection.