Polynomial access to a ridge-visible vertex (open)

There exist $C,k$ such that in every bounded H-polytope $P\subseteq\mathbb R^d$ with $n$ rows, from every vertex $u$ and for every nonzero row $i$ met by $P$, some vertex $y$ is reachable from $u$ by a padded walk of length $C(n+d)^k$ such that either $y$ lies on row $i$, or $y$ lies on a nonzero row $r\ne i$ that meets row $i$ inside $P$ (the face of $r$ through $y$ sees the target face across a ridge).

This is the honest inductive form of the polynomial Hirsch conjecture isolated by the campaign: by Hirsch.access_of_ridge_visible_access it implies polynomial facet access with one more factor of $d$, hence (by the platform's transfer theorem) the polynomial Hirsch conjecture; conversely it follows from the conjecture by walking to a vertex on row $i$. It is therefore equivalent to the open conjecture and is recorded so that the inductive step is separated from the dimension drop, which is a theorem. On spindles the statement is trivially true from an apex (Hirsch.spindle_apex_ridge_visible); exact computation on the polar of the Matschke--Santos--Weibel prismatoid $Q_{28}$ shows ridge-visible access at most $1$ for all vertex/facet pairs while facet access reaches $4$.

Formalization Note The reached vertex may already lie on row $i$. No condition relates $u$ to the target beyond membership.