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

Open

Hirsch.slack_descent_to_exposed_face

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

hirsch-conjecturelinear-optimizationpolytopes

Let $P\subseteq\mathbb R^D$ be a polytope (finitely many extreme points), $F=P\cap\{x:\langle n,x\rangle=\beta\}$ a nonempty exposed face cut out by a valid inequality $\langle n,x\rangle\le\beta$ , and $s(x):=\beta-\langle n,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 $-n$ 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.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model

open scoped RealInnerProductSpace

/-!
# Coordinate-free slack-descent to an exposed face (Black–Xue campaign "Theorem II")

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`, no gaps found in any of the
three derivations). This is one run of the simplex method for the linear
objective `-n` on the exposing inequality of a face `F`: existence and finite
termination only, **not** a polynomial-length claim (a polynomial bound on
this exact walk is the campaign's still-open leaf
`polynomial_access_to_given_supporting_face`, and would prove the polynomial
Hirsch conjecture — do not conflate the two).
-/

Formal statement

namespace Hirsch

theorem slack_descent_to_exposed_face
    {D : ℕ} (P : Set (EuclideanSpace ℝ (Fin D)))
    (hPfin : (Set.extremePoints ℝ P).Finite)
    (n : EuclideanSpace ℝ (Fin D)) (β : ℝ)
    (hvalid : ∀ x ∈ P, ⟪n, x⟫ ≤ β)
    (F : Set (EuclideanSpace ℝ (Fin D))) (hF : F = P ∩ {x | ⟪n, x⟫ = β})
    (hFne : (F ∩ Set.extremePoints ℝ P).Nonempty) :
    -- (1) the slack `s(x) = β - ⟪n,x⟫` vanishes at a vertex iff the vertex lies in `F`
    (∀ v ∈ Set.extremePoints ℝ P, β - ⟪n, v⟫ = 0 ↔ v ∈ F)
    -- (2) a vertex with positive slack always has a neighbour with strictly smaller slack
    ∧ (∀ v ∈ Set.extremePoints ℝ P, 0 < β - ⟪n, v⟫ →
        ∃ w ∈ Set.extremePoints ℝ P, Adj P v w ∧ β - ⟪n, w⟫ < β - ⟪n, v⟫)
    -- (3) iterating (2) reaches `F` in at most `|V(P)| - 1` steps, with no vertex repeated
    ∧ (∀ v ∈ Set.extremePoints ℝ P, ∃ k : ℕ, k ≤ Nat.card (Set.extremePoints ℝ P) - 1 ∧
        ∃ w : ℕ → EuclideanSpace ℝ (Fin D), w 0 = v ∧ w k ∈ F ∧
          (∀ i ≤ k, w i ∈ Set.extremePoints ℝ P) ∧
          (∀ i < k, Adj P (w i) (w (i + 1)) ∧ β - ⟪n, w (i + 1)⟫ < β - ⟪n, 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; re-derived independently three times with no gaps found across all three derivations)

View graph