Walks and graph distance in the vertex-edge graph of a polytope

Vocabulary for diameter inductions on H-polytopes, extending the mission's base model Hirsch_model (which defines the H-polytope $P=\{x\in\mathbb{R}^d:\langle a_i,x\rangle\le b_i\}$, adjacency $\mathrm{Adj}(P,u,v)$, and the walk predicate $\mathrm{DiamLE}(P,B)$).

Reach P L u v — there is a walk $w_0=u,\,w_1,\dots,w_L=v$ of exactly $L$ steps in the vertex-edge graph of $P$, each step either stationary ($w_i=w_{i+1}$) or along an edge ($\mathrm{Adj}(P,w_i,w_{i+1})$). This is precisely the body of $\mathrm{DiamLE}$: by definition,

recorded as the (definitional) lemma diamLE_iff_reach. Since stationary steps are allowed, $\mathrm{Reach}$ is monotone in $L$.

gdist P u v — the combinatorial (graph) distance from $u$ to $v$ in the vertex-edge graph of $P$: the least $L$ with $\mathrm{Reach}(P,L,u,v)$, and the junk value $0$ when no walk exists (Lean's sInf of an empty set of naturals).

These are the objects every layer-by-distance argument on polytope graphs (Barnette–Larman, Kalai–Kleitman) manipulates: distance layers from a base vertex, monotonicity and concatenation of walks, and distance comparison between a polytope and its relaxations. Publishing them as a shared definition lets such lemmas be stated on the platform without each proof re-minting a private Reach.

Formalization Note Reach and gdist are defined for an arbitrary real vector space $E$ and set $P\subseteq E$, exactly as Adj and DiamLE are in Hirsch_model. gdist is noncomputable. The only lemmas included are the definitional unfolding diamLE_iff_reach and the trivial reach_zero.