Read-back: Def_SmaleNinth_KleeMinty

All indices below are 0-based: row indices range over $i \in \{0, 1, \dots, n-1\}$ and column indices over $j \in \{0, 1, \dots, 2n-1\}$. When $n = 0$ every one of these index sets is empty, so all five data definitions are the empty matrix/vector/map and are trivially well-formed.

kleeMintyA

For each natural number $n$, this is the $n \times 2n$ real matrix $A$ whose entry in row $i \in \{0,\dots,n-1\}$ and column $j \in \{0,\dots,2n-1\}$ is

$$A_{ij} = \begin{cases} 2 \cdot 10^{\,i-j} & \text{if } j < n \text{ and } j < i,\\ 1 & \text{if } j < n \text{ and } j = i,\\ 0 & \text{if } j < n \text{ and } j > i,\\ 1 & \text{if } j \ge n \text{ and } j = n + i,\\ 0 & \text{if } j \ge n \text{ and } j \ne n + i. \end{cases}$$

The exponent $i - j$ is natural-number (truncated) subtraction, but it is only used in the branch where $j < i$, where it agrees with ordinary subtraction and is at least $1$. So row $i$ reads: entries $2\cdot 10^{i-j}$ in the columns $j = 0,\dots,i-1$, a $1$ in column $i$, zeros in columns $i+1,\dots,n-1$, a $1$ in column $n+i$, and zeros in the remaining columns $\ge n$.

kleeMintyb

For each natural number $n$, the vector $b \in \mathbb{R}^n$ with

$$b_i = 100^{\,i} \qquad (i = 0, \dots, n-1),$$

so in particular $b_0 = 1$ (when $n \ge 1$).

kleeMintyc

For each natural number $n$, the vector $c \in \mathbb{R}^{2n}$ with

$$c_j = \begin{cases} -\,10^{\,n-1-j} & \text{if } j < n,\\ 0 & \text{if } n \le j < 2n. \end{cases}$$

The exponent $n - 1 - j$ is again natural-number truncated subtraction; in the branch $j < n$ one has $j \le n-1$, so it agrees with the ordinary value $n-1-j \ge 0$. Thus $c_0 = -10^{n-1}$, decreasing in magnitude down to $c_{n-1} = -10^0 = -1$, and $c_j = 0$ on the last $n$ coordinates. (For $n = 0$ there are no coordinates at all.)

kleeMintySlackBasis

For each natural number $n$, the injective map $B \colon \{0,\dots,n-1\} \hookrightarrow \{0,\dots,2n-1\}$ given by

$$B(i) = n + i .$$

This is only a function selecting $n$ of the $2n$ column indices (the last $n$ of them), packaged with a proof of injectivity. Nothing in the definition asserts that the corresponding columns of any matrix form a basis, are linearly independent, or that any associated basis matrix is invertible.

kleeMintySlackSolution

For each natural number $n$, the vector $x \in \mathbb{R}^{2n}$ with

$$x_j = \begin{cases} 0 & \text{if } j < n,\\ 100^{\,j-n} & \text{if } n \le j < 2n, \end{cases}$$

where $j - n$ is natural subtraction, well-defined in the used branch since $j \ge n$; equivalently $x_{n+i} = 100^{\,i}$ for $i = 0,\dots,n-1$. Nothing in the definition asserts that this vector is feasible for any system, or that it is the basic solution associated with any basis; it is just this explicit vector.

IsDantzigPivot

Fix natural numbers $m, n$, a real $m \times n$ matrix $A$, a cost vector $c \in \mathbb{R}^n$, an injective map $B \colon \{0,\dots,m-1\} \hookrightarrow \{0,\dots,n-1\}$, a vector $x \in \mathbb{R}^n$, a second injective map $B'$ of the same type, and a vector $x' \in \mathbb{R}^n$. (Injectivity of $B$ and $B'$ is built into their type; no other property of them — and no property of $x$ such as feasibility, nonnegativity, or being a basic solution — is assumed.)

Two auxiliary quantities, both defined via Lean's total matrix inverse:

• the basis matrix $A_B$ is the $m \times m$ matrix with $(A_B)_{ik} = A_{i,\,B(k)}$ (columns of $A$ selected by $B$);
• $A_B^{-1}$ denotes Lean's matrix inverse, which is the true inverse when $A_B$ is invertible and the zero matrix otherwise (a junk value; no hypothesis in this predicate rules that case out);
• the pivot column at index $j$ is the vector $u = u(j) = A_B^{-1} A_j \in \mathbb{R}^m$, where $A_j$ is the $j$-th column of $A$ (so $u = 0$ identically when $A_B$ is not invertible);
• the reduced cost of index $j'$ is

$$\bar{c}_{j'} = c_{j'} - c_B^\top \bigl(A_B^{-1} A_{j'}\bigr), \qquad c_B = \bigl(c_{B(0)}, \dots, c_{B(m-1)}\bigr),$$

which degenerates to $\bar{c}_{j'} = c_{j'}$ when $A_B$ is not invertible;

• the basic direction at $j$ is the vector

$$d = e_j - \sum_{i=0}^{m-1} u_i \, e_{B(i)} \in \mathbb{R}^n,$$

where $e_k$ is the $k$-th standard basis vector (this formula is applied as written, with no separate assumption inside it that $j$ avoids the range of $B$).

The predicate $\operatorname{IsDantzigPivot}(A, c, B, x, B', x')$ asserts: there exist an index $j \in \{0,\dots,n-1\}$ and a row $\ell \in \{0,\dots,m-1\}$ such that all of the following hold (writing $u = u(j)$ throughout):

1. Pivot step core (the unfolded $\operatorname{IsPivotStepAt}$ at $(j,\ell)$), a conjunction of six conditions:

   • $j$ is not in the range of $B$ (i.e. $j \ne B(i)$ for every $i$);
   • $\bar{c}_j < 0$;
   • $u_\ell > 0$;
   • $B'(i) = B(i)$ for every $i \ne \ell$;
   • $B'(\ell) = j$;
   • $x' = x + \dfrac{x_{B(\ell)}}{u_\ell}\, d$ as an exact equality of vectors in $\mathbb{R}^n$ (the division is well-defined in the real numbers since $u_\ell > 0$ is asserted; note the step length is $x_{B(\ell)}/u_\ell$, whatever the sign of $x_{B(\ell)}$, with no requirement that it be nonnegative).

2. Ratio test on the exit row: for every row $i$ with $u_i > 0$,

$$\frac{x_{B(\ell)}}{u_\ell} \;\le\; \frac{x_{B(i)}}{u_i}.$$

3. Entering-index minimality: for every column index $j' \in \{0,\dots,n-1\}$ — the quantifier ranges over all $n$ indices, basic ones and $j$ itself included, not only nonbasic ones —

$$\bar{c}_j \;\le\; \bar{c}_{j'}.$$

That is, $\bar{c}_j$ is a minimum of the reduced costs over all columns; nothing constrains which minimizer is chosen when several attain the minimum, and the comparison is non-strict throughout.

Since the whole predicate is a bare existential over $j$ and $\ell$, it holds as soon as some such pair exists; it does not assert uniqueness of $(j, \ell)$, of $B'$, or of $x'$.