A second-best vertex under a uniquely-maximized bounded objective is adjacent to the optimum

Open

Hirsch.second_best_vertex_adjacent

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

hirsch-conjecturelinear-optimizationpolytopes

Let $c$ uniquely maximize a linear functional on $\mathrm{Hpoly}(a,b)$ at $v$ (i.e. $\langle c,x\rangle<\langle c,v\rangle$ for every other point $x$ of the polyhedron, which forces both boundedness above and uniqueness of the maximizer). If $u\ne v$ is an extreme point attaining the largest $c$ -value among all extreme points other than $v$ , then $u$ is adjacent to $v$ in the polyhedron's vertex-edge graph.

This is a completely self-contained, general, elementary LP fact — essentially the statement underlying simplex-method correctness (a non-optimal vertex always has an improving adjacent edge, and by the uniqueness/boundedness of the true optimum that improving neighbor must be the optimum itself when $u$ is already second-best). No polytope-gluing, cap, or Black–Xue structure is used.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

/-!
# Second-best-vertex lemma

Source: `hirsch-campaign/route1/shortcut_astra/attempt.md` Lemma 6, exactly quoted
in the flagship triage report (`route1/flagship_triage_report.md`, Part A1
companion sub-lemma): "For a pointed polyhedron and an objective uniquely
maximized at a vertex `v`, the largest objective value among other finite
vertices is attained at a finite neighbor of `v`." Flagged there as "a completely
self-contained, general, elementary LP fact with no polytope-gluing context at
all" and recommended `PUBLISH-AS-THEOREM-STATEMENT` + `ATTEMPT-LEAN-PROOF-NOW`.

**Frame audit.** The source's standing hypothesis "an objective uniquely
maximized at a vertex `v`, bounded above" is exactly the pair `(c, hc)` below:
`hc` is definitionally the body of `Hirsch.IsUniqueBoundedMaximizer a b v`
(`Definitions/Def_Hirsch_simple_vertex.lean`) with its witness `c` made
explicit, since the conclusion needs the *same* `c` compared across several
vertices (`u`, `u'`) — a bare `∃ c, ...` existential would not let the
statement fix one functional throughout. No new definition is introduced; `c`
and `hc` are literally what `IsUniqueBoundedMaximizer a b v` asserts to exist.
The conclusion "the largest objective value among other finite vertices is
attained at a finite neighbor" is stated conditionally on `u` actually being
such a maximizer (`hbest`), rather than presupposing one exists — this is a
strengthening of scope, not a restriction: it makes the statement true and
general even when the supremum over other vertices is not attained (e.g.
infinitely many vertices), whereas the source's finite-vertex setting always
has one. Nothing about polyhedron gluing, caps, or Black–Xue structure is
used or assumed; `a`, `b` are an arbitrary H-presentation.
-/

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

/-- If `c` uniquely maximizes on `Hpoly a b` at `v` (bounded above, as in
`IsUniqueBoundedMaximizer`), and `u` is a vertex other than `v` attaining the
largest `c`-value among all vertices other than `v`, then `u` is adjacent to
`v`. -/
theorem second_best_vertex_adjacent
    {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v c : EuclideanSpace ℝ (Fin d))
    (hc : ∀ x ∈ Hpoly a b, x ≠ v → ⟪c, x⟫ < ⟪c, v⟫)
    (u : EuclideanSpace ℝ (Fin d)) (hu : u ∈ Set.extremePoints ℝ (Hpoly a b))
    (huv : u ≠ v)
    (hbest : ∀ u' ∈ Set.extremePoints ℝ (Hpoly a b), u' ≠ v → ⟪c, u'⟫ ≤ ⟪c, u⟫) :
    Adj (Hpoly a b) v u := by sorry

end Hirsch

Source

hirsch-campaign/route1/flagship_triage_report.md, Part A1/A2/A3; hirsch-campaign/route1/shortcut_astra/attempt.md §5, Lemma 6 ("For a pointed polyhedron and an objective uniquely maximized at a vertex v, the largest objective value among other finite vertices is attained at a finite neighbor of v")

View graph