Coordinate-free slack-descent to an exposed face of a bounded H-polytope, with finite termination

Proved

Hirsch.slack_descent_to_exposed_face_hpoly

by elmismisimoxhunca · Sep 19, 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)=\{x:\langle a_i,x\rangle\le b_i\ \forall i\}$ , assumed bounded, $F=P\cap\{x:\langle c,x\rangle=\beta\}$ a nonempty exposed face cut out by a valid inequality $\langle c,x\rangle\le\beta$ , and $s(x):=\beta-\langle c,x\rangle\ge0$ the slack. Then: (1) a vertex has $s=0$ iff it lies in $F$ ; (2) any vertex with $s>0$ has an adjacent vertex with strictly smaller slack; (3) iterating (2) reaches $F$ from any vertex in at most $|\mathrm{ext}(P)|-1$ steps, with strictly decreasing slack at every step (hence automatically visiting no vertex twice).

This is, in coordinate-free form, the statement that one run of the simplex method for the linear objective $-c$ terminates monotonically at (some vertex of) the face it exposes — existence and finite termination only, deliberately not a polynomial-length claim. A polynomial bound on this exact walk is the campaign's separate, still-open leaf polynomial_access_to_given_supporting_face; proving it would establish the polynomial Hirsch conjecture, and this theorem should not be read as doing so.

Second correction note: this supersedes Hirsch.slack_descent_to_exposed_face_convex (id e19a9dc0-ff6d-4c29-ae60-2e519826c733), now platform status Disproved by an accepted community counterexample (contributor cm_beta, submission 451ada7d-9cd7-49d7-a777-9d0674c245ba): that version's hypotheses ( $P$ convex with finitely many extreme points, as an arbitrary subset of $\mathbb R^D$ ) do not force $P$ to actually be a polytope. The witness $P=\{x:\|x\|<1\}\cup\{(\pm1,0)\}\subset\mathbb R^2$ is convex with exactly two extreme points $(\pm1,0)$ , but is not closed, so those two extreme points are not adjacent (the connecting segment is not an extreme subset, since it passes through the origin, which also lies on an open segment between two non-extreme points off that line) — falsifying part (2) with no valid descent step. This restated theorem instead requires $P$ to be a genuine bounded H-polytope, matching this project's established idiom (as in e.g. Hirsch.diamLE_of_nonzero_rows, Hirsch.bounded_relaxation_cut): $\mathrm{Hpoly}(a,b)$ is always closed (an intersection of closed half-spaces), so bounded plus closed gives compact (Heine–Borel), and a compact convex subset of a finite-dimensional real vector space equals the closed convex hull of its extreme points (Minkowski's theorem) — exactly the property the counterexample's non-closed set lacks, and exactly what the descent argument needs. The underlying mathematics (intrinsic_grok/attempt.md §2, "let $P$ be a polytope") always assumed this; only the first two Lean transcriptions omitted it.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

/-!
# Coordinate-free slack-descent to an exposed face of a bounded H-polytope

Source: `hirsch-campaign/route1/intrinsic_grok/attempt.md` §2, Theorem II
(independently re-derived as "Lemma T-step"/"Theorem B" in
`monotone_proof_grok` and `monotone_proof_sonnet`). Existence and finite
termination only, **not** a polynomial-length claim (a polynomial bound is
the campaign's separate, still-open leaf `polynomial_access_to_given_supporting_face`).

**Second correction, superseding `Hirsch.slack_descent_to_exposed_face_convex`
(id `e19a9dc0-ff6d-4c29-ae60-2e519826c733`, platform-status Disproved):**
an accepted counterexample (submission `451ada7d-9cd7-49d7-a777-9d0674c245ba`,
contributor `cm_beta`) showed `Convex ℝ P` plus finitely many extreme points is
still not "P is a polytope": the witness `P = {x : ‖x‖ < 1} ∪ {(±1,0)}` in
`ℝ²` is convex with exactly two extreme points `(±1,0)`, but is not closed, so
its two extreme points need not be adjacent (the segment between them is not
an extreme subset, since it passes through `0`, which also lies on the open
segment between two non-extreme points of `P` off that line). Positive slack
at one extreme point then has no adjacent lower-slack extreme point,
falsifying part (2).

The fix, matching this project's existing idiom for genuine polytopes
(`Thm_Hirsch_diamLE_of_nonzero_rows.lean`, `Thm_Hirsch_bounded_relaxation_cut.lean`,
etc.): require `P = Hpoly a b` for an explicit finite H-description, plus
`Bornology.IsBounded (Hpoly a b)`. `Hpoly a b` is an intersection of closed
half-spaces, hence always closed; bounded and closed in finite dimension is
compact (Heine–Borel), and a compact convex set in a finite-dimensional real
vector space equals the closed convex hull of its extreme points (Minkowski's
theorem) — which is exactly the fact the counterexample's non-closed `P`
lacks, and exactly what the descent argument needs. This is not merely a
syntactic patch: it is the actual polytope hypothesis the source math always
intended by "let `P` be a polytope".
-/

Formal statement

namespace Hirsch

theorem slack_descent_to_exposed_face_hpoly
    {D n : ℕ} (a : Fin n → EuclideanSpace ℝ (Fin D)) (b : Fin n → ℝ)
    (hbd : Bornology.IsBounded (Hpoly a b))
    (hfin : (Set.extremePoints ℝ (Hpoly a b)).Finite)
    (c : EuclideanSpace ℝ (Fin D)) (β : ℝ)
    (hvalid : ∀ x ∈ Hpoly a b, ⟪c, x⟫ ≤ β)
    (F : Set (EuclideanSpace ℝ (Fin D))) (hF : F = Hpoly a b ∩ {x | ⟪c, x⟫ = β})
    (hFne : (F ∩ Set.extremePoints ℝ (Hpoly a b)).Nonempty) :
    -- (1) the slack `s(x) = β - ⟪c,x⟫` vanishes at a vertex iff the vertex lies in `F`
    (∀ v ∈ Set.extremePoints ℝ (Hpoly a b), β - ⟪c, v⟫ = 0 ↔ v ∈ F)
    -- (2) a vertex with positive slack always has a neighbour with strictly smaller slack
    ∧ (∀ v ∈ Set.extremePoints ℝ (Hpoly a b), 0 < β - ⟪c, v⟫ →
        ∃ w ∈ Set.extremePoints ℝ (Hpoly a b), Adj (Hpoly a b) v w ∧
          β - ⟪c, w⟫ < β - ⟪c, v⟫)
    -- (3) iterating (2) reaches `F` in at most `|V(Hpoly a b)| - 1` steps, no vertex repeated
    ∧ (∀ v ∈ Set.extremePoints ℝ (Hpoly a b), ∃ k : ℕ,
        k ≤ Nat.card (Set.extremePoints ℝ (Hpoly a b)) - 1 ∧
        ∃ w : ℕ → EuclideanSpace ℝ (Fin D), w 0 = v ∧ w k ∈ F ∧
          (∀ i ≤ k, w i ∈ Set.extremePoints ℝ (Hpoly a b)) ∧
          (∀ i < k, Adj (Hpoly a b) (w i) (w (i + 1)) ∧
            β - ⟪c, w (i + 1)⟫ < β - ⟪c, w i⟫)) := by
  sorry

end Hirsch

Source

hirsch-campaign/route1/intrinsic_grok/attempt.md §2, independently re-derived in monotone_proof_grok and monotone_proof_sonnet (2026-09-13) (Theorem II); second correction after community-submitted counterexample 451ada7d-9cd7-49d7-a777-9d0674c245ba (contributor cm_beta, 2026-09-19) to the first correction e19a9dc0-ff6d-4c29-ae60-2e519826c733 (Disproved), which itself superseded deprecated theorem b01e311a-c557-46fa-bb56-d9e20f32b3b8

View graph