Section 9 — Canonical matrix SDP dual and slackness layer #
This module contains the canonical objective and dual operators, the dual slack
block identities, and the slack-block saturation step used to extract the
paper-form primal normalization. The optimal-witness packages built from these
canonical facts live in MatrixRealization/Canonical/Witness.lean.
References #
references/ldt-paper/self_improvement.tex
The canonical objective matrix C = diag(A_g, 0) in the paper's block SDP.
Equations
- MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalObjectiveBlockFamily params model none = 0
- MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalObjectiveBlockFamily params model (some g) = MIPStarRE.LDT.SelfImprovement.matrixAveragedPointOperator params model g
Instances For
The canonical objective operator of the block SDP.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The block family representing the canonical dual operator associated to a
paper dual variable Z.
In the paper calculation this is
∑_{i,j} z_{ij} D_{ij}, which is the block-diagonal matrix with the same
operator Z on every canonical block.
Equations
- MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualOperatorBlockFamily params model Z x✝ = Z
Instances For
The canonical dual operator corresponding to a paper dual variable Z.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The block family for the canonical dual slack operator.
It has polynomial blocks Z - A_g and slack block Z, exactly as in the
canonical dual constraint obtained from the paper SDP.
Equations
- MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualSlackBlockFamily params model Z none = Z
- MIPStarRE.LDT.SelfImprovement.matrixSdpCanonicalDualSlackBlockFamily params model Z (some g) = MIPStarRE.LDT.SelfImprovement.matrixSdpDualSlackOperator params model Z g
Instances For
The canonical dual slack is the difference between the canonical dual operator and the canonical objective operator.
The canonical dual slack block matrix is positive semidefinite under paper dual feasibility.
The canonical dual constraint for the block SDP is the positivity of the block
diagonal operator with blocks Z - A_g on the polynomial summands and Z on
the slack summand. The polynomial blocks are precisely the paper dual
feasibility inequalities, while the slack block follows from the same
inequalities because the averaged point operators are positive.
Positivity of the canonical dual slack block matrix is equivalent to the
paper dual feasibility inequalities Z ≥ A_g.
The canonical dual constraint for Z is equivalent to the paper dual
constraints Z ≥ A_g.
Paper dual feasibility implies feasibility of the canonical block dual constraint.
Feasibility of the canonical block dual constraint recovers the paper dual inequalities.
The paper's strict dual witness Z = 2I is feasible for the canonical dual
constraint.
Every canonical dual-slack block of the strict dual witness dominates the identity.
The canonical strict dual slack dominates the identity on the block Hilbert space.
The canonical block matrix associated to the strict primal witness is feasible for the canonical primal SDP.
The slack block of the strict primal canonical matrix is (1/2)I.
Canonical block-SDP feasible bounds supplied by the explicit paper Slater-type witnesses.
This is not an optimality statement. It records the primal canonical
feasibility of the uniform family, the strict slack block (1/2)I, the
canonical dual constraint for Z = 2I, and the corresponding paper dual
feasibility data.
- primalFeasible : MatrixSdpCanonicalPrimalFeasible params model (matrixSdpCanonicalPrimalBlockMatrix params model (matrixSdpStrictPrimalSubmeasurement params model))
- primalSlackHalf : matrixSdpCanonicalDiagonalBlock params model (matrixSdpCanonicalPrimalBlockMatrix params model (matrixSdpStrictPrimalSubmeasurement params model)) none = (1 / 2) • 1
- canonicalDualFeasible : 0 ≤ matrixSdpCanonicalDualOperator params model (matrixSdpStrictDualWitness model) - matrixSdpCanonicalObjectiveOperator params model
- paperDualFeasible (g : Polynomial params) : 0 ≤ matrixSdpDualSlackOperator params model (matrixSdpStrictDualWitness model) g
- paperDualSlackDominatesIdentity (g : Polynomial params) : 1 ≤ matrixSdpDualSlackOperator params model (matrixSdpStrictDualWitness model) g
- canonicalDualSlackDominatesIdentity : 1 ≤ matrixSdpCanonicalDualOperator params model (matrixSdpStrictDualWitness model) - matrixSdpCanonicalObjectiveOperator params model
Instances For
The explicit uniform primal witness and Z=2I give the canonical feasible
bounds used before applying finite-dimensional SDP strong duality.
The canonical block objective evaluated on the block matrix associated to a paper primal submeasurement is the paper primal objective.
The paper writes this as Tr(C† X). In the present canonical model the
objective blocks are the averaged point operators, hence Hermitian measurement
effects averaged over points; the without-dagger trace pairing used here is the
same expression in this Hermitian case.
The strict primal canonical matrix has the paper primal objective of the strict primal submeasurement.
The canonical block objective evaluated on an arbitrary feasible canonical primal matrix is the paper primal objective of its extracted submeasurement.
This is the converse objective identity to
matrixSdpCanonicalObjective_trace_primalBlockMatrix: once a canonical feasible
matrix X is given, reading the polynomial diagonal blocks as T_g = X_{gg}
preserves the SDP objective value.
Replacing a feasible canonical matrix by the canonical block matrix of the extracted paper submeasurement preserves the canonical objective value.
Pairing the canonical dual operator with a feasible canonical primal matrix gives the paper dual objective.
The canonical equality constraint says that the sum of the diagonal blocks of
X is the identity. Since the canonical dual operator has the same block Z
on every summand, the trace pairing collapses to Tr Z, exactly the paper
dual objective.
The canonical primal-dual gap is the trace pairing with the canonical dual slack operator.
This is the algebraic identity behind weak duality for the canonical SDP: after
the dual trace pairing is identified with the paper dual objective, subtracting
the canonical objective leaves the trace pairing against D(Z)-C.
Canonical weak duality for the self-improvement SDP.
For a feasible canonical primal matrix (X) and a feasible canonical dual operator (D(Z)-C), the primal-dual gap is the trace pairing of two positive semidefinite operators. The preceding trace identity and positivity of this pairing give the usual weak-duality inequality.
Zero duality gap gives canonical complementary slackness.
This is the local algebraic consequence used after the Watrous strong-duality
theorem supplies an optimal feasible primal-dual pair with equal objective
values. The remaining hard part is producing such a pair from Slater's
condition; once it is available, this theorem converts the zero gap into the
product equation X * (D(Z) - C) = 0.
The diagonal block of a canonical primal-dual slack product is the product of the corresponding primal diagonal block and canonical dual slack block.
The concrete complementary-slackness defect T_g (Z - A_g).
Equations
- MIPStarRE.LDT.SelfImprovement.matrixSdpComplementarySlacknessDefect params model T Z g = T.effect g * MIPStarRE.LDT.SelfImprovement.matrixSdpDualSlackOperator params model Z g
Instances For
Multiplying the canonical primal block matrix by the canonical dual slack keeps only the blockwise products.
This is the formal block-diagonal calculation behind the paper's passage from
canonical complementary slackness to the equations
T_g (Z - A_g) = 0.
If a feasible canonical primal matrix satisfies canonical complementary slackness, then the block-diagonal matrix obtained from its polynomial diagonal blocks also satisfies canonical complementary slackness.
This is the formal version of the reduction in the SDP proof which permits one to replace an optimal canonical matrix by its block-diagonal part.
Canonical complementary slackness implies the paper-form defect equation
T_g (Z - A_g) = 0 on each polynomial block.
Canonical complementary slackness for a feasible canonical matrix gives the paper-form defect equation for the extracted paper primal submeasurement.
Canonical complementary slackness also gives the slack-block equation
S Z = 0, where S = I - ∑_g T_g.
Vanishing of the canonical slack block is exactly saturation of the paper primal submeasurement.