The cyclic polar's diameter is exactly n-d in the balanced range d<n<=2d

Proved

Hirsch.cyclic_polar_diameter_balanced

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

cyclic-polytopeshirsch-conjecturepolytopes

For $n,d$ with $1\le d$ , $d<n\le2d$ (the balanced range), some pair of extreme points $u,v$ of $\mathrm{cyclicPolar}(n,d)$ is not reachable by any padded walk of length $n-d-1$ : the diameter bound of cyclic_polar_hirsch is tight, and the true diameter is exactly $n-d$ , in this range.

The range hypothesis $n\le2d$ is load-bearing: the underlying two-disjoint-block lower-bound argument needs both blocks nonempty, which requires $n\le2d$ ; outside this range only the upper bound of cyclic_polar_hirsch is currently established, and this theorem does not claim more.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_walk
import Definitions.Def_Hirsch_cyclic_polar

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem cyclic_polar_diameter_balanced (n d : ℕ) (hd : 1 ≤ d) (hn : d < n) (hn2 : n ≤ 2 * d) :
    ∃ u v, u ∈ Set.extremePoints ℝ (cyclicPolar n d) ∧ v ∈ Set.extremePoints ℝ (cyclicPolar n d) ∧
      ¬ Reach (cyclicPolar n d) (n - d - 1) u v := by sorry

end Hirsch

Source

Campaign research notes (2026-09-13/17), Prove2Me mission 'The Polynomial Hirsch Conjecture'; plans/attempt_thin.md + plans/referee_thin.md (cyclic-polar family, referee-verified SOUND); plans/attempt_flag.md + plans/referee_flag.md (flag/stellar subdivision, referee-verified SOUND) (Lemma 7 of attempt_thin.md, two-disjoint-block lower bound, exactly for d<n<=2d; referee_thin.md confirms SOUND for this range)

View graph