Simple vertices, simple polyhedra, and normal-cone-interior vocabulary

Definition

Hirsch_simple_vertex

by elmismisimoxhunca · Sep 19, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convex-geometryhirsch-conjecturepolytopes

For an H-presentation $(a,b)$ of a polyhedron $\mathrm{Hpoly}(a,b)\subseteq\mathbb R^d$ , $\mathrm{TightSet}(a,b,v)=\{i:\langle a_i,v\rangle=b_i\}$ is the set of row indices tight at $v$ . A point $v$ is a simple vertex ( $\mathrm{IsSimpleVertex}$ ) if it is an extreme point of $\mathrm{Hpoly}(a,b)$ with $|\mathrm{TightSet}(a,b,v)|=d$ exactly (no degeneracy); $\mathrm{Hpoly}(a,b)$ is a simple polyhedron ( $\mathrm{IsSimplePolyhedron}$ ) if every extreme point is simple. $v$ is the unique maximizer of a linear functional bounded above ( $\mathrm{IsUniqueBoundedMaximizer}$ ) if some $c$ satisfies $\langle c,x\rangle<\langle c,v\rangle$ strictly for every other $x$ in the polyhedron (this single strict inequality is equivalent to "bounded above and uniquely maximized at $v$ "). Finally $y$ is a strictly positive combination of exactly the rows tight at $v$ ( $\mathrm{IsPositiveCombinationOfTightRows}$ ) if $y=\sum_i\lambda_i a_i$ with every $\lambda_i>0$ on a tight row and $\lambda_i=0$ off it; when $v$ is simple this set coincides exactly with the topological interior of $v$ 's normal cone.

This vocabulary supplies the hypothesis structure for the flagship covering-diameter effort's two top-priority general (Black–Xue-independent) results: the cap-gluing composition lemma (cap_gluing_diameter_composition) and the simple-polytope rank/co-rank distance lower bound (simple_vertex_adjacent_tight_inter_card, simple_polyhedron_target_distance_lower_bound).

Formalization Note Boundedness/full-dimensionality of the polyhedron are deliberately not baked into these definitions (matching this workspace's Hpoly convention); theorems using them supply such hypotheses explicitly where the proof needs them. $\mathrm{IsPositiveCombinationOfTightRows}$ avoids invoking a generic topological-interior operator so that the equivalence to "interior of the normal cone" (which needs $v$ simple) is an explicit fact invoked at the point of use, not a hidden assumption.

Definition code

import Mathlib
import Definitions.Def_Hirsch_model

/-!
# Simple vertices, simple polyhedra, and normal-cone interiors

Vocabulary for the flagship covering-diameter effort's general (Black–Xue-independent)
convex-polytope lemmas: A1 (cap-gluing composition/diameter lemma) and A3 (simple-polytope
rank/co-rank distance lower bound) of
`hirsch-campaign/route1/flagship_triage_report.md`.

Source for the exact meaning of "simple": `route1/shortcut_astra/attempt.md` §2
("`v` its simple top") together with the A1 synthesis in the triage report
("vertex `v` such that `v` is tight on exactly `D` facets ('simple')") and
`route1/flagship_actual_distance/attempt.md` §3.1 ("In a **simple** local model
`e=0` everywhere", i.e. every vertex has exactly `D` tight facets, no more).
"Simple" is a per-vertex notion (`IsSimpleVertex`); "simple polyhedron" (`IsSimplePolyhedron`)
requires it at every vertex, as used globally in `flagship_actual_distance` §3.1 and
`flagship_simple_general` §3.

Source for "unique maximizer of a linear functional bounded above": triage report
Part A1 hypothesis (0) and `shortcut_astra/attempt.md` Lemma 6 ("an objective uniquely
maximized at a vertex `v`").

Source for "interior of the normal cone": `shortcut_astra/attempt.md` §2 condition (1)
("every cap normal lies in `int N_P(v)`"). Since a simple vertex's tight rows are exactly
`d` in number and (for a vertex) linearly independent, the normal cone they generate is a
full-dimensional simplicial cone, whose interior is *exactly* the set of strictly positive
combinations of those `d` generators — this is the standard fact used (without further
comment) throughout `shortcut_astra`/`shortcut_sol`/`flagship_decomposition`. We encode
this directly as `IsPositiveCombinationOfTightRows` rather than invoking a generic
topological-interior operator, so the definition does not silently assume the generators
are independent; callers supply `IsSimpleVertex` separately where that equivalence is used.
-/

open scoped RealInnerProductSpace

namespace Hirsch

/-- The set of row indices of the H-presentation `(a, b)` tight (active) at `v`:
`{i | ⟪a i, v⟫ = b i}`. -/
def TightSet {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v : EuclideanSpace ℝ (Fin d)) : Set (Fin n) :=
  {i | ⟪a i, v⟫ = b i}

/-- `v` is a **simple vertex** of `Hpoly a b`: it is an extreme point of the polyhedron and
exactly `d` of the `n` facet inequalities are tight there (no degeneracy). Matches the
triage report's synthesized A1 hypothesis "`v` tight on exactly `D` facets ('simple')" and
`flagship_actual_distance`'s "simple local model" (`e(v) = 0`). -/
def IsSimpleVertex {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v : EuclideanSpace ℝ (Fin d)) : Prop :=
  v ∈ Set.extremePoints ℝ (Hpoly a b) ∧ (TightSet a b v).ncard = d

/-- `Hpoly a b` is a **simple polyhedron**: every extreme point is a simple vertex.
Matches the global "simple local model, `e = 0` everywhere" hypothesis of
`flagship_actual_distance` §3.1 and the "simple polytope" hypothesis of
`flagship_simple_general` §3, used for A3's rank/co-rank distance lower bound. -/
def IsSimplePolyhedron {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ) :
    Prop :=
  ∀ v ∈ Set.extremePoints ℝ (Hpoly a b), IsSimpleVertex a b v

/-- `v` is the **unique maximizer of a linear functional bounded above** on `Hpoly a b`:
there is a direction `c` such that every other point of the polyhedron has strictly
smaller `c`-value than `v`. (Boundedness above of `⟪c, ·⟫` on the polyhedron, and
uniqueness of the maximizer, both follow immediately from this single strict inequality;
this is the standard unpacking, not a weakening.) Matches the triage report's A1
hypothesis (0) and the objective hypothesis of `shortcut_astra` Lemma 6. -/
def IsUniqueBoundedMaximizer {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v : EuclideanSpace ℝ (Fin d)) : Prop :=
  ∃ c : EuclideanSpace ℝ (Fin d), ∀ x ∈ Hpoly a b, x ≠ v → ⟪c, x⟫ < ⟪c, v⟫

/-- `y` is a **strictly positive combination of exactly the rows of `(a, b)` tight at `v`**:
every coefficient on a tight row is strictly positive and every coefficient on a non-tight
row is zero. When `v` is a simple vertex (so its `d` tight rows are linearly independent
and span `ℝ^d`), this set is exactly the topological interior of the normal cone of
`Hpoly a b` at `v` — the notion used, without further formalization, in
`shortcut_astra/attempt.md` §2 condition (1) ("every cap normal lies in `int N_P(v)`"). -/
def IsPositiveCombinationOfTightRows {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d))
    (b : Fin n → ℝ) (v y : EuclideanSpace ℝ (Fin d)) : Prop :=
  ∃ lam : Fin n → ℝ, (∀ i, i ∈ TightSet a b v → 0 < lam i) ∧
    (∀ i, i ∉ TightSet a b v → lam i = 0) ∧ y = ∑ i, lam i • a i

end Hirsch

Source

hirsch-campaign/route1/flagship_triage_report.md, Part A1/A2/A3; hirsch-campaign/route1/shortcut_astra/attempt.md §2, Lemma 6; hirsch-campaign/route1/flagship_actual_distance/attempt.md §3.1

View graph