Larman's layer step: a facet relaxed to the rows of a distance layer creates no shortcuts

Let $P=\{x\in\mathbb{R}^d:\langle a_i,x\rangle\le b_i,\ i<n\}$ be a bounded H-polytope, fix a base vertex $u$ and write $\rho(\cdot)=\mathrm{gdist}_P(u,\cdot)$ for the graph distance from $u$ (definition Hirsch_walk). Let $r$ be a row with $a_r\ne0$, let $T$ be a set of rows containing $r$, and suppose (inductive hypothesis) that every bounded H-polyhedron in $\mathbb{R}^{d-1}$ described by $|T|$ inequalities has diameter at most $B$. Let $y,z$ be vertices of $P$ on the facet $F_r=\{x\in P:\langle a_r,x\rangle=b_r\}$ whose tight rows all lie in $T$, and assume the layer condition: every vertex $w$ of $P$ on $F_r$ at which some row outside $T$ is tight lies strictly closer to $u$ than $y$,

Then

This is the inductive step of Larman's proof of $\Delta(d,n)\le 2^{d-3}n$ in the form given by Kim--Santos: the facet $F_r$, relaxed to the inequalities active in the current distance layer (and bounded by one auxiliary cut, Hirsch.bounded_relaxation_cut), is a $(d-1)$-polyhedron with $|T|$ inequalities, so its vertices $y,z$ are joined by a walk of $B$ steps there. Followed backwards from $z$, that walk cannot leave $P$: as long as it stays at distance $\ge\rho(y)+1$ from $u$, every neighbour of the current vertex on $F_r$ is at distance $\ge\rho(y)$, hence has all its rows in $T$ by the layer condition, so by Hirsch.relaxation_exit_vertex the next step is an edge of $P$. Consequently the walk is a walk in $P$ and $\rho(z)\le\rho(y)+B$.

Formalization Note $T$ is a Finset (Fin n); the inductive hypothesis is stated with exactly T.card inequalities in EuclideanSpace ℝ (Fin (d-1)) and no nonemptiness hypothesis (the empty polytope satisfies every DiamLE). The direction of the walk (from $z$ towards $y$) is what makes the layer condition, which only constrains vertices closer than $y$, sufficient.