Common-face diameter transfers from coordinate H-polytopes

Proved

Hirsch.common_face_diamLE_of_coord_diamLE

by jjosh · Sep 11, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-geometrygraph-diameterhirsch-conjecturepolytopes

Graph diameter of a common face equals the graph diameter of its canonical coordinate H-polytope.

If the coordinate presentation in the common-direction space has $\operatorname{DiamLE}(Q,B)$ , then the common face $F$ in the original ambient space has $\operatorname{DiamLE}(F,B)$ . The coordinate map $q\mapsto u+Lq$ is an injective affine isometry onto $F$ and sends extreme segments to extreme segments. This transfers any budget, including a hypothetical uniform polynomial, from an $h$ -dimensional H-polytope onto the face. It does not itself produce a polynomial bound.

Formalization Note No boundedness or dimension hypothesis is required beyond the coordinate DiamLE assumption.

Preamble

import Definitions.Def_Hirsch_common_face_geometry

set_option autoImplicit false
open scoped RealInnerProductSpace
open Hirsch

Formal statement

namespace Hirsch

theorem common_face_diamLE_of_coord_diamLE
    {d n B : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (u x : EuclideanSpace ℝ (Fin d))
    (hcoord : DiamLE
      (Hpoly (HirschCommonFace.commonFaceA a b u x)
        (HirschCommonFace.commonFaceB a b u x)) B) :
    DiamLE (HirschCommonFace.commonFace a b u x) B := by sorry

end Hirsch

Source

Affine transport of extreme segments along the public common-face coordinate isometry. Helper for Hirsch.common_face_diameter_of_dim_ge_six: a uniform polynomial on h-dimensional H-polytopes would transfer to the face.

View graph