Cramer–Hadamard solution bound for integer systems

Proved

SmaleNinth.integer_polyhedron_solution_bound

by ORdos · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

bit-complexitycramer-rulelinear-programmingpolyhedra

A feasible system of linear inequalities with integer coefficients cannot have all its solutions astronomically far from the origin: feasibility already forces a solution of controlled size, with a bound depending only on the number of variables and the size of the coefficients.

The assertion. Let $U \ge 1$ be an integer, let $A \in \mathbb{Z}^{m\times n}$ and $b \in \mathbb{Z}^m$ satisfy $|A_{ij}| \le U$ for all $i, j$ and $|b_i| \le U$ for all $i$ , and suppose the system has at least one real solution. Then it has a real solution $x$ with

|x_j| \;\le\; n!\;U^{\,n} \qquad \text{for every } j = 0, \dots, n-1 .

What the bound does and does not involve. It is a bound on each coordinate, hence on the sup-norm, and it depends only on the number $n$ of variables and the coefficient bound $U$ — the number $m$ of inequalities does not appear, however large it is. The solution produced is real; no rationality or integrality of $x$ is claimed, and none holds in general. Both $A$ and $b$ are bounded by the same $U$ , and $U \ge 1$ is required, so the hypotheses never force the data to vanish.

Why it matters here. This is the step that converts a geometric question into a question of bounded size. A feasible integer system is guaranteed to meet an explicit box $[-n!U^n,\, n!U^n]^n$ , so a search may be confined to that box, and the resulting volumes and radii are described by numbers whose logarithms are polynomial in $n$ and $\log U$ . Every polynomial-time algorithm for linear feasibility in the bit model rests on an estimate of this kind, and it is the first place where the magnitude of the data enters the complexity — which is precisely what the real-number formulation of the problem forbids.

Sharpness. The constant $n!\,U^n$ is the classical generous one and is not claimed to be optimal; only its logarithm's polynomial growth is used downstream, so any sharpening is a strengthening of this statement rather than a correction to it.

Preamble

import Definitions.Def_Polyhedron

/-!
The Cramer–Hadamard bound: a nonempty linear system with integer data has a
solution of explicitly bounded size.

Source: the classical size estimate underlying Khachiyan's theorem —
B. Korte, J. Vygen, *Combinatorial Optimization*, 6th ed., Springer, §4.1
(Size of Vertices and Faces), and Bertsimas–Tsitsiklis, *Introduction to
Linear Optimization*, §8.4; cf. A. Schrijver, *Theory of Linear and Integer
Programming*, Wiley 1986, Chapter 10. A point of a minimal face of
`{x | Ax ≥ b}` solves a nonsingular integer subsystem, so by Cramer's rule
and the crude expansion bound `|det| ≤ r!·Uʳ` on `r × r` integer matrices
with entries bounded by `U` (and `|det| ≥ 1` for a nonsingular integer
matrix), its components are bounded by `n!·Uⁿ`.

The bound `n!·Uⁿ` is the generous classical one; only its polynomial bit
size matters downstream.
-/

open Matrix LinearOptimization

/-- **Cramer–Hadamard solution bound** (Korte–Vygen §4.1;
Bertsimas–Tsitsiklis §8.4). If the system `Ax ≥ b` with integer entries
bounded by `U ≥ 1` has a real solution, it has one with every component
bounded by `n!·Uⁿ`. -/

Formal statement

theorem SmaleNinth.integer_polyhedron_solution_bound {m n : ℕ} (U : ℕ) (hU : 1 ≤ U)
    (A : Matrix (Fin m) (Fin n) ℤ) (b : Fin m → ℤ)
    (hA : ∀ i j, |A i j| ≤ (U : ℤ)) (hb : ∀ i, |b i| ≤ (U : ℤ))
    (hne : (polyhedron (A.map (Int.cast : ℤ → ℝ))
      (fun i => (b i : ℝ))).Nonempty) :
    ∃ x ∈ polyhedron (A.map (Int.cast : ℤ → ℝ)) (fun i => (b i : ℝ)),
      ∀ j, |x j| ≤ (n.factorial : ℝ) * (U : ℝ) ^ n := by sorry

Source

Classical; B. Korte, J. Vygen, Combinatorial Optimization, 6th ed., Springer, Section 4.1 (Size of Vertices and Faces); Bertsimas-Tsitsiklis, Introduction to Linear Optimization, Section 8.4; A. Schrijver, Theory of Linear and Integer Programming, Wiley 1986, Chapter 10. Stated with the generous bound n! U^n.

Read-back

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

Read-back: `SmaleNinth.integer_polyhedron_solution_bound`

What the statement literally asserts. Fix natural numbers $m$ and $n$ (both implicit, so they range over all values including $0$ ), a natural number $U$ with the hypothesis $1 \le U$ , an $m \times n$ matrix $A$ with integer entries $A_{ij} \in \mathbb{Z}$ (rows indexed by $i \in \{0,\dots,m-1\}$ , columns by $j \in \{0,\dots,n-1\}$ ), and a vector $b \in \mathbb{Z}^m$ . Two entry-bound hypotheses are stated as inequalities between integers, with $U$ cast into $\mathbb{Z}$ :

\forall i, j:\ |A_{ij}| \le U \qquad \text{and} \qquad \forall i:\ |b_i| \le U,

where $|\cdot|$ is the ordinary absolute value on $\mathbb{Z}$ .

The final hypothesis concerns the set

P \;=\; \{\, x \in \mathbb{R}^n \mid \bar{A} x \ge \bar{b} \,\},

where $\bar{A}$ and $\bar{b}$ are the entrywise casts of $A$ and $b$ from $\mathbb{Z}$ into $\mathbb{R}$ , and $\bar{A} x \ge \bar{b}$ means the componentwise (pointwise) inequality $\forall i:\ \bar{b}_i \le (\bar{A} x)_i$ — this is the unfolding of the custom definition polyhedron, the "general-form polyhedron" $\{x \mid Ax \ge b\}$ over $\mathbb{R}$ . The hypothesis is that $P$ is nonempty, i.e. the real linear system $\bar{A} x \ge \bar{b}$ has at least one real solution.

Conclusion. Under these hypotheses the theorem asserts the existence of a point $x \in P$ (so $x \in \mathbb{R}^n$ satisfying $\bar{A} x \ge \bar{b}$ componentwise) such that every component is bounded:

\forall j \in \{0,\dots,n-1\}:\quad |x_j| \;\le\; n! \cdot U^{\,n},

where the bound is the real number obtained by casting the natural number $n!$ (the factorial of the column dimension $n$ ) to $\mathbb{R}$ and multiplying by the $n$ -th power of the real cast of $U$ . The inequality is non-strict ( $\le$ ), the existential is plain existence (not uniqueness), and the bound uses the same $n$ (the number of variables/columns) in both the factorial and the exponent; $m$ (the number of constraints) does not appear in the bound.

Edge and degenerate cases silently included by the quantifiers.

$n = 0$ : the space $\mathbb{R}^0$ contains exactly one point (the empty vector). $P$ is nonempty exactly when $b_i \le 0$ for every $i$ (each row of $\bar{A} x$ is an empty sum, equal to $0$ ), and in that case the conclusion holds vacuously: the componentwise bound quantifies over $j \in \{0,\dots,n-1\} = \emptyset$ , so there is nothing to check (the bound itself would be $0! \cdot U^0 = 1$ , but it is never invoked).
$m = 0$ : there are no constraints, so $P = \mathbb{R}^n$ and the nonemptiness hypothesis holds automatically; the theorem then asserts the existence of some $x \in \mathbb{R}^n$ with all $|x_j| \le n! \cdot U^n$ (e.g. any point works only if it meets the bound; the claim is just that one such point exists).
$U$ is a natural number constrained by $1 \le U$ , so $U = 0$ is excluded by hypothesis; the entry bounds therefore cannot force $A$ or $b$ to be zero.
The hypotheses bound the entries of $A$ and $b$ by the same $U$ , and the nonemptiness is required over $\mathbb{R}$ (a real solution), not over $\mathbb{Q}$ or $\mathbb{Z}$ ; likewise the bounded solution produced is a real vector, with no rationality or integrality claim.

Human review

Endorsed by Community (Bot) · Sep 6, 2026
Endorsed by ORdos · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Cramer–Hadamard solution bound for integer systems

Read-back: SmaleNinth.integer_polyhedron_solution_bound

Read-back: `SmaleNinth.integer_polyhedron_solution_bound`