The cube blend has an edge cut of size separating half its vertices
ProvedHirsch.cube_blend_expansiongraph-expansionhirsch-conjecturepolytopes
For , the polytope blendPoly d has a set of vertices (one of its two cube lobes) such that at most edges of the polytope leave . Hence its edge expansion is at most , exponentially small in , although the polytope is simple with only facets. (Balinski's theorem gives the matching lower bound , so the expansion is exactly .) Consequently no universal bound of the form holds for graphs of bounded H-polytopes, and unweighted expansion cannot be the mechanism behind a polynomial diameter bound.
Proof idea. Same-sign vertices are adjacent iff ; the only edges between the two signs are the bridges .
Preamble
import Mathlib import Definitions.Def_Hirsch_model import Definitions.Def_Hirsch_cube_blend open scoped RealInnerProductSpace
Formal statement
namespace Hirsch
theorem cube_blend_expansion (d : ℕ) (hd : 2 ≤ d) :
∃ W E : Finset (EuclideanSpace ℝ (Fin d)),
(∀ x ∈ W, x ∈ Set.extremePoints ℝ (blendPoly d)) ∧
W.card = 2 ^ d - 1 ∧ E.card ≤ d ∧
∀ x ∈ W, ∀ y, y ∉ W → Adj (blendPoly d) x y → y ∈ E := by sorry
end HirschSource
Campaign research notes (2026-09-06), Prove2Me mission 'The Polynomial Hirsch Conjecture', discussion thread; independently audited on-paper proofs, note 'deep_astra_geom' Sections 2.3 and 4.1 (audited; exhaustive cut check in dimension 4)