Distances from a base vertex along a facet form an interval

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 $\mathrm{gdist}_P(u,\cdot)$ for the graph distance from $u$ (definition Hirsch_walk). Let $s$ be a row index and let $p,q$ be vertices of $P$ at which the $s$-th inequality is tight. Then for every integer $t$ with

there is a vertex $w$ of $P$ with $\langle a_s,w\rangle=b_s$ and $\mathrm{gdist}_P(u,w)=t$.

So the set of distances from $u$ realised on the face cut out by a given inequality is an interval of integers. This is the "connected layer family" property of polytope graphs isolated by Eisenbrand, Hähnle, Razborov and Rothvoß, in the form in which Larman's induction uses it: a facet active in two distance layers is active in every layer in between. It follows from connectivity of the graph of each face (Hirsch.face_connected: $p$ and $q$ are joined by a walk along which the $s$-th inequality stays tight) and the fact that the distance to $u$ changes by at most one along each step of a walk.

Formalization Note The vertices are the extreme points of $P$; boundedness guarantees that all graph distances are attained by walks (Hirsch.gdist_reach).