A diameter bound for descriptions with nonzero normals extends to all descriptions

Fix an ambient dimension $d$ and a monotone function $\beta:\mathbb{N}\to\mathbb{N}$. Suppose that every bounded H-polytope in $\mathbb{R}^d$ described by $m$ inequalities all of whose normals are nonzero has combinatorial diameter at most $\beta(m)$, for every $m$. Then every bounded H-polytope in $\mathbb{R}^d$ described by $n$ inequalities, with no restriction on the normals, satisfies

An inequality with zero normal, $\langle 0,x\rangle\le b_j$, is either vacuous (if $b_j\ge0$) and can be deleted, or unsatisfiable (if $b_j<0$), in which case $P$ is empty and the bound holds vacuously. Deleting the vacuous rows leaves a description with $m\le n$ nonzero rows and the same polytope, and monotonicity of $\beta$ together with stationary padding of walks gives the bound $\beta(n)$. This lemma lets the geometric inductions (Larman, Kalai--Kleitman) assume that every normal is nonzero, so that every row defines a genuine supporting hyperplane.

Formalization Note DiamLE allows stationary steps, hence is monotone in the bound; the hypothesis is quantified over all row counts $m$ because deletion changes the index type from Fin n to Fin m.