Spindle apices are ridge-visible to every opposite facet

Proved

Hirsch.spindle_apex_ridge_visible

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

hirsch-conjecturepolytopes

Let $P\subseteq\mathbb R^d$ ( $d\ge2$ ) be a bounded spindle with apices $u,v$ : every describing row (all with nonzero normal) is tight at exactly one of $u,v$ . Let $i$ be a row tight at $v$ that defines a genuine facet (some point of $P$ has $i$ as its only tight row). Then some row $r$ tight at $u$ meets row $i$ inside $P$ : there is $x\in P$ with $\langle a_i,x\rangle=b_i$ and $\langle a_r,x\rangle=b_r$ .

In the language of the campaign's access decomposition, the apex $u$ is ridge-visible to every facet through the opposite apex, so on spindles the open 'walk to a ridge-visible vertex' step is vacuous and the whole difficulty sits in the dimension drop. Verified exactly on the polar of the Matschke--Santos--Weibel prismatoid $Q_{28}$ .

Proof idea. The facet $F_i$ is a $(d-1)$ -polytope with vertex $v$ and is not a cone with apex $v$ (a bounded polytope of positive dimension has a facet missing any given vertex), so it has a facet $F_i\cap F_r$ not containing $v$ ; then $v\notin F_r$ and the spindle condition puts $u$ on $F_r$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

theorem spindle_apex_ridge_visible (d n : ℕ) (hd : 2 ≤ d)
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hne : (Hpoly a b).Nonempty) (hbd : Bornology.IsBounded (Hpoly a b))
    (hane : ∀ i, a i ≠ 0)
    (u v : EuclideanSpace ℝ (Fin d))
    (hu : u ∈ Set.extremePoints ℝ (Hpoly a b)) (hv : v ∈ Set.extremePoints ℝ (Hpoly a b))
    (hspindle : ∀ i, (⟪a i, u⟫ = b i) ↔ ⟪a i, v⟫ ≠ b i)
    (i : Fin n) (hiv : ⟪a i, v⟫ = b i)
    (hfacet : ∃ x ∈ Hpoly a b, ⟪a i, x⟫ = b i ∧ ∀ j, ⟪a j, x⟫ = b j → j = i) :
    ∃ r : Fin n, ⟪a r, u⟫ = b r ∧ ∃ x ∈ Hpoly a b, ⟪a i, x⟫ = b i ∧ ⟪a r, x⟫ = b r := 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_grok_geom' Theorem 5.1 (audited)

View graph