The full common-face presentation is a subpresentation of size n

Proved

Hirsch.common_face_has_full_subpresentation

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

convex-geometryhirsch-conjecturepolytopes

The full common-face coordinate presentation is always a subpresentation of itself, so the admissible row-budget set is nonempty.

This is the trivial witness $M=n$ for CommonFaceHasSubpresentationAtMost. It does not identify the least equivalent row count with the number of geometric facets; that genuine-facet bridge remains open.

Formalization Note The embedding is the identity on Fin n.

Preamble

import Definitions.Def_Hirsch_common_face_geometry

set_option autoImplicit false
open scoped RealInnerProductSpace
open Hirsch

Formal statement

namespace Hirsch

theorem common_face_has_full_subpresentation
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (u x : EuclideanSpace ℝ (Fin d)) :
    HirschCommonFace.CommonFaceHasSubpresentationAtMost a b u x n := by sorry

end Hirsch

Source

Immediate from the definition of HasSubpresentationAtMost; first public existence witness for the least-row-count program on common-face coordinates.

View graph