TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Weak duality for the finite SDP pair

Statement

For every primal-feasible $X$ and dual-feasible $y$ in Finite semidefinite primal-dual pair, $tr (C X) \leq b \cdot y$ . More precisely, $b \cdot y - tr (C X) = \sum_{j = 1}^{m} y_{j} (b_{j} - tr (A_{j} X)) + tr ⁣ ((\sum_{j = 1}^{m} y_{j} A_{j} - C) X),$ and every term on the right is nonnegative.

Facts & Assumptions

Given: $X ⪰ 0$ , $tr (A_{j} X) \leq b_{j}$ , $y_{j} \geq 0$ , and $D : = \sum_{j} y_{j} A_{j} - C ⪰ 0$ .

[F1]

Finite semidefinite primal-dual pair: these are the exact primal and dual feasibility conditions and trace sign convention.

[F2]

Trace is a linear functional on $M_{n} (F)$ : trace is linear.

[F3]

Trace of a product of positive semidefinite matrices is nonnegative: for positive semidefinite $P, Q$ , $tr (P Q) \geq 0$ .

Proof

technique · direct

1.1givenF1F2F3algebra

Expand $D = \sum_{j} y_{j} A_{j} - C$ and use [F2] to obtain the displayed identity. Each scalar term is nonnegative because both $y_{j}$ and $b_{j} - tr (A_{j} X)$ are nonnegative by [F1]. The remaining term is nonnegative by [F1] and [F3] applied to $D, X$ .

2.1step 1.1F1algebra∎

The right side of the identity in step 1.1 is a sum of nonnegative real numbers, so $b \cdot y - tr (C X) \geq 0$ , which is the claimed inequality. No feasibility beyond [F1], optimizer, or strong-duality assumption is used.

Depends on

Used by

A one-constraint scalar SDP and its dual Example

Dependency tree · two levels

21 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

https://arxiv.org/pdf/1705.01843v4 (standard reference, not scraped)