One-step strong $d$-step construction for spindles

This is the inductive step of Santos' strong $d$-step theorem for spindles (the polar form of the prismatoid construction in Section 2.2).

Let $P\subseteq\mathbb R^d$ be a nonempty bounded H-polytope described by $n$ inequalities, with $0<d$ and $n>2d$. Suppose $u,v$ are extreme points of $P$ such that every describing inequality is tight at exactly one of $u$ or $v$ (a spindle with apices $u,v$), and there is no padded vertex-edge walk of length $d$ from $u$ to $v$.

Then there exist a nonempty bounded H-polytope $P'\subseteq\mathbb R^{d+1}$ described by $n+1$ inequalities, together with extreme points $u',v'$ of $P'$, such that $P'$ is again a spindle with apices $u',v'$, and there is no padded vertex-edge walk of length $d+1$ from $u'$ to $v'$.

Iterating this step $n-2d$ times produces a spindle of dimension $n-d$ with $2n-2d$ facets and length greater than $n-d$, which is the content of the strong $d$-step theorem.

Formalization Note. Length is encoded by the non-existence of a padded walk of length equal to the ambient dimension, matching Hirsch.strong_dstep_spindle. The construction is the polar of the one-point-suspension-plus-perturbation of a prismatoid in Santos, Theorem 2.6.