Boundedness transport boundedness-gap estimates #
This file contains the helper boundedness-gap decomposition, its data-processing transport, and the final projective-residual boundedness constructors used in the self-improvement proof.
References #
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. This is the
formal algebraic bridge between the reindexing calculation and the final
boundedness estimate in the proof of self-improvement.
Helper-stage boundedness from the scalar comparison and the off-diagonal estimate.
The helper boundedness gap decomposes as
⟨Z ⊗ I⟩ - ⟨I ⊗ Hhat.total⟩ plus the off-diagonal average from
helper_boundedness_slack_average_ev_eq_off_diagonal_avg. Thus the comparison
⟨Z ⊗ I⟩ - ⟨I ⊗ Hhat.total⟩ ≤ 3 √δ, together with the off-diagonal estimate
≤ 4 √ζ_variance, gives the helper threshold after applying
helper_boundedness_error_le_selfImprovementHelperError.
Helper-stage boundedness from the scalar comparison and the
point-consistency add-in-u transfer.
This theorem composes the off-diagonal estimate supplied by
pointConsistencyAddInUSelection with
helper_boundedness_gap_le_selfImprovementHelperError. It is the formal
statement of the sentence "combined with the explicit A-consistency bound" in the
boundedness paragraph of the self-improvement proof.
Convert the helper-completeness Hhat-versus-Z comparison to the
right-placed total comparison used in the boundedness gap.
The helper-completeness paragraph naturally proves
⟨ψ, Z ⊗ I⟩ - 3√δ ≤ subMeasMass ψ Hhat.liftLeft. The boundedness decomposition,
however, uses the right-placed total ⟨ψ, I ⊗ Hhat.total⟩. On the
permutation-invariant strategy state these scalars agree, so the comparison
becomes ⟨ψ, Z ⊗ I⟩ - ⟨ψ, I ⊗ Hhat.total⟩ ≤ 3√δ.
Helper-stage boundedness from the actual helper comparison and the
point-consistency add-in-u transfer.
This theorem composes the helper-completeness comparison Hhat-versus-Z
with the boundedness off-diagonal estimate. Complementary slackness remains an
explicit hypothesis because the reduced SelfImprovementHelperConclusion
records only the presently formalized SDP facts. The off-diagonal transfer is
likewise explicit: it is the formal statement of the add-in-u application
with S_u = {(a,h) : h(u) ≠ a}.
Transport the helper boundedness gap through the data-processing
approximation between Hhat and H.
The input hdata is exactly the data-processing SDD bound already produced
inside selfImprovement. The conclusion says that replacing the helper
polynomial family in the point-agreement average by the projective family costs
at most sqrt ε, matching Proposition easy-approx-from-approx-delta in the
boundedness paragraph of the paper.
Compare the final projective residual with the helper boundedness gap for the same projective family.
This is the SDP dual-slack step in the projective boundedness paragraph of
thm:self-improvement (references/ldt-paper/self_improvement.tex, lines
742--749): the term Z ⊗ H_h in the projective residual dominates
(E_u A^u_{h(u)}) ⊗ H_h for each polynomial h, and summing these inequalities
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
comparator above and the existing data-processing transport produce the final
projective residual at the paper's natural error
selfImprovementHelperError + sqrt selfImprovementDataProcessingError. The
separate numerical absorption into the literal selfImprovementError threshold
is intentionally not hidden in this theorem.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
This is a source-faithful construction step for the final-fields boundedness
conclusion.
Literal-threshold projective-residual construction.
This theorem combines final_fields_projective_residual_bound_natural with a separately
named numerical absorption lemma. The analytic inputs are only the helper-stage
boundedness estimate, dual feasibility from SelfImprovementHelperConclusion,
and the data-processing SDD output already produced inside selfImprovement.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
This is a source-faithful construction step for the final-fields boundedness
conclusion.
Literal-threshold projective-residual construction under the standard unit-interval smallness hypotheses.
This derived theorem follows from
final_fields_projective_residual_bound: the numerical absorption input is
provided by
final_fields_projective_residual_error_le_selfImprovementError, so callers
only need the helper-stage boundedness estimate, data-processing output, and
the usual smallness assumptions on eps, delta, and d/q.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
This is a source-faithful construction step for the final-fields boundedness
conclusion.
Final projective-residual construction from helper outputs and the
point-consistency add-in-u transfer.
The theorem proves the boundedness part of the final-fields construction once the
orthonormalization data-processing estimate is available. It supplies the
helper-stage boundedness estimate from the helper comparison, complementary
slackness, point self-consistency, and the off-diagonal add-in-u transfer,
then applies the standard data-processing transport and numerical absorption
into selfImprovementError.
Paper source: references/ldt-paper/self_improvement.tex lines 742--755.
This is a source-faithful construction step for the final-fields boundedness
conclusion.
Final-fields constructor for the BoundedByOperator conclusion.
If the SDP dual witness dominates the identity, then the left-placed mass of any
submeasurement is dominated by Z ⊗ I: the total bound A.total ≤ 1 ≤ Z lifts
by monotonicity to leftTensor A.total ≤ leftTensor Z, and evaluation against
the state preserves this order. Consequently bndError ψ A.liftLeft (Z ⊗ I) = 0,
so the boundedness statement holds at any nonnegative tolerance. The
selfImprovement proof uses this constructor instead of requiring a combined
boundedness-field hypothesis.