The cube blend has combinatorial diameter exactly $2d-1$

Proved

Hirsch.cube_blend_diameter

by elmismisimoxhunca · Sep 7, 2026 · Mathlib c5ea003 (Lean v4.30.0)

hirsch-conjecturepolytopes

For $d\ge2$ the polytope blendPoly d satisfies $\mathrm{DiamLE}(P,2d-1)$ , and the two antipodal vertices $v_+([d])$ , $v_-([d])$ are joined by no padded walk of length $2d-2$ . Distances are $|S\triangle T|$ within a lobe and $|S|+|T|\mp1$ across lobes according to whether $S\cap T$ is nonempty, so the diameter is $2d-1<n-d=2d$ : the polytope satisfies the Hirsch bound while having exponentially small expansion.

Proof idea. A shortest cross-lobe path uses exactly one bridge; the cost of crossing at singleton $\{i\}$ is $|S\triangle\{i\}|+1+|T\triangle\{i\}|$ , minimized over $i$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk
import Definitions.Def_Hirsch_cube_blend

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem cube_blend_diameter (d : ℕ) (hd : 2 ≤ d) :
    DiamLE (blendPoly d) (2 * d - 1) ∧
    ∃ u v, u ∈ Set.extremePoints ℝ (blendPoly d) ∧ v ∈ Set.extremePoints ℝ (blendPoly d) ∧
      ¬ Reach (blendPoly d) (2 * d - 2) u v := by sorry

end Hirsch

Source

Campaign research notes (2026-09-06), Prove2Me mission 'The Polynomial Hirsch Conjecture', discussion thread; independently audited on-paper proofs, note 'deep_astra_geom' Section 3.1 (audited)

View graph

The cube blend has combinatorial diameter exactly 2d−12d-12d−1

The cube blend has combinatorial diameter exactly $2d-1$