The graph distance between two vertices of a bounded H-polytope is attained by a walk

Let $P=\{x\in\mathbb{R}^d:\langle a_i,x\rangle\le b_i,\ i<n\}$ be a bounded H-polytope and let $u,v$ be vertices (extreme points) of $P$. Write $\mathrm{gdist}_P(u,v)$ for the combinatorial distance in the vertex-edge graph of $P$: the least $L$ such that there is a walk of exactly $L$ steps from $u$ to $v$, each step stationary or along an edge (Reach, from the definition Hirsch_walk). Then this least length is attained:

The content is that the set of walk lengths is nonempty, i.e. that the graph of a bounded polytope is connected (Balinski; on the platform, Hirsch.face_connected or Hirsch.graph_connected_general), after which the infimum of a nonempty set of naturals is a member. This is the basic bridge between the distance function $\mathrm{gdist}$ and explicit walks, used by every layer-by-distance argument.

Formalization Note gdist is defined as sInf of the set of walk lengths and takes the junk value $0$ when no walk exists; boundedness is what rules that case out here.