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.
Strict feasibility, boundary feasibility, and a weakly infeasible SDP
Example
Two affine slices of illustrate why Phase I must report a zero margin as inconclusive.
Facts & Assumptions
Given: The positive-semidefinite cone and the Phase-I margin model of The conic phase-I margin separates strict feasibility but may leave weak infeasibility undecided.
exactly when for every , and the cone is self-dual (The positive semidefinite cone is self-dual and its log determinant barrier has parameter n).
A zero Phase-I margin alone does not decide feasibility (The conic phase-I margin separates strict feasibility but may leave weak infeasibility undecided).
Verification
The slice , is feasible at but has no positive-definite point: a symmetric matrix in the slice is . If , the vector gives , so is not positive semidefinite; if , it is singular. Its Phase-I margin with is , since for and is impossible for by testing the second coordinate.
Every matrix in the slice , has form . If , the vector gives quadratic form ; if , vector gives ; if , vector gives . Thus the slice is infeasible. For , the matrix is positive semidefinite because its quadratic form is ; its Frobenius distance from is . For any , choose . Then has quadratic form , which is positive for every nonzero , so it is positive definite and is Phase-I feasible. If , the lower-right diagonal entry of is , so it cannot be positive semidefinite. Hence the Phase-I infimum is zero and is not attained.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
13 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
- Stephen Boyd and Lieven Vandenberghe, Convex Optimization (standard reference, not scraped)
- Hamza Fawzi, Topics in Convex Optimisation, Lecture 16 (standard reference, not scraped)