A $d$-spindle has at least $2d$ inequalities

A spindle in dimension $d$ cannot be described by fewer than $2d$ inequalities.

Let $P\subseteq\mathbb R^d$ be an H-polytope cut out by $n$ inequalities, and let $u,v$ be extreme points of $P$ such that every describing inequality is tight at exactly one of $u$ or $v$. If $d>0$, then

The two tight sets are disjoint by the spindle (XOR) hypothesis. Each extreme point of a $d$-dimensional polytope is the unique solution of at least $d$ linearly independent tight inequalities (otherwise a line through the point would remain in $P$), so each tight set has cardinality at least $d$.

This is the observation that the asimpliciality $s=n-2d$ of a spindle is nonnegative, used as the induction parameter in Santos' strong $d$-step theorem.

Formalization Note. The H-polytope may include redundant inequalities; the bound counts all describing inequalities, so it remains valid in the presence of redundancy.