LemmaStatement: 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.

Basic feasible solutions, extreme points, and basis existence

Statement

Let $A \in R^{m \times n}$ have full row rank and let $P (A, b)$ be the feasible set of Revised simplex standard-form linear program. For a feasible $x$ , define its support by $S (x) = {j : x_{j} > 0}$ . A set $C$ is convex if $t u + (1 - t) v \in C$ for all $u, v \in C$ and $0 < t < 1$ . A point $x \in C$ is an extreme point if every representation $x = t u + (1 - t) v$ with $u, v \in C$ and $0 < t < 1$ forces $u = v = x$ . Then $x$ is an extreme point of $P (A, b)$ if and only if the columns ${a_{j} : j \in S (x)}$ are linearly independent. This is equivalent to $x$ being a basic feasible solution for Basis dictionaries and reduced costs for revised simplex. In particular, every nonempty $P (A, b)$ has a basic feasible solution. The statement includes $m = 0$ using the empty-basis convention.

Facts & Assumptions

Given: A full-row-rank matrix $A$ , a vector $b$ , and a feasible point $x \in P (A, b)$ .

[F1]

Revised simplex standard-form linear program: Its feasible set is $P (A, b) = {x \in R^{n} : A x = b, x_{j} \geq 0 for every j}$ .

[F2]

Basis dictionaries and reduced costs for revised simplex: The basic vector $x (B)$ is defined by $x_{B} (B) = A_{B}^{- 1} b$ and $x_{j} (B) = 0$ for $j \in N$ ; the basis is primal feasible, and $x (B)$ is a basic feasible solution, exactly when $A_{B}^{- 1} b \geq 0$ .

Proof

1.1givenF1chooseconstructalgebra

If the support columns indexed by $S (x)$ are dependent, choose a nonzero vector $d$ supported on $S (x)$ with $A d = 0$ . Since each $x_{j} > 0$ on this finite support, choose $ε > 0$ smaller than $x_{j} / ∣ d_{j} ∣$ for every nonzero $d_{j}$ . Then $x + ε d$ and $x - ε d$ are distinct nonnegative solutions of $A z = b$ , and their midpoint is $x$ ; hence $x$ is not extreme.

1.2givenF1algebra

Suppose the support columns are independent and $x = t u + (1 - t) v$ for feasible $u, v$ and $0 < t < 1$ . For $j \notin S (x)$ , nonnegativity and $x_{j} = 0$ force $u_{j} = v_{j} = 0$ . Thus $u - v$ is supported on $S (x)$ and $A (u - v) = 0$ ; independence forces $u = v$ , and the convex-combination identity then gives $u = v = x$ . This proves extremality under its stated definition.

2.1givenF1step 1.1choosealgebra

If the support columns of a feasible point are dependent, take $d$ as in step 1.1 and choose its sign so some $d_{j} < 0$ . With $t = \min_{d_{j} < 0} x_{j} / (- d_{j}) > 0$ , the point $x + t d$ remains feasible, remains nonnegative, and has strictly fewer positive coordinates. Repeating this support reduction at most $n$ times gives a feasible point whose support columns are independent.

3.1F1F2step 2.1chooseconstruct

Because $A$ has rank $m$ , its columns span $R^{m}$ . Extend the independent support columns from step 2.1 to $m$ independent columns of $A$ by repeatedly taking the least-index column outside their current span; assigning zero to each added coordinate makes the reduced point the basic vector of that basis. It is therefore a basic feasible solution. When $m = 0$ , support reduction gives the zero vector and the empty list is the required basis.

4.1F1F2step 1.1step 1.2step 3.1∎

A basic feasible solution has support contained in an independent basis, so its support columns are independent and step 1.2 makes it extreme. Conversely, an extreme feasible point has independent support by step 1.1 and extends to a basis by step 3.1. Thus the three stated conditions are equivalent, and step 3.1 proves existence whenever $P (A, b)$ is nonempty.

Depends on

Used by

Bland-rule finite termination and optimal-basis existence Theorem

Dependency tree · one level

2 results within one dependency step 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, §§2.2–2.6 (standard reference, not scraped)
Michel Goemans, MIT 18.310 Lecture Notes: Linear Programming, §§1.2–2.3 (standard reference, not scraped)