Larman's dimension step: $\Delta(d+1,n)\le 2^{d-2}n-1$ from $\Delta(d,m)\le 2^{d-3}m-1$

Let $d\ge3$ and suppose that every nonempty bounded H-polytope in $\mathbb{R}^{d}$ described by $m$ inequalities has combinatorial diameter at most $2^{d-3}m-1$, for every $m$. Then every nonempty bounded H-polytope $P\subseteq\mathbb{R}^{d+1}$ described by $n$ inequalities satisfies

This is one rung of Larman's induction on the dimension. Its proof is the layer decomposition Hirsch.larman_layer_recursion with $\beta(m)=2^{d-3}m-1$ and $B_{d+1}=2^{d-2}n-1$: the facets of $P$ are $d$-dimensional, the relaxation of a facet to the $m_i$ rows active in the $i$-th layer has diameter at most $\beta(m_i)$ by hypothesis (via Hirsch.larman_layer_step), and the arithmetic condition reads $\sum_i(2^{d-3}m_i-1)+k=2^{d-3}\sum_i m_i\le 2^{d-3}\cdot2n=2^{d-2}n$. Rows with zero normal are removed first by Hirsch.diamLE_of_nonzero_rows. Together with Klee's theorem $\Delta(3,n)\le n-3$ as the base case, iterating this step gives Larman's bound $\Delta(d,n)\le2^{d-3}n$ for all $d\ge3$.

Formalization Note Subtraction is truncated natural subtraction; since $m\ge1$ for every description that has a vertex and $2^{d-3}\ge1$, the bounds $2^{d-3}m-1$ are exact. The invariant with the "$-1$" is slightly sharper than the milestone's $n\cdot2^{d-3}$ and is what the sum telescopes to; the milestone follows by padding.