Off-diagonal add-in-u selection for helper point consistency #
The add-in-u specialization with Outcome = Fq params, M = A (the point measurement) 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): the counterpart of the vendored
SelfImprovement/Theorems/Results/AddInUPointConsistency.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
pointConsistencyAddInUCSChainQ0β¦Q4: the selected Cauchy--Schwarz chain at the off-diagonal selection, with its endpoint identifications.pointConsistencyAddInU_transfer_of_selected_chain_boundsandpointConsistencyAddInU_transfer_of_selected_chain_selfConsistency_globalVariance: the selection-dependent transfer, from four step bounds and from point self-consistency with the global-variance sum bound.addInULeftQuantity_pointConsistencySelection_eq_off_diagonal_avg,addInURightQuantity_pointConsistencySelection_eq_zero: the left side is the averaged off-diagonal mass, the right side vanishes by projectivity of the point measurement.pointConsistencyAddInU_off_diagonal_avg_le_of_transferand its_helper_error_form.
A strategy is a SymStrat params π K; the point measurement and T, H are local (in π), and
every scalar is strategy.state.ev of a joint operator strategy.state.opTensor X Y. The
vendored opTensor 0 Y = 0 step, proved entrywise there, is zero_mul after map_zero here. No
statement of the vendored file carries a swap, density or normalization hypothesis, so no
statement changed; the file sets no option, the vendored file-wide respectTransparency false
not being needed.
The vendored module is imported for its two classical declarations; the classical threshold
helper_point_consistency_error_le_selfImprovementHelperError comes from the vendored
Thresholds/Helper.lean through Thresholds/Final.lean, as in the vendored file.
Not ported #
pointConsistencyAddInUSelection: classical, imported.
References #
In LionSR/MIPStarRE at commit 507e8122, not in this repository:
references/ldt-paper/self_improvement.texlines 420β437blueprint/src/chapter/ch07_self_improvement.texlines 155β179
Upstream keeps this helper private since its Lean-module port (LionSR/MIPStarRE at 5fc363b); the port carries its own copy, with upstream's proof.
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.