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.
A two-resource allocation LP and its central path
Example
Allocate one unit between two resources by minimizing subject to and . The exact optimum is , at .
Facts & Assumptions
Given: The LP, the strict-interior logarithmic barrier objective , and the exact candidate , at .
The exact central point has gap at most (Exact central points have barrier gap m/t or nu/t).
For valid inputs with positive-definite restricted barrier Hessian and finite primal value, the short-step theorem gives the stated count from a strictly feasible centered start, provided the exact Newton solver is supplied and the finite caps permit all required updates (Short-step path following takes Newton steps).
The orthant log barrier has parameter (The orthant logarithmic barrier has parameter equal to its dimension).
Verification
Substituting , stationarity of the barrier objective gives , or . Multiplying by and using yields . Its roots are ; because , only the plus root is positive. Thus , and rationalizing gives . These coordinates sum to one and satisfy stationarity. The restricted second derivative is , so the stationary point is the unique exact central point. At these become the values in Given, whose reciprocal difference is ; hence the supplied start is exact and its decrement is zero.
The central inequality multipliers are . Their difference is , so the equality multiplier satisfies both dual stationarity equations. Every primal feasible vector has objective , while attains , so and the objective excess is . The primal-dual gap is ; hence by [F1]. By [F3], . For , put , supply exact solves of the scalar restricted Newton equations, and choose and . Their scalar Hessian is positive by step 1.1. With the exact start from that step and , all hypotheses of [F2] hold, so at most path updates suffice, with at most two corrections each.
Depends on
- Conic, LP, and convex QP primal-dual models
- Log-barrier central paths and primal-dual Newton residuals
- The orthant logarithmic barrier has parameter equal to its dimension
- Exact central points have barrier gap m/t or nu/t
- Short-step path following takes $O(\sqrt{\nu}\log(\nu/(\varepsilon t_0)))$ Newton steps
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
15 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 15: Path-following methods (standard reference, not scraped)
- Hamza Fawzi, Topics in Convex Optimisation, Lecture 16: LP, SOCP, and SDP (standard reference, not scraped)