Boundedness transport point-consistency estimates #
The point-consistency consequences of the helper-agreement off-diagonal decomposition, and the
natural-error transports of point consistency from the helper output to the projective output of
self-improvement: the counterpart of the vendored
SelfImprovement/Theorems/Results/BoundednessTransport/PointConsistency.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
opTensor_one_left_eq_rightTensor:S.opTensor 1 B = S.R B, kept under its vendored name with the modelSan explicit first argument.pointMeasurement_total_evalFamily_total_opTensor_ev_eq_rightTensorand itsS.L · * S.R ·form: the total-overlap term of the point measurement against an evaluation family isev (S.R G.total).helper_point_consistency_error_eq_off_diagonal_avg: the bipartite consistency defect of the point measurement againstpolynomialEvaluationFamily params His the averaged off-diagonal mass; with it,helper_point_consistency_of_pointConsistencyAddInU_transferandhelper_point_consistency_of_selected_chain_selfConsistency_globalVariance.final_fields_point_consistency_totalGap_natural,…_of_total_difference,final_fields_total_difference_le_sqrt_card_dataand…_of_data_processing: the submeasurement triangle at the natural error, with the total-overlap displacement explicit, as a single scalar difference, or bounded by√(#F_q · ε).
A strategy is a SymStrat params 𝔓 K; the point measurement, H and Hhat are local (in 𝔓).
The vendored opTensor A B is strategy.state.opTensor A B, leftTensor (ι₂ := ι) X * rightTensor (ι₁ := ι) Y is strategy.state.L X * strategy.state.R Y (the named carrier arguments
dropped), ev strategy.state is strategy.state.ev, the lifted families F.liftLeft,
F.liftRight are IdxSubMeas.liftLeft strategy.state F, IdxSubMeas.liftRight strategy.state F,
and Error is ℝ.
The two vendored transports from left to right lifts (sddRel_liftRight_of_liftLeft_permInv strategy.permInvState …) call M8's MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv strategy.state …, which needs no permutation invariance, swap symmetry being a theorem of the
model; the two vendored strategy.isNormalized arguments (of
Preliminaries.triangleSub_right_subMeas_totalGap and
Preliminaries.subMeas_total_ev_gap_abs_le_sqrt_card_qSDD) are dropped, since the ported lemmas
take none. 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 argument S : SubMeas … of the two
pointMeasurement_total_evalFamily_total_* lemmas is named G here, S being the model.
The imports mirror the vendored ones, with the Co ProjectivizationChain/Basic in place of the
vendored file (which it imports for its classical declarations).
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.texlines 435 and 747--755blueprint/src/chapter/ch07_self_improvement.tex
The tensor product with the identity on the left register is the right tensor placement.
The point measurement is complete and polynomial evaluation preserves the right-register total, so the tensor total has the same expectation as the right placement of the original total.
Left and right tensor placements of the point-measurement and evaluation totals reduce to the right-register total expectation.
The helper-stage consistency defect is exactly the averaged off-diagonal
mass appearing in the point-consistency add-in-u calculation.
This is the same algebraic identity as
helper_boundedness_slack_average_ev_eq_off_diagonal_avg, read as a
ConsRel defect for the point measurement against the polynomial-evaluation
family of H.
Helper-stage point consistency from the point-consistency add-in-u
transfer hypothesis.
The transfer bound controls the off-diagonal mass
E_u ∑_h ∑_{a ≠ h(u)} ⟨ψ, A^u_a ⊗ Hhat_h ψ⟩. The preceding algebraic
identity identifies this mass with the ConsRel defect for the point
measurement and the polynomial-evaluation family of Hhat.
Helper-stage point consistency obtained directly from the selected
add-in-u chain.
The hypotheses are the two analytic inputs used by the selected four-step
chain: bipartite self-consistency for the point measurement, and the
global-variance sum bound for the polynomial submeasurement T. The helper
submeasurement is the averaged sandwiched polynomial submeasurement built from
T, exactly as in the helper-stage application.
Natural-error transport of point consistency from the helper output to the projective output, with the submeasurement total-overlap displacement stated explicitly.
The measurement-valued right-register triangle lemma has no total-overlap term:
both right-register totals are the identity. In the present application
polynomialEvaluationFamily params Hhat and
polynomialEvaluationFamily params H.toSubMeas are only submeasurements, so
the total-overlap term
⟨ψ, A^u_{\mathrm{tot}} ⊗ H^u_{\mathrm{tot}} ψ⟩ must also be transported.
This theorem separates that displacement as the parameter η; the remaining
contribution is exactly the square root of the data-processing SDD error. The
upstream note docs/paper-gaps/issue-1093-submeasurement-triangle-total-overlap.tex
records the corresponding discrepancy with the measurement-valued paper step.
Natural-error point-consistency transport when the total-overlap displacement is supplied as a single right-register total difference.
Since the point measurement is complete and
polynomialEvaluationFamily params H has the same total as H, the averaged
total-overlap term in final_fields_point_consistency_totalGap_natural is
independent of the point u. This theorem records the corresponding reduction
of the upstream issue #1226 obstruction to the scalar difference between the totals of
the two right-register submeasurements.
The data-processing SDD comparison controls the total-overlap displacement which appears in the submeasurement form of the point-consistency triangle.
For each point u, the right-register total difference is the sum of the
field-answer differences in the two postprocessed polynomial families. The
finite-outcome Cauchy--Schwarz estimate
subMeas_total_ev_gap_abs_le_sqrt_card_qSDD, averaged over u, bounds this
single scalar by
sqrt (#F_q * ε). The factor #F_q records the cost of passing from the
outcomewise state-dependent distance to the total operator.
Natural-error point-consistency transport with the total-overlap displacement bounded internally from the data-processing SDD estimate.
The price of eliminating the explicit total-difference hypothesis is the
additional term sqrt (#F_q * selfImprovementDataProcessingError).