Motivation

A local improvement algorithm can reach an optimum without coming close to doing so quickly. A pivot rule chooses the next neighboring solution of a linear program. Cunningham’s rule uses a fixed cyclic order and remembers the last variable selected. It resumes its scan from that variable, choosing the first eligible entering variable. Avis and Friedmann prove exponential lower bounds for this rule in several connected optimization models. This mission treats that known result as a formal verification project. Avis and Friedmann, 2017.

Setting

The common optimization representation is a rational matrix $A$, a rational right-hand side $b$, and rational objective coefficients $c$. A feasible vector satisfies $Ax=b$ and $x_j\geq0$ for every coordinate. The objective is $c^Tx$. A basis selects one column for each equality constraint. It is valid only when these columns are distinct, their square matrix is nonsingular, and its inverse applied to $b$ has nonnegative coordinates. All other coordinates of the associated basic solution are zero.

An entering variable is nonbasic and has strictly positive reduced cost. A leaving row is chosen by the minimum ratio test, considering only positive entries of the transformed entering column. The basis changes by replacing that row’s selected column. The formal relation requires both endpoint bases to be feasible; a later theorem must prove strict objective increase for the particular family.

The parameter $n\geq3$ controls an explicit family with $5(n-1)$ equality constraints and $10(n-1)$ nonnegative variables. Column numbers follow the source’s ordering (1). The starting basis chooses the specified actions, including the exceptional action $e_1^1$. The occurrence of a variable in the cyclic scan is distinct from its entering the basis.

Formalization targets

The main target is the simplex lower bound. Let $T$ count pivots of a complete execution from the prescribed basis, and let $x_t$ be its basic solutions. The goal asserts the existence of such an execution with

$$T\geq 2^n,\qquad c^Tx_t<c^Tx_{t+1}\quad(0\leq t<T).$$

Supporting targets cover the same source’s parity-game, Markov-decision-process, and polytope-orientation results. The parity game uses a finite graph with a designated owner and natural-number priority at each vertex. Its valuation compares priority occurrence counts, since different vertices may have equal priorities. A positional strategy fixes one successor at every vertex owned by that player.

The eliminated-state decision process has two actions at every decision vertex. Each action supplies a rational immediate reward and a substochastic transition row; missing probability goes to an absorbing sink. Its policy values are the solution of the corresponding transient linear system. Separate targets establish that the transition rows are valid, the systems are invertible, and policy improvements coincide with simplex pivots.

The final companion target concerns an acyclic unique sink orientation of a cube. Every face must have exactly one sink and the directed graph must have no cycle. Its dimension is $5(n-1)$, while the required walk length is at least $2^n$. The realization condition uses actual extreme points and one-dimensional faces of the feasible rational polytope. A rational objective may resolve ties while retaining every original strict improvement. The cube walk scans both signed directions at each coordinate in the prescribed cyclic order.

Significance

The statement package distinguishes the optimization problem from the algorithm used to solve it. Its outputs include reusable basis, reduced-cost, ratio-test, cyclic-history, decision-process, and polytope-graph interfaces. Each lower-bound theorem remains an open proof obligation in this draft; successful elaboration establishes that the statement is meaningful Lean code, rather than establishing its mathematical truth. The intended contribution is a machine-checked reconstruction of a published result. Paper and publication record.

Difficulty

Local progress does not bound the number of distinct intermediate policies. A complete proof must control every eligible improvement while also retaining the cyclic cursor. The transition to linear programming additionally requires the chosen entering action to induce the minimum-ratio basis exchange. For the cube result, constructing an abstract directed graph is insufficient: its vertices and edges must match those of the specified feasible polytope.

Formalization scope

All coefficients and finite-dimensional vectors in the optimization layer are rational. Matrix inverses are guarded by explicit nonsingularity conditions. The complete-run definitions require a feasible start, a legal step at every counted time, and an optimal endpoint. Runtime, correctness, and long-execution conclusions are absent from input structures.

The linear program is derived from the source’s graph and general policy-to-LP transformation. It explicitly retains the rewards incurred by the aliases $b_1=c_1=g_1$ when random vertices are eliminated. Those terms differ from a literal reading of the displayed shorthand objective in Section 4.4. An independent source audit derives every action class and boundary case for arbitrary n. A separate Lean certificate proves the disputed local reward elimination and its agreement with the implemented coefficients. Two exact feasible points show that the omitted term is not a constant offset. The explicit initial state follows Sections 2.3 and 4.4; the all-zero-e shorthand in Sections 3.3 and 5.2 adds one preliminary switch. The MDP and AUSO targets use the common explicit counter start and are justified through the counter-run transfer, rather than by subtracting one from a lower bound. The realization predicate explicitly includes boundedness. Geometry is represented over rational points; the rational-to-real justification is recorded as a mathematical argument, not a checked Lean transport theorem. These audit results do not prove the open asymptotic targets.

Definitions precede theorem targets. Companion results remain in this mission, and the main theorem is not duplicated as a milestone. Proof contributions may develop the shared interfaces or the explicit family, but must preserve the declared starting states, signed-direction order, cardinalities, strictness, and termination requirements.

Selected references

• David Avis and Oliver Friedmann, An exponential lower bound for Cunningham’s rule, Mathematical Programming 161, 271–305 (2017), DOI. Published online in 2016.
• Author’s accepted manuscript, used for theorem numbering.
• Earlier arXiv version, with different theorem numbers.