Matrix SDP comparison

This file compares the concrete matrix-level SDP slackness interface with the abstract self-improvement SDP statement interface.

The comparison is intentionally split into two interfaces. The source-shaped matrix optimal witness supplies dual feasibility, complementary slackness, and the saturated canonical slack block needed for the abstract Section 9 statement. No auxiliary dominance bound I ≤ Z is part of this comparison theorem.

Mathlib provides the underlying finite-dimensional matrix order and convex-cone infrastructure used throughout this project, but it does not yet provide a ready-made finite-dimensional semidefinite-programming strong-duality theorem with complementary slackness in the shape needed here. Consequently this file does not reprove SDP duality. It only transports the project-local matrix witness MatrixSdpStatementWithSlackness to the abstract Section 9 interface. If a Mathlib SDP theorem is later available, its output should replace the project-local witness while the comparison theorem below should remain the comparison with the self-improvement notation.

References

• references/ldt-paper/self_improvement.tex
• blueprint/src/chapter/ch07_self_improvement.tex

noncomputable def MIPStarRE.LDT.SelfImprovement.matrixSdpPointRealizationOfStrategy {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : MatrixSdpRealization params

The point-measurement part of the matrix SDP realization associated to a strategy.

The present comparison only uses the point-measurement fields of MatrixSdpRealization, through matrixAveragedPointOperator and matrixSdpDualSlackOperator. The state field is therefore filled by the zero positive operator. This construction should not be used for state-dependent matrix expressions such as matrixExpectation; such expressions would compute with the zero operator rather than with strategy.state.

Equations

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

theorem MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator_ofPointRealization {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (g : Polynomial params) : matrixAveragedPointOperator params (matrixSdpPointRealizationOfStrategy params strategy) g = averagedPointOperator params strategy g

The averaged point operator for the point-measurement matrix realization is the abstract averaged point operator.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpDualSlackOperator_ofPointRealization {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (Z : Quantum.Op ι) (g : Polynomial params) : matrixSdpDualSlackOperator params (matrixSdpPointRealizationOfStrategy params strategy) Z g = sdpDualSlackOperator params strategy Z g

The matrix dual slack operator for the point-measurement matrix realization is the abstract dual slack operator.

structure MIPStarRE.LDT.SelfImprovement.MatrixSdpCanonicalOptimalPair (params : Parameters) [FieldModel params.q] (model : MatrixSdpRealization params) (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)) (Z : MakingMeasurementsProjective.MatrixOperator model.space) : Prop

Canonical primal-dual data with complementary slackness and zero slack block.

This is the paper-faithful canonical output still required from the strong-duality argument in lem:sdp: a feasible canonical primal matrix, a dual-feasible operator with the same objective value, canonical complementary slackness, and vanishing of the extra slack block (X_{\mathrm{none},\mathrm{none}}). The dominance condition (I \le Z) is not part of this structure.

• feasible : MatrixSdpCanonicalPrimalFeasible params model X
• dualFeasible (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model Z g
• strongDuality : (matrixSdpCanonicalObjectiveOperator params model * X).trace.re = matrixSdpDualObjective model Z
• complementarySlackness : X * (matrixSdpCanonicalDualOperator params model Z - matrixSdpCanonicalObjectiveOperator params model) = 0
• slackBlock_eq_zero : matrixSdpCanonicalDiagonalBlock params model X none = 0

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

Build a saturated canonical optimal pair by completing the primal slack block at sdpDistinguishedPolynomial params.

Paper origin: references/ldt-paper/self_improvement.tex:177-190. This is the source-faithful strong-duality slice: from a feasible canonical primal matrix, dual feasibility, and primal-dual objective equality, first move the none slack block into the distinguished polynomial block. The saturated matrix is still feasible, has zero none block, and keeps objective equality by objective monotonicity plus canonical weak duality. No auxiliary dominance hypothesis I ≤ Z is used.

theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpCanonicalOptimalPair.toMatrixSdpStatementWithSlackness {params : Parameters} [FieldModel params.q] {model : MatrixSdpRealization params} {X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params model)} {Z : MakingMeasurementsProjective.MatrixOperator model.space} (h : MatrixSdpCanonicalOptimalPair params model X Z) : MatrixSdpStatementWithSlackness params model

A saturated canonical optimal pair gives the matrix-level slackness statement without adding the auxiliary dominance condition.

theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpOptimalWitness.toSdpOptimalPairWithSlackness {ι : Type u_1} [Fintype ι] [DecidableEq ι] {params : Parameters} [FieldModel params.q] {strategy : SymStrat params ι} {T : MakingMeasurementsProjective.MatrixSubmeasurement (GlobalVariance.DegreeBoundedPolynomialAnswer params) (matrixSdpPointRealizationOfStrategy params strategy).space} {Z : Quantum.Op ι} (h : MatrixSdpOptimalWitness params (matrixSdpPointRealizationOfStrategy params strategy) T Z) : SdpOptimalPairWithSlackness params strategy T.toSubMeas Z

A matrix optimal witness gives the abstract slackness-carrying SDP pair.

theorem MIPStarRE.LDT.SelfImprovement.MatrixSdpStatementWithSlackness.toSdpStatementWithSlackness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (h : MatrixSdpStatementWithSlackness params (matrixSdpPointRealizationOfStrategy params strategy)) : SdpStatementWithSlackness params strategy

A matrix strong-duality statement for the point-measurement realization of a strategy implies the abstract slackness statement.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpPointRealization_canonicalOptimalPair {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : ∃ (X : MakingMeasurementsProjective.MatrixOperator (matrixSdpCanonicalBlockHilbertSpace params (matrixSdpPointRealizationOfStrategy params strategy))) (Z : Quantum.Op ι), MatrixSdpCanonicalOptimalPair params (matrixSdpPointRealizationOfStrategy params strategy) X Z

Canonical strong-duality and complementary-slackness construction for the point-measurement realization of the Section 9 SDP.

Paper origin: references/ldt-paper/self_improvement.tex lines 82--190 (\label{lem:sdp} and the proof using Slater's condition). The paper first rewrites the primal and dual SDPs in canonical block form, invokes strong duality, and then applies complementary slackness to obtain a saturated canonical optimal pair.

This is the source-faithful construction for the formalized SDP route. Its conclusion is the native canonical block-SDP output: a feasible canonical primal matrix, a dual-feasible operator with equal objective value, canonical complementary slackness, and a vanishing slack block. It does not assume the auxiliary dominance condition I ≤ Z; the saturated slack block is part of the expected strong-duality output. The matrix statement matrixSdpPointRealization_statementWithSlackness follows by extracting the diagonal polynomial blocks.

Tracked by issue #1230 and documented in docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.

theorem MIPStarRE.LDT.SelfImprovement.matrixSdpPointRealization_statementWithSlackness {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) : MatrixSdpStatementWithSlackness params (matrixSdpPointRealizationOfStrategy params strategy)

Matrix-level strong-duality and complementary-slackness statement for the point-measurement realization of the Section 9 SDP.

Paper origin: references/ldt-paper/self_improvement.tex lines 82--190 (\label{lem:sdp}), documented by docs/paper-gaps/issue-1230-self-improvement-sdp-usage.tex.

Source-faithful transport: This declaration is a proved extraction from the canonical optimal-pair construction for lem:sdp; it is not a conditional replacement for the SDP strong-duality theorem.

This theorem is a proved transport from the native canonical optimal-pair construction matrixSdpPointRealization_canonicalOptimalPair. It contains no additional dominance, bridge, residual, or package hypothesis.