Section 9 — Saturated canonical SDP witnesses

This module contains the zero-slack variant of the canonical SDP output used in the self-improvement argument. The canonical block SDP supplies a feasible matrix X; when its slack diagonal block is zero, the extracted polynomial blocks form a complete measurement without using the auxiliary dominance condition (I \le Z).

References

• references/ldt-paper/self_improvement.tex

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockFamily (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : MatrixSdpCanonicalBlockIndex params → MakingMeasurementsProjective.MatrixOperator model.space

Move the canonical primal slack block into the distinguished polynomial block.

Paper origin: references/ldt-paper/self_improvement.tex:177-190. The paper passes from an optimal canonical block matrix to a saturated paper primal measurement. This block family implements the source-faithful completion step: the none block is set to zero, and its positive mass is added to the fixed polynomial block sdpDistinguishedPolynomial params. This avoids the auxiliary route which proves saturation from an additional bound I ≤ Z.

Equations

• One or more equations did not get rendered due to their size.
• MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockFamily params model X none = 0

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockFamily_none (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : matrixSdpCanonicalSaturateSlackBlockFamily params model X none = 0

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockFamily_some (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (g : Polynomial params) : matrixSdpCanonicalSaturateSlackBlockFamily params model X (some g) = matrixSdpCanonicalDiagonalBlock params model X (some g) + if g = sdpDistinguishedPolynomial params then matrixSdpCanonicalDiagonalBlock params model X none else 0

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockMatrix (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)

The saturated canonical matrix obtained by completing the slack at the distinguished polynomial block.

This is a source-faithful replacement for the Lean-only saturation route through I ≤ Z: it changes only the primal matrix, setting the extra canonical slack block to zero and adding that block to sdpDistinguishedPolynomial params.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_saturateSlackBlockMatrix_none (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalSaturateSlackBlockMatrix params model X) none = 0

The saturated canonical matrix has zero extra slack block.

@[simp]

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDiagonalBlock_saturateSlackBlockMatrix_some (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (g : Polynomial params) : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalSaturateSlackBlockMatrix params model X) (some g) = matrixSdpCanonicalDiagonalBlock params model X (some g) + if g = sdpDistinguishedPolynomial params then matrixSdpCanonicalDiagonalBlock params model X none else 0

The polynomial blocks of the saturated canonical matrix agree with the original diagonal blocks, except that the distinguished polynomial receives the old none slack block.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockMatrix_feasible (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : MatrixSdpCanonicalPrimalFeasible params model (matrixSdpCanonicalSaturateSlackBlockMatrix params model X)

Feasibility is preserved by moving the none slack block into sdpDistinguishedPolynomial params.

The proof uses only positivity of principal diagonal blocks of the original feasible canonical matrix and the canonical equality constraint. It is the source-faithful saturation step corresponding to references/ldt-paper/self_improvement.tex:182-190, avoiding any use of an auxiliary dominance hypothesis I ≤ Z.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalObjective_trace_saturateSlackBlockMatrix (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) : (matrixSdpCanonicalObjectiveOperator params model * matrixSdpCanonicalSaturateSlackBlockMatrix params model X).trace.re = (matrixSdpCanonicalObjectiveOperator params model * X).trace.re + (matrixAveragedPointOperator params model (sdpDistinguishedPolynomial params) * matrixSdpCanonicalDiagonalBlock params model X none).trace.re

Exact objective formula for source-faithful slack saturation.

After the none block is moved to sdpDistinguishedPolynomial params, the canonical objective increases by the trace pairing of the old slack block with the averaged point operator for that distinguished polynomial. The none block itself has objective coefficient zero, which is why this completion is the paper-faithful alternative to deriving saturation through an auxiliary I ≤ Z hypothesis.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalObjective_trace_le_saturateSlackBlockMatrix (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re ≤ (matrixSdpCanonicalObjectiveOperator params model * matrixSdpCanonicalSaturateSlackBlockMatrix params model X).trace.re

Saturating the canonical slack block cannot decrease the canonical primal objective.

The added objective term is nonnegative because the distinguished averaged point operator is positive semidefinite and the original none block is a positive principal block of the feasible canonical matrix.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalSaturateSlackBlockMatrix_strongDuality (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hdual : ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) (hstrong : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re = matrixSdpDualObjective model Z) : (matrixSdpCanonicalObjectiveOperator params model * matrixSdpCanonicalSaturateSlackBlockMatrix params model X).trace.re = matrixSdpDualObjective model Z

Objective equality survives source-faithful slack saturation.

If a feasible canonical primal matrix and a dual-feasible Z have equal objective values, then the saturated matrix obtained by moving the slack block to sdpDistinguishedPolynomial params has the same objective value. The proof combines objective monotonicity of the completion with canonical weak duality; it does not use the auxiliary dominance condition I ≤ Z.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpPrimalTotalEqOne_extracted_of_canonicalSlackBlock_eq_zero (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (hSlack : matrixSdpCanonicalDiagonalBlock params model X none = 0) : ∑ g : Polynomial params, (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX).effect g = 1

Vanishing of the slack diagonal block saturates the extracted paper primal submeasurement.

This is the paper-faithful replacement for deriving saturation from an auxiliary lower bound on the dual variable: if the canonical optimal solution is supplied with zero slack block, then the extracted family satisfies ∑_g T_g = I directly.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpOptimalWitness_of_canonicalSaturatedComplementarySlackness (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hdual : ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) (hstrong : matrixSdpPrimalObjective params model T = matrixSdpDualObjective model Z) (hcanonical : matrixSdpCanonicalPrimalBlockMatrix params model T * (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model) = 0) (hSlack : matrixSdpCanonicalSlackOperator params model T = 0) : MatrixSdpOptimalWitness params model T Z

Assemble a paper-form optimal witness from canonical complementary slackness and an explicitly saturated slack block.

The hypotheses are precisely the canonical SDP data needed after the block-diagonal reduction: dual feasibility, equality of the primal and dual objectives, canonical complementary slackness, and zero slack block I - ∑_g T_g = 0. No dominance condition on the dual variable is used.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpOptimalWitness_of_canonicalFeasibleSaturatedComplementarySlackness (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hdual : ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) (hstrong : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re = matrixSdpDualObjective model Z) (hcanonical : X * (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model) = 0) (hSlack : matrixSdpCanonicalDiagonalBlock params model X none = 0) : MatrixSdpOptimalWitness params model (matrixSdpCanonicalExtractedPrimalSubmeasurement params model X hX) Z

Assemble a paper-form optimal witness from an arbitrary feasible canonical matrix with zero slack block.

The extracted polynomial diagonal blocks form the paper primal measurement. The zero slack block supplies normalization; the canonical objective and complementary-slackness equations are transported to the extracted submeasurement.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpStatementWithSlackness_of_canonicalSaturatedComplementarySlackness (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) model.space) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hdual : ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) (hstrong : matrixSdpPrimalObjective params model T = matrixSdpDualObjective model Z) (hcanonical : matrixSdpCanonicalPrimalBlockMatrix params model T * (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model) = 0) (hSlack : matrixSdpCanonicalSlackOperator params model T = 0) : MatrixSdpStatementWithSlackness params model

Assemble the canonical block-SDP conclusions as the matrix-level statement with an explicitly saturated slack block.

This is the statement form of matrixSdpOptimalWitness_of_canonicalSaturatedComplementarySlackness. It records the paper-form strong-duality output with the saturated canonical slack block as an explicit hypothesis, and it does not add an auxiliary dominance condition.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpStatementWithSlackness_of_canonicalFeasibleSaturatedComplementarySlackness (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (hX : MatrixSdpCanonicalPrimalFeasible params model X) (Z : MakingMeasurementsProjective.MatrixOperator model.space) (hdual : ∀ (g : Polynomial params), 0 ≤ matrixSdpDualSlackOperator params model Z g) (hstrong : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re = matrixSdpDualObjective model Z) (hcanonical : X * (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model) = 0) (hSlack : matrixSdpCanonicalDiagonalBlock params model X none = 0) : MatrixSdpStatementWithSlackness params model

Assemble the canonical block-SDP conclusions as the matrix-level statement with zero slack block.

For a feasible canonical primal matrix X, the hypothesis X_none,none = 0 is exactly the saturated form of the paper's final slack block assertion. The theorem extracts the polynomial diagonal blocks and records the resulting complete primal measurement and complementary-slackness equations.