A common-tight-facet walk of length n-d between any two vertices of the cyclic polar

Proved

Hirsch.cyclic_polar_face_preserving_walk

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

cyclic-polytopeshirsch-conjecturepolytopes

For $n>d\ge1$ and any two extreme points $u,v$ of $\mathrm{cyclicPolar}(n,d)$ , there is a padded walk $w:\{0,\dots,n-d\}\to\mathbb R^d$ from $u$ to $v$ of exactly $n-d$ steps such that every facet normal tight at both $u$ and $v$ remains tight along the entire walk.

This is the "common-cut domino route": besides witnessing the diameter bound of cyclic_polar_hirsch, the walk never leaves any facet shared by the two endpoints, a stronger structural property than mere reachability.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
import Definitions.Def_Hirsch_cyclic_polar

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem cyclic_polar_face_preserving_walk (n d : ℕ) (hd : 1 ≤ d) (hn : d < n)
    (u v : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ Set.extremePoints ℝ (cyclicPolar n d))
    (hv : v ∈ Set.extremePoints ℝ (cyclicPolar n d)) :
    ∃ w : ℕ → EuclideanSpace ℝ (Fin d), w 0 = u ∧ w (n - d) = v ∧
      (∀ j < n - d, w j = w (j + 1) ∨ Adj (cyclicPolar n d) (w j) (w (j + 1))) ∧
      ∀ i : Fin n, ⟪cyclicPolarA n d i, u⟫ = 1 → ⟪cyclicPolarA n d i, v⟫ = 1 →
        ∀ j ≤ n - d, ⟪cyclicPolarA n d i, w j⟫ = 1 := 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) (Lemmas 3-4 of attempt_thin.md, the common-cut domino route; referee_thin.md confirms SOUND)

View graph