Recursive positive projective product certificates give the Hirsch row-excess bound

Let $P$ be described by $n$ real linear inequalities in $\mathbb R^d$. Suppose it has a finite recursive geometric certificate built from the following operations. A leaf is a bounded H-polyhedron with at most three excess describing rows. An affine step transports a certificate through an affine equivalence without changing the dimension or number of rows. At a split, an invertible linear coordinate map and a partition of all rows identify a source with a Cartesian product of at least two positive-dimensional certified factors. Each factor's row count is at least its dimension. A positive projective map $x\mapsto x/(1+c\cdot x)$ then sends this source onto the parent with sheared rows $a_i+b_i c$; both forward and inverse denominators are required positive on their full feasible sets. Different nodes may use different charts.

Then the ordinary-edge graph diameter of $P$ is at most $n-d$. Product costs add and chart/affine transport preserves them, so the sum of leaf excesses is exactly the parent excess. There is no restriction on total excess or tree depth beyond the existence of the finite certificate.

This is a sufficient criterion. It does not assert that arbitrary polytopes admit such trees, or that chart discovery is efficient. The separate exact rational search is not part of this Lean theorem. Natural subtraction and stationary walk steps follow the Hirsch model's padded diameter convention.