Boundedness transport boundedness-gap estimates #
The helper boundedness-gap decomposition, its data-processing transport, and the final
projective-residual boundedness constructors of the self-improvement proof: the counterpart of
the vendored SelfImprovement/Theorems/Results/BoundednessTransport/BoundednessGap.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
Contents #
helper_boundedness_gap_eq_upper_gap_add_off_diagonal_avg: the helper gap is⟨Z ⊗ I⟩ - ⟨I ⊗ H.total⟩plus the averaged off-diagonal mass; with it the helper-stage boundshelper_boundedness_gap_le_selfImprovementHelperError,…_of_pointConsistencyAddInU_transferand…_of_helper_outputs, and the comparisonhelper_upper_gap_rightTensor_le_three_sqrt_delta_of_helper_outputs.helper_boundedness_gap_transport_through_data_processing: replacingHhatby the projectiveHcosts√ε.projective_boundedness_gap_le_helper_boundedness_gap: the SDP dual-slack comparison.final_fields_projective_residual_bound_natural,…_bound,…_of_small_errorsand…_of_helper_outputs: the projective residual at the natural and the literal error.final_fields_bounded:1 ≤ ZgivesBoundedByOperatorat every nonnegative tolerance.
The translation is that of BoundednessTransport/PointConsistency.lean: a strategy is a
SymStrat params 𝔓 K, opTensor A B is strategy.state.opTensor A B, leftTensor (ι₂ := ι) X
and rightTensor (ι₁ := ι) X are strategy.state.L X and strategy.state.R X, ev strategy.state
is strategy.state.ev, the lifts F.liftLeft, F.liftRight are IdxSubMeas.liftLeft strategy.state F, IdxSubMeas.liftRight strategy.state F (and SubMeas.liftLeft S A for a single
submeasurement), helperUpperOperator params Z is helperUpperOperator strategy.state params Z,
and Error is ℝ.
The vendored swap strategy.permInvState.swap_ev Hhat.total is the keystone's
strategy.state.ev_L_eq_ev_R Hhat.total; the vendored sddRel_liftRight_of_liftLeft_permInv strategy.permInvState … is M8's MakingMeasurementsProjective.sddRel_liftRight_of_liftLeft_permInv strategy.state …; the vendored strategy.isNormalized argument of
Preliminaries.easyApproxFromApproxDelta is dropped, the ported lemma taking none. In
final_fields_bounded the vendored (ψ : QuantumState (ι × ι)) is the model (S : SymModel 𝔓 K),
an explicit first argument, and Matrix.PosSemidef.one.nonneg is zero_le_one. The hypotheses
hslack : ∀ h, T_h A_h = T_h Z are SDP complementary slackness passed through, of unchanged
shape. No statement of the vendored file carries a swap, density or normalization hypothesis, so
no statement changed beyond the translation; the file sets no option, the vendored file-wide
respectTransparency false not being needed.
The classical threshold lemmas helper_boundedness_error_le_selfImprovementHelperError (vendored
Thresholds/Helper.lean) and final_fields_projective_residual_error_le_selfImprovementError
(vendored Thresholds/Final.lean) are imported; the imports mirror the vendored one.
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 612--613 and 742--755blueprint/src/chapter/ch07_self_improvement.tex
Algebraic decomposition of the helper boundedness gap.
The scalar gap ⟨Z ⊗ I - helperAgreementAverageOperator⟩ is the sum of
⟨Z ⊗ I⟩ - ⟨I ⊗ H.total⟩ and the off-diagonal average produced by
helper_boundedness_slack_average_ev_eq_off_diagonal_avg.
Helper-stage boundedness from the scalar comparison and the off-diagonal estimate.
The comparison ⟨Z ⊗ I⟩ - ⟨I ⊗ Hhat.total⟩ ≤ 3 √δ and the off-diagonal estimate
≤ 4 √ζ_variance give the helper threshold, by
helper_boundedness_error_le_selfImprovementHelperError.
Helper-stage boundedness from the scalar comparison and the point-consistency add-in-u
transfer: the off-diagonal estimate of pointConsistencyAddInU_off_diagonal_avg_le_of_transfer
composed with helper_boundedness_gap_le_selfImprovementHelperError.
Convert the helper-completeness Hhat-versus-Z comparison to the right-placed total
comparison used in the boundedness gap.
The helper-completeness paragraph proves ⟨Z ⊗ I⟩ - 3√δ ≤ subMeasMass (Hhat.liftLeft S); the
swap symmetry of the model, S.ev_L_eq_ev_R, turns the left-placed total into the right-placed
one.
Helper-stage boundedness from the helper comparison and the point-consistency add-in-u
transfer.
Complementary slackness hslack and the off-diagonal transfer htransfer remain explicit
hypotheses, as in the vendored statement.
Transport the helper boundedness gap through the data-processing approximation between
Hhat and H: replacing the helper polynomial family in the point-agreement average by the
projective family costs at most √ε (Proposition easy-approx-from-approx-delta).
Compare the final projective residual with the helper boundedness gap for the same projective family.
This is the SDP dual-slack step of the projective boundedness paragraph: Z ⊗ H_h dominates
(E_u A^u_{h(u)}) ⊗ H_h for each polynomial h, and summing turns Z ⊗ (I - H) into the
helper-stage defect Z ⊗ I - E_u Σ_a A^u_a ⊗ H_[h(u)=a].
Natural-error projective-residual construction.
Given the helper-stage boundedness estimate for Hhat, the dual-slack comparison and the
data-processing transport give the final projective residual at the natural error
selfImprovementHelperError + √selfImprovementDataProcessingError.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
Literal-threshold projective-residual construction: the natural bound followed by a
separately named numerical absorption habsorb.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
Literal-threshold projective-residual construction under the standard unit-interval
smallness hypotheses, the absorption being
final_fields_projective_residual_error_le_selfImprovementError.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
Final projective-residual construction from helper outputs and the point-consistency
add-in-u transfer: the helper-stage bound of
helper_boundedness_gap_le_selfImprovementHelperError_of_helper_outputs, then
final_fields_projective_residual_bound_of_small_errors.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
Final-fields constructor for the BoundedByOperator conclusion.
If 1 ≤ Z, the left-placed mass of any submeasurement is dominated by Z ⊗ I: A.total ≤ 1 ≤ Z
lifts by monotonicity of S.L and of ev, so bndError (A.liftLeft S) (Z ⊗ I) = 0 and the
boundedness statement holds at any nonnegative tolerance.