The second-best vertex for a linear objective is adjacent to the best vertex (corrected)

Proved

Hirsch.second_best_vertex_adjacent_v2

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

hirsch-conjecturelinear-optimizationpolytopes

Let $a:\{1,\dots,n\}\to\mathbb R^d$ , $b:\{1,\dots,n\}\to\mathbb R$ describe the H-polytope $P=\mathrm{Hpoly}(a,b)$ , $v\in P$ , and $c$ a linear functional strictly and uniquely maximized on $P$ at $v$ . If $u$ is an extreme point of $P$ other than $v$ attaining the largest value of $c$ among all extreme points other than $v$ , then $u$ is adjacent to $v$ .

This is the elementary linear-programming fact that the second-best vertex for a linear objective is always adjacent to the best one — a standard consequence of the structure of the vertex-edge graph of a polytope.

Correction note: this supersedes Hirsch.second_best_vertex_adjacent (id 0c8577ca-5544-4bcb-9557-09f6f9710f77), now deprecated after an independent audit found its hypotheses did not require $v\in P$ : a point $v$ strictly outside $P$ that dominates every point of $P$ in the $c$ direction satisfied every other hypothesis while making the adjacency conclusion trivially false, since adjacency requires the connecting segment to lie in $P$ . This restatement adds the missing membership hypothesis $v\in P$ .

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

/-!
# Second-best-vertex lemma (corrected)

Source: `hirsch-campaign/route1/shortcut_astra/attempt.md` 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`."

**Correction, superseding `Hirsch.second_best_vertex_adjacent`
(id `0c8577ca-5544-4bcb-9557-09f6f9710f77`, deprecated):** an independent
audit (audit_sonnet, 2026-09-20) found the published statement's hypothesis
`hc` (the unpacked body of `Hirsch.IsUniqueBoundedMaximizer a b v`, which
itself has the same gap) never required `v ∈ Hpoly a b`. Witness: `d = 1`,
`Hpoly a b = {0}`, `c = v = e1` (a point strictly outside the polytope,
dominating its unique point `0` in the `c` direction), `u = 0` (the polytope's
unique extreme point). Every hypothesis of the deprecated statement holds, but
`Adj (Hpoly a b) v u` forces `segment ℝ v u ⊆ Hpoly a b`, which fails since the
endpoint `v = e1 ∉ Hpoly a b`. A machine-checked Lean proof of this negation
was built (`route1/audit_sonnet/second_best_vertex_adjacent_counterexample.lean`).

The fix adds the missing `hv : v ∈ Hpoly a b`, matching the source's actual
"objective uniquely maximized at a vertex `v`" (a vertex of the polyhedron,
not an arbitrary point of the ambient space). `Hirsch.IsUniqueBoundedMaximizer`
(`Definitions/Def_Hirsch_simple_vertex.lean`) has the identical gap and should
be treated as unreliable until independently corrected; this restatement does
not reuse it, stating `v`'s maximizing hypothesis directly with the added
membership conjunct instead.
-/

open scoped RealInnerProductSpace

Formal statement

namespace Hirsch

/-- If `v ∈ Hpoly a b` and `c` uniquely maximizes on `Hpoly a b` at `v`, 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_v2
    {d n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (v c : EuclideanSpace ℝ (Fin d)) (hv : v ∈ Hpoly a b)
    (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/shortcut_astra/attempt.md Lemma 6; correction after independent audit finding audit_sonnet/second_best_vertex_adjacent_counterexample.lean (2026-09-20), superseding deprecated theorem 0c8577ca-5544-4bcb-9557-09f6f9710f77

View graph