Balancing H-polytopes with a diameter-transfer map

Let $P\subseteq\mathbb{R}^d$ be a nonempty bounded H-polytope cut out by $n$ linear inequalities $\langle a_i,x\rangle\le b_i$. There exist an ambient dimension

(with natural-number subtraction) and a nonempty bounded H-polytope $Q\subseteq\mathbb{R}^D$ described by exactly $2D$ inequalities, such that for every $L\in\mathbb{N}$,

In particular $D\le n+d$, and $D=\max(d,n-d)$. When $n\le 2d$ the construction pads tautological inequalities $0\cdot x\le 1$; when $n>2d$ it iterates a description-level Klee–Walkup wedge, replacing one inequality $a_1\cdot x\le b_1$ by $a_1\cdot x+t\le b_1$ and $-t\le 0$. Projection of the wedge sends vertices to vertices and edges to edges or points, so padded walks of a given length descend. The argument uses the given inequality description: redundant inequalities, lower-dimensional polytopes, and the zero-dimensional case are included.

This is formalization infrastructure for the classical wedge/$d$-step reduction, not a new diameter bound. Combined with a polynomial bound on the balanced subfamily $n=2D$, it yields the unrestricted polynomial Hirsch conjecture with the same exponent.

Formalization Note The witnesses $a_Q,b_Q$ are an explicit H-description in EuclideanSpace ℝ (Fin D). Boundedness is Bornology.IsBounded. The identity $D=d+(n-2d)$ uses Lean's truncated subtraction.