Read-back: SmaleNinth.klee_minty_dantzig_exponential

What the statement asserts. For every natural number $n$ with $1 \le n$, there exists a function

$$f : \mathbb{N} \longrightarrow \big(\text{injections } \{0,\dots,n-1\} \hookrightarrow \{0,\dots,2n-1\}\big) \times \big(\mathbb{R}^{2n}\big),$$

defined on all of $\mathbb{N}$ (write $f(k) = (B_k, x_k)$, where $B_k$ is an injective map from row indices $\{0,\dots,n-1\}$ into column indices $\{0,\dots,2n-1\}$, thought of as a choice of $n$ basic columns, and $x_k \in \mathbb{R}^{2n}$), such that the following five conjuncts hold. Only the values $f(0), f(1), \dots, f(2^n-1)$ are constrained; the values of $f$ at $k > 2^n - 1$ are completely arbitrary. The trajectory is existentially quantified: the theorem claims that some such sequence exists, not that every sequence satisfying the pivot rule behaves this way.

The fixed data (all indices 0-based). Throughout, $A = A^{(n)}$ is the $n \times 2n$ real matrix with entries, for row $i \in \{0,\dots,n-1\}$ and column $j \in \{0,\dots,2n-1\}$:

$$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 subtraction, but it is only used when $j < i$, so it equals the ordinary difference.) The right-hand side is $b \in \mathbb{R}^n$ with

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

so in particular $b_0 = 1$. The cost vector is $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}$$

again with natural-number subtraction in the exponent, which for $j < n$ equals the ordinary $n-1-j \ge 0$; e.g. $c_0 = -10^{n-1}$ and $c_{n-1} = -1$.

The initial state (conjuncts 1 and 2). $B_0$ is the specific injection $B_0(i) = n + i$ (each basic column is the slack column $n+i$), and $x_0$ is the specific vector

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

Conjunct 3 (simplex states). For every $k$ with $k \le 2^n - 1$ (an inclusive bound, so this covers the $2^n$ indices $k = 0, 1, \dots, 2^n-1$, including the final one), the pair $(B_k, x_k)$ is a simplex state for $(A, b)$, meaning the conjunction of:

• the $n$ columns $A_{B_k(0)}, \dots, A_{B_k(n-1)}$ of $A$ are linearly independent over $\mathbb{R}$;
• $x_k$ lies in the standard-form polyhedron: $A x_k = b$ and $x_k \ge 0$ componentwise;
• $x_k(j) = 0$ for every column index $j$ not in the image of $B_k$.

Conjunct 4 (Dantzig pivots). For every $k$ with $k < 2^n - 1$ (a strict bound, so this covers the $2^n - 1$ steps $k = 0, \dots, 2^n - 2$), the pair $(B_k, x_k)$ passes to $(B_{k+1}, x_{k+1})$ by a Dantzig pivot with respect to $(A, c)$. Unfolded, this says: there exist a column index $j \in \{0,\dots,2n-1\}$ and a row index $\ell \in \{0,\dots,n-1\}$ such that, writing $M_k$ for the $n \times n$ matrix whose columns are the basic columns $A_{B_k(0)},\dots,A_{B_k(n-1)}$ (in that order), $u = M_k^{-1} A_j \in \mathbb{R}^n$ for the pivot column, and

$$\bar c_{j'} \;=\; c_{j'} - c_{B_k}^{\top} M_k^{-1} A_{j'}$$

for the reduced cost of column $j'$ (where $c_{B_k} = (c_{B_k(0)},\dots,c_{B_k(n-1)})$ and $A_{j'}$ is the $j'$-th column of $A$; the matrix inverse here is a total operation that returns the zero matrix when $M_k$ is singular — no invertibility hypothesis appears inside this predicate itself), all of the following hold:

1. $j$ is not in the image of $B_k$ (the entering column is nonbasic);
2. $\bar c_j < 0$;
3. $u_\ell > 0$;
4. $B_{k+1}(i) = B_k(i)$ for every $i \ne \ell$, and $B_{k+1}(\ell) = j$;
5. $x_{k+1} = x_k + \dfrac{x_k(B_k(\ell))}{u_\ell}\, d$, where $d \in \mathbb{R}^{2n}$ is the $j$-th basic direction: $d_j$-component $1$ minus $\sum_{i=0}^{n-1} u_i$ placed at position $B_k(i)$ — i.e. $d(j) = 1$ contribution, $d(B_k(i))$ receives $-u_i$, and all other components are $0$ (formally $d = e_j - \sum_i u_i\, e_{B_k(i)}$);
6. the ratio test: for every row $i$ with $u_i > 0$, $\;\dfrac{x_k(B_k(\ell))}{u_\ell} \le \dfrac{x_k(B_k(i))}{u_i}$;
7. Dantzig's rule: for every column index $j' \in \{0,\dots,2n-1\}$ — the quantifier ranges over all columns, basic ones included, not only nonbasic ones — $\;\bar c_j \le \bar c_{j'}$; that is, the entering column attains the minimum reduced cost over all $2n$ columns. Ties are not further constrained.

(In items 5 and 6, the divisions are real-number division, which is a total operation; item 3 guarantees $u_\ell \ne 0$ for the step size itself.)

Conjunct 5 (optimal-terminal final basis). The basis $B_{2^n-1}$ (the first component of $f(2^n-1)$; the exponent uses natural-number subtraction, and since $n \ge 1$ one has $2^n - 1 \ge 1$) is an optimal terminal state for $(A, c)$: for every column index $j$ not in the image of $B_{2^n-1}$, the reduced cost $\bar c_j = c_j - c_{B_{2^n-1}}^{\top} M_{2^n-1}^{-1} A_j$ satisfies $\bar c_j \ge 0$. This final conjunct constrains only the basis $B_{2^n-1}$, not the vector $x_{2^n-1}$, and asserts nonnegativity of reduced costs — it does not itself assert that $x_{2^n-1}$ minimizes $c^\top x$ over the feasible set.

Bookkeeping of the index ranges. The state condition holds for $k \le 2^n-1$ (inclusive: $2^n$ states $k = 0,\dots,2^n-1$), while the pivot condition holds for $k < 2^n-1$ (strict: $2^n-1$ pivots, connecting state $k$ to state $k+1$ for $k = 0,\dots,2^n-2$). The hypothesis $1 \le n$ rules out $n = 0$; for $n \ge 1$ all natural-number subtractions above coincide with the ordinary ones in the ranges where they are used. The whole assertion is a single existential over $f$: one admissible trajectory with these properties exists.