Larman's layer recursion: summing the layer steps along a facet decomposition

Let $P=\{x\in\mathbb{R}^d:\langle a_i,x\rangle\le b_i,\ i<n\}$ be a bounded H-polytope with all normals nonzero, in which every vertex has at least one tight inequality. Let $\beta:\mathbb{N}\to\mathbb{N}$ and $B_d\in\mathbb{N}$. Assume:

1. (layer step) for every base vertex $u$, row $r$, set of rows $T\ni r$, and vertices $y,z$ on the facet $F_r$ with tight rows in $T$ such that every vertex of $F_r$ carrying a row outside $T$ is strictly closer to $u$ than $y$, one has $\mathrm{gdist}(u,z)\le\mathrm{gdist}(u,y)+\beta(|T|)$ (this is Hirsch.larman_layer_step);
2. (arithmetic) for every $k$ and every family $m_1,\dots,m_k\ge1$ with $\sum_i m_i\le 2n$,

Then $\operatorname{DiamLE}(P,B_d)$: the combinatorial diameter of $P$ is at most $B_d$.

This is Larman's argument as presented by Kim--Santos. From a base vertex $u$, stratify the vertices by distance into layers $V_1,\dots,V_k$ with $V_i=\{v:\delta_{i-1}<\mathrm{gdist}(u,v)\le\delta_i\}$, $\delta_0=-1$, where $\delta_i$ is the largest distance of a vertex sharing a facet $F_i$ with some vertex at distance $\delta_{i-1}+1$. Let $T_i$ be the rows tight at some vertex of $V_i$ and $m_i=|T_i|$. Because a facet active in two layers is active in all layers between (Hirsch.tight_row_interval) and the choice of $F_{i+1}$ is maximal, no row is active in three layers, so $\sum_i m_i\le2n$. The layer step applied to $F_i$, $T_i$, a vertex $y_i\in F_i$ at distance $\delta_{i-1}+1$ and a vertex $z_i\in F_i$ at distance $\delta_i$ gives $\delta_i-\delta_{i-1}-1\le\beta(m_i)$, and summing over $i$ yields $\mathrm{ecc}(u)=\delta_k\le\sum_i\beta(m_i)+k-1\le B_d$.

Formalization Note The hypothesis that every vertex has a tight row holds automatically when $d\ge1$ (the tight normals span, Hirsch.vertex_tight_rows_span), and is stated explicitly to keep the recursion dimension-free. The layer-step hypothesis is quantified over all base vertices $u$ and all finsets $T$ of rows.