Helper completeness: bracketed mass identities, the SDP, and reduced reductions #
The exact bracketed reindexing of the helper-stage mass, the paper-shaped completeness
assemblies, the SDP statement lem:sdp with complementary slackness, and the reduced addInU
reduction used by the surrounding self-improvement theorem: the counterpart of the vendored
SelfImprovement/Theorems/Results/HelperCompleteness/Bracketed.lean (under
MIPRE/Background/LIDT/MIPStarRE/LDT/) in the port of planning/c6b-plan.md (milestone M10,
section "Port conventions").
A strategy is a SymStrat params π K; T, Hhat and Z are local, in π, and the joint
operators are strategy.state.L and strategy.state.R in K βL[β] K. The vendored
Hhat.liftLeft is Hhat.liftLeft strategy.state, and subMeasMass, ConsRel,
BipartiteSSCRel and CompletenessAtLeast are those of the state. The vendored
Matrix.sum_mul/Matrix.mul_sum regrouping is Finset.sum_mul/Finset.mul_sum, and the
averaging step of helper_mass_eq_avg_pointwise_sandwich_sum is the keystone's
ev_leftTensor_averageOperatorOverDistribution, in place of the vendored
ev_opTensor_averageOperatorOverDistribution_left at B = 1. The vendored file has no swap or
density hypotheses.
The SDP producer. The vendored sdp_statement_with_slackness is unconditional: it is
finite-dimensional Slater duality, through the canonical block SDP of the matrix realization and
the bridge SelfImprovement/Theorems/Results/SdpMatrixBridge.lean. Here it is M9's summed
semidefinite form: Theorem 10 (MIPRE/Foundations/SummedSdp.lean,
MIPRE/Background/Orthonormalization/SdpMaximizer.lean), pulled back to the first player's
algebra by Doubling.exists_isSummedSdp_A (Co/Doubling/Sdp.lean) and read as the SDP statement
by SdpStatementWithSlackness.of_isSummedSdp (Co/SelfImprovement/Theorems/Statements.lean).
Theorem 10 maximizes over the faithful trace of a finite pair (reports/c6b-paper-proofs.md,
Β§5.1 and Β§5.3), so sdp_statement_with_slackness and sdp_slackness_measurement take
hS : strategy.state.toBipartite.IsFinitePair after strategy. Neither needs the absence of
abelian projections, ΞΆ > 0 or the doubling.
Dropped vendored files. The pairing script reads only ported files, so the two vendored inputs of the SDP producer that have no Co file are recorded here.
SelfImprovement/Theorems/Results/SdpMatrixBridge.lean(313 lines), the bridge from the finite-dimensional matrix SDP toSdpStatementWithSlackness. Its declarationsmatrixSdpPointRealizationOfStrategy,matrixAveragedPointOperator_ofPointRealization,matrixSdpDualSlackOperator_ofPointRealization,MatrixSdpCanonicalOptimalPair,ofFeasibleStrongDualitySaturateSlackBlock,toMatrixSdpStatementWithSlackness,toSdpOptimalPairWithSlackness,toSdpStatementWithSlackness,matrixSdpPointRealization_canonicalOptimalPairandmatrixSdpPointRealization_statementWithSlacknessare not ported: they are replaced by M9's summed form throughSdpStatementWithSlackness.of_isSummedSdpandDoubling.exists_isSummedSdp_A.SelfImprovement/MatrixRealization/(7 files, 3,667 lines, among themCanonical/SaturatedandCanonical/StrongDuality/Separation, the two modulesSdpMatrixBridgeimports): the canonical block SDP, Slater strong duality and slack-block saturation. Its only importer isSdpMatrixBridge, whose only importer is this file. It is replaced by Theorem 10 (MIPRE/Foundations/SummedSdp.lean,MIPRE/Background/Orthonormalization/SdpMaximizer.lean).
"Dropped" means that no Co declaration uses these files, which a constant-closure walk over the
built oleans confirms. They stay in the build's import closure through the classical imports:
Co AddInUStep34AndTransfer/{Factored,Selected,Transfer,Variance}, AddInUPointConsistency and
HelperSSC/Core import their vendored counterparts for classical lemmas, and each of those reaches
the vendored AddInUStep34AndTransfer/Factored, which imports the vendored version of this file,
which imports SdpMatrixBridge and through it MatrixRealization/Canonical/Saturated β¦
MatrixRealization/Base. Likewise MakingMeasurementsProjective/NaimarkCore, dropped by M8, stays
in the closure through Co SelfImprovement/Defs β vendored SelfImprovement/Defs. Moving those
classical declarations into modules that import neither would remove them
(planning/c6b-plan.md, "Departures in M10 and M11").
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 62--190 and 354--414blueprint/src/chapter/ch07_self_improvement.tex
Exact Hhat reindexing for the helper-stage left-placed mass.
Expanding Hhat = E_u H^u through subMeasMass (Hhat.liftLeft S) = ev (L Hhat.total),
swapping the placement 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.
The conclusion is exact (not approximate) and depends on no input-consistency or SDP hypotheses.
Operator-level fiberwise reindexing identity for the per-point sandwich
operator. Inside each fiber {h : h u = a} the inner A^u_{h(u)} is constant
(equal to A^u_a), and Finset.sum_mul/Finset.mul_sum pull this constant
factor through the sum over T_h. Mirrors the operator-level computation in
sandwichedPolynomialOutcomeOperatorAt_sum_le_one.
Per-point bracketing identity for the helper-stage left-placed mass.
Fiberwise reindexing by h β¦ h(u) and pulling A^u_a Β· _ Β· A^u_a through the
sum, the placement, 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, at a fixed
point u (before averaging). The conclusion is exact and depends on no
input-consistency, SDP, or self-consistency hypotheses.
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, composed with eq:bracketize-the-expression. The conclusion
is exact 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.
The vendored statement is unconditional: its proof is finite-dimensional Slater duality, through
the canonical block SDP of the matrix realization. Here the proof is M9's summed semidefinite
form: Theorem 10 (MIPRE.Orthonormalization.exists_isSummedSdp_finitePairA) maximizes over the
faithful trace of a finite pair (reports/c6b-paper-proofs.md, Β§5.1 and Β§5.3), so the port needs
hS, that the model's bipartite reading is a finite pair. Doubling.exists_isSummedSdp_A pulls
the solution back to π for A_g = averagedPointOperator params strategy g, which is positive,
hence self-adjoint, and SdpStatementWithSlackness.of_isSummedSdp reads it as the statement.
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
sdp_statement_with_slackness. As there, the vendored theorem is unconditional (finite-dimensional
Slater duality), and the port takes hS, that the model's bipartite reading is a finite pair,
because Theorem 10 uses the faithful trace of a finite pair (reports/c6b-paper-proofs.md, Β§5.1
and Β§5.3).
Reduced version of lem:add-in-u.
This keeps only the global-variance consequence used downstream, derived from the
post-triangle six-step edge-transport chain bound via
globalVarianceOfPointsFromTransportChainBound and localVarianceTransportChainBound. The
gamma and hgood arguments are retained so that this reduced theorem matches the surrounding
self-improvement API and can be strengthened back to the full paper statement without a
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
formalized here.