Theorem 4.2 — a small integral objective with the same optimal solutions and optimal dual bases

Proved

DiophantinePreprocessing.FrankTardos.same_optimal_solutions_and_dual_bases

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-approximationlinear-programmingp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1strongly-polynomial

Let $n \ge 0$ , let $w \in \mathbb{Q}^n$ be a rational objective and put $N = (n+1)! + 1$ . There is an integral vector $\tilde w \in \mathbb{Z}^n$ with

\|\tilde w\|_\infty \le 2^{4n^3} N^{n(n+2)}, \qquad N = (n+1)! + 1,

such that for every $m$ , every $m \times n$ matrix $A$ with entries in $\{0, +1, -1\}$ and every $b \in \mathbb{R}^m$ , with $P = \{x \in \mathbb{R}^n : Ax \le b\}$ :

a point $x \in P$ is $w$ -maximal if and only if it is $\tilde w$ -maximal;
a set of rows of $A$ is an optimal dual basis for $\max\{wx : Ax \le b\}$ if and only if it is an optimal dual basis for $\max\{\tilde w x : Ax \le b\}$ .

In the paper $\tilde w$ is the output of the preprocessing algorithm applied to $w$ and $N$ . The theorem lets any linear-programming algorithm whose running time is polynomial in $n$ and in the length of the objective be run on $\tilde w$ instead of $w$ , whose length is polynomial in $n$ alone, which is how polynomial algorithms over $0, \pm1$ polyhedra become strongly polynomial.

Formalization Note "The output of the preprocessing algorithm" is replaced by the guarantee it provides: the statement asserts the existence of an integral $\tilde w$ with the explicit size bound of the Output line (p. 55). $\tilde w$ is chosen before $A$ and $b$ , so one vector works for every $0, \pm 1$ matrix with $n$ columns and every right-hand side. The size bound is essential: without it a multiple of $w$ by a common denominator would satisfy the conclusion.

Preamble

import Mathlib
import Definitions.Def_DiophantinePreprocessing_FrankTardos_IsWMaximal
import Definitions.Def_DiophantinePreprocessing_FrankTardos_IsOptimalDualBasis

Formal statement

namespace DiophantinePreprocessing.FrankTardos

/-- Frank–Tardos, Theorem 4.2 (p. 58), existence form: for every rational `w ∈ ℚⁿ` there is an
integral `w̃` with `‖w̃‖∞ ≤ 2^{4n³} N^{n(n+2)}`, `N = (n+1)! + 1` (the output of the
preprocessing algorithm applied to `w` and `N`), such that for every matrix `A` with entries
`0, ±1` and every `b`: (i) `x ∈ P = {x : A x ≤ b}` is `w`-maximal iff it is `w̃`-maximal, and
(ii) a set of rows of `A` is an optimal dual basis for `max (w x : A x ≤ b)` iff it is one for
`max (w̃ x : A x ≤ b)`. -/
theorem same_optimal_solutions_and_dual_bases (n : ℕ) (w : Fin n → ℚ) :
    ∃ wt : Fin n → ℤ,
      (∀ j, |wt j| ≤ 2 ^ (4 * n ^ 3) * (((n + 1).factorial : ℤ) + 1) ^ (n * (n + 2))) ∧
      ∀ (m : ℕ) (A : Matrix (Fin m) (Fin n) ℤ),
        (∀ i j, A i j = -1 ∨ A i j = 0 ∨ A i j = 1) →
        ∀ b : Fin m → ℝ,
          (∀ x : Fin n → ℝ,
            IsWMaximal A b (fun j => (w j : ℝ)) x ↔ IsWMaximal A b (fun j => (wt j : ℝ)) x) ∧
          (∀ B : Finset (Fin m),
            IsOptimalDualBasis A b (fun j => (w j : ℝ)) B ↔
              IsOptimalDualBasis A b (fun j => (wt j : ℝ)) B) := by sorry

end DiophantinePreprocessing.FrankTardos

Source

Frank & Tardos, An application of simultaneous diophantine approximation in combinatorial optimization, Combinatorica 7(1) (1987), p. 58, Theorem 4.2 (with the preceding sentence defining w̃ and N = (n+1)! + 1); Output line p. 55; standing assumption of Sect. 4, p. 56

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Fix a natural number $n$ and a rational vector $w = (w_1,\dots,w_n) \in \mathbb{Q}^n$ (indexed by $\{0,\dots,n-1\}$ ). There is no other hypothesis on $n$ or $w$ . The statement says there exists an integer vector $\tilde w \in \mathbb{Z}^n$ with two properties.

(Size bound.) Every coordinate satisfies

|\tilde w_j| \;\le\; 2^{4n^3}\,\bigl((n+1)! + 1\bigr)^{n(n+2)} \qquad \text{for all } j,

computed exactly in the integers.

(Invariance.) The same $\tilde w$ works for every $m \in \mathbb{N}$ , every $b \in \mathbb{R}^m$ and every integer matrix $A \in \mathbb{Z}^{m\times n}$ whose entries all lie in $\{-1, 0, 1\}$ . Since $\tilde w$ is chosen before $m$ , $A$ and $b$ , it depends only on $n$ and $w$ . Here $w$ and $\tilde w$ are both read as real vectors through the exact embeddings $\mathbb{Q}\subset\mathbb{R}$ and $\mathbb{Z}\subset\mathbb{R}$ . For every such $m$ , $A$ and $b$ :

For every real vector $x \in \mathbb{R}^n$ :

\mathrm{IsWMaximal}(A, b, w, x) \iff \mathrm{IsWMaximal}(A, b, \tilde w, x).

For every finite set $B \subseteq \{0,\dots,m-1\}$ of row indices of $A$ :

\mathrm{IsOptimalDualBasis}(A, b, w, B) \iff \mathrm{IsOptimalDualBasis}(A, b, \tilde w, B).

The two predicates are not shown here. $\mathrm{IsWMaximal}$ and $\mathrm{IsOptimalDualBasis}$ are defined in separate files of this bundle, and I was given only their names and argument lists, not their definitions. So this read-back cannot say what they mean. In particular it cannot say whether they refer to the polyhedron $\{x : Ax \le b\}$ , whether they require $x$ to be feasible or $B$ to have a particular size or linear independence, or what they say when that system is infeasible or the objective is unbounded. The theorem only says that swapping $w$ for $\tilde w$ in the objective-vector argument leaves each predicate's truth value unchanged, with $A$ , $b$ and $x$ (or $B$ ) held fixed.

What the statement does not say. It is purely an existence claim. It names no algorithm and does not say how $\tilde w$ is computed. It says nothing about the sign of $\tilde w$ , about whether $\tilde w$ is nonzero, or about whether $\tilde w$ is unique. The bound above is always at least $1$ , so for example $\tilde w = 0$ is never ruled out by the bound alone.

Degenerate cases.

$n = 0$ : $\mathbb{Q}^0$ and $\mathbb{Z}^0$ each contain only the empty vector, so $\tilde w$ is the empty vector. The bound becomes $2^0 \cdot 2^0 = 1$ and is vacuous because there are no coordinates. Once both are read as real vectors, $w$ and $\tilde w$ are the same empty vector, so both equivalences hold trivially.
$m = 0$ : $A$ and $b$ are empty, the entry condition on $A$ holds vacuously, and the only choice of $B$ is $\emptyset$ .
$b$ arbitrary: $b$ may be any real vector, including one that makes $Ax \le b$ infeasible. What the equivalences then say depends entirely on the unseen definitions.

No division, natural-number subtraction, integral, supremum or other default-valued total function appears in the statement itself. The factorial is computed in $\mathbb{N}$ and embedded exactly into $\mathbb{Z}$ .

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph