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.
An infeasible Phase I problem and its Farkas certificate
Example
Consider , , and with . The equality matrix has full row rank.
Facts & Assumptions
Given: , , and .
Phase I revised simplex and rank reduction: Add artificial variables and solve the Phase I problem subject to , , starting at with artificial basis .
Phase I feasible-basis extraction and infeasibility certificate: If its minimum artificial-variable sum is positive, its returned vector yields a Farkas certificate , , so the original system is infeasible.
Verification
The third right-hand side is negative, so gives and . The Phase I point , satisfies and has objective .
The Phase I dual vector satisfies and . For any Phase I feasible , its objective is at least by multiplying the constraints by and using , , and . Thus the displayed feasible point attains the Phase I optimum .
The original Farkas vector is . Direct calculation gives and . Hence no can satisfy , as also follows from [F2].
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
7 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
- Dimitris Bertsimas and John N. Tsitsiklis, Introduction to Linear Optimization, §3.5 and §4.6 (standard reference, not scraped)
- Michel Goemans, MIT 18.310 Lecture Notes: Linear Programming, §2.5 (standard reference, not scraped)