Helper completeness: bracketed mass identities and reduced reductions #
This file contains the exact bracketed reindexing of the helper-stage mass, the
paper-shaped completeness assemblies, and the reduced addInU reduction used
by the surrounding self-improvement theorem.
References #
references/ldt-paper/self_improvement.texlines 354--414blueprint/src/chapter/ch07_self_improvement.tex
Exact Hhat reindexing for the helper-stage left-tensor mass.
Expanding Hhat = E_u H^u through subMeasMass ψ Hhat.liftLeft = ev ψ (Hhat.total ⊗ I),
swapping the leftTensor through the polynomial sum, and pulling the ev through
the per-outcome point average gives the paper identity
⟨ψ| Hhat ⊗ I |ψ⟩ = E_u Σ_h ⟨ψ| H^u_h ⊗ I |ψ⟩,
where H^u_h = A^u_{h(u)} · T_h · A^u_{h(u)} is
sandwichedPolynomialOutcomeOperatorAt. This is the algebraic opening of the
helper-stage completeness chain at
references/ldt-paper/self_improvement.tex, lines 354--356, mirrored at
blueprint/src/chapter/ch07_self_improvement.tex, lines 103--106.
The conclusion is exact (not approximate) and depends on no input-consistency
or SDP hypotheses. The remaining helper-completeness ingredients --- the
Cauchy--Schwarz reductions
(self_improvement.tex:360--403) onto a Z ⊗ I-shaped expression, and the
input-consistency dual-mass bound already supplied by
input_consistency_dual_mass_lower_bound --- compose against this identity.
Per-point bracketing identity for the helper-stage left-tensor mass.
Fiberwise reindexing by h ↦ h(u) and pulling A^u_a · _ · A^u_a through the
sum, leftTensor, and ev give the paper identity at a fixed point u:
Σ_h ⟨ψ| H^u_h ⊗ I |ψ⟩ = Σ_a ⟨ψ| (A^u_a · T_{[h(u) = a]} · A^u_a) ⊗ I |ψ⟩,
where H^u_h = A^u_{h(u)} · T_h · A^u_{h(u)} is
sandwichedPolynomialOutcomeOperatorAt, and the bracketed
T_{[h(u) = a]} = Σ_{h : h u = a} T_h is the inner fiber sum.
This is the identity eq:bracketize-the-expression of
references/ldt-paper/self_improvement.tex, lines 356--358 (mirrored at
blueprint/src/chapter/ch07_self_improvement.tex, lines 110--113), at a fixed
point u (before averaging). The conclusion is exact (not approximate) and
depends on no input-consistency, SDP, or self-consistency hypotheses; it is
purely an algebraic regrouping of Σ_h H^u_h by the value of h at u.
Composed with helper_mass_eq_avg_pointwise_sandwich_sum, this yields the
bracketed form helper_mass_eq_avg_pointwise_bracketed_sum of the helper-stage
Hhat ⊗ I mass, which is the starting point for the remaining
Cauchy--Schwarz reduction at self_improvement.tex:360--403 toward
eq:gonna-use-this-later-H-versus-Z.
Bracketed form of the helper-stage Hhat ⊗ I mass identity.
Combines helper_mass_eq_avg_pointwise_sandwich_sum with the per-point
bracketing identity helper_pointwise_sandwich_sum_eq_bracketed:
⟨ψ| Hhat ⊗ I |ψ⟩ = E_u Σ_a ⟨ψ| (A^u_a · T_{[h(u) = a]} · A^u_a) ⊗ I |ψ⟩,
where T_{[h(u) = a]} = Σ_{h : h u = a} T_h. This is the second equality in the
displayed completeness chain at
references/ldt-paper/self_improvement.tex, lines 354--358 (mirrored at
blueprint/src/chapter/ch07_self_improvement.tex, lines 103--113), composed
with the bracketing reindexing eq:bracketize-the-expression. The conclusion
is exact (not approximate) and depends on no input-consistency, SDP, or
self-consistency hypotheses.
The named bracketed helper-completeness quantity is exactly the
helper-stage Hhat ⊗ I mass for the averaged sandwiched family.
This is the Lean form of the equality labelled
eq:bracketize-the-expression, after composing the fiberwise reindexing with
the preceding expansion of Hhat as the average of the pointwise sandwiched
submeasurements.
The paper-shaped Hhat-versus-Z comparison assembled from the bracketed
expression, the two Cauchy--Schwarz estimates, and complementary slackness.
The first Cauchy--Schwarz hypothesis moves from the bracketed expression
E_u Σ_a ⟨ψ, (A^u_a T_[h(u)=a] A^u_a) ⊗ I ψ⟩ to
helperFirstMovedCompletenessQuantity. The second removes the remaining
right-register copy of A^u_a, giving helperLinearizedCompletenessQuantity.
The latter is then identified with the dual mass by the SDP
complementary-slackness equation.
The Hhat-versus-Z comparison from point self-consistency and
complementary slackness.
This is the helper-completeness comparison at
eq:gonna-use-this-later-H-versus-Z with the two Cauchy--Schwarz estimates
supplied internally by helper_first_move_abs_sub_bracketed_le_two_sqrt_delta
and helper_second_move_abs_sub_first_moved_le_sqrt_delta.
Helper-stage completeness from the paper-shaped Cauchy--Schwarz estimates, complementary slackness, and input consistency.
Compared with helper_completeness_of_cauchy_schwarz_input_consistency, this
version names the expression before the first Cauchy--Schwarz move exactly as
it appears in eq:bracketize-the-expression; the equality with the
Hhat-mass is supplied internally by
helperBracketedCompletenessQuantity_eq_mass.
Helper-stage completeness from point self-consistency, complementary slackness, and input consistency.
This theorem removes the two external Cauchy--Schwarz hypotheses from
helper_completeness_of_bracketed_cauchy_schwarz_input_consistency; both are
proved from the single point-measurement self-consistency hypothesis.
Extract the orientation of complementary slackness used by the helper completeness proof from the strengthened helper conclusion.
The Hhat-versus-Z comparison from point self-consistency and a helper
conclusion carrying SDP complementary slackness.
This is the version of eq:gonna-use-this-later-H-versus-Z whose inputs are a
single strengthened helper conclusion and point-measurement self-consistency,
rather than a separate family of slackness equations.
Helper-stage completeness from point self-consistency, a helper conclusion carrying SDP complementary slackness, and input consistency.
This theorem removes the standalone hslack hypothesis from
helper_completeness_of_self_consistency_complementary_slackness_input_consistency;
the slackness equations are read from
SelfImprovementHelperConclusionWithSlackness.
Paper-origin statement for lem:sdp with complementary slackness.
Paper origin: references/ldt-paper/self_improvement.tex lines 62--88 state
\label{lem:sdp} for the primal/dual SDP pair and assert optimal witnesses
{T_g}, Z with ∑ g, T_g = I and T_g Z = T_g A_g. Lines 168--190 prove
this by Slater strong duality and complementary slackness after passing through
the canonical SDP form.
The proof transports the formalized canonical optimal-pair output for the Section 9 SDP back to the paper's abstract notation. That canonical optimal pair is obtained from the finite-dimensional strong-duality argument and the slack-block saturation step in the matrix realization.
Displayed measurement and complementary-slackness conclusion of lem:sdp.
Paper origin: references/ldt-paper/self_improvement.tex lines 82--88 state
that the Section 9 SDP admits a primal family {T_g} with ∑ g, T_g = I and
a dual operator Z satisfying T_g Z = T_g A_g for every polynomial g.
This theorem extracts exactly that complete-measurement and slackness form from
the source-shaped SDP statement sdp_statement_with_slackness, whose proof now
derives the strong-duality and complementary-slackness witnesses from the
canonical Section 9 SDP argument.
Reduced version of lem:add-in-u.
This currently keeps only the global-variance consequence used downstream. It
now derives that consequence from the post-triangle six-step edge-transport
chain bound via globalVarianceOfPointsFromTransportChainBound. The gamma and
hgood arguments are intentionally retained so this reduced theorem still
matches the surrounding self-improvement API and can be strengthened back to the
full paper statement without another caller-wide signature change. The
selection-dependent transfer inequality from the paper, together with its
dependence on an auxiliary family M and the averaged family H, is not yet
formalized here.