A box cut by one balance equation has graph diameter at most the number of coordinates

Proved

Hirsch.box_slice_diameter_le_dimension

by jjosh · Sep 8, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-geometrypolytopes

For any real capacities cap indexed by Fin d and any real total, the set of x with 0 <= x_k <= cap_k and sum x_k = total has vertex-edge graph diameter at most d. Negative capacities simply make it empty; zero-width coordinates and dimension zero are included. The proof constructs maximal two-coordinate edges with a strictly decreasing mismatch-plus-mixed-buffer potential. This is a restricted one-balance box theorem, not a general polynomial Hirsch bound.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
open Set Hirsch

Formal statement

theorem Hirsch.box_slice_diameter_le_dimension (d : ℕ) (cap : Fin d → ℝ) (total : ℝ) :
    DiamLE {x : Fin d → ℝ | (∀ k, 0 ≤ x k ∧ x k ≤ cap k) ∧ ∑ k, x k = total} d  := by sorry

Source

Constructive formalization in jjoshua2/prove2me-work, chatgpt/box-slice-pivot. Related two-row transportation bounds are known; no literature-priority claim.

View graph