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

Disproved

Hirsch.slack_descent_to_exposed_face_convex

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

hirsch-conjecturelinear-optimizationpolytopes

Let $P\subseteq\mathbb R^D$ be a convex 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.

Correction note: this supersedes the deprecated theorem Hirsch.slack_descent_to_exposed_face (id b01e311a-c557-428c-a2e5-1296b0f3d60c), which omitted the convexity hypothesis on $P$ . Adj P u v requires the whole closed segment $[u,v]\subseteq P$ (via Mathlib's IsExtreme.subset), so without convexity a finite non-convex $P$ (e.g. two isolated points in $\mathbb R^1$ ) satisfies every other hypothesis of the deprecated statement while making part (2) vacuously false; a machine-checked Lean counterexample was built proving no term of the deprecated statement's type can exist. The source math (intrinsic_grok/attempt.md §2, "let $P$ be a polytope") always assumed convexity — only the earlier Lean transcription dropped it.

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 separate, still-open leaf
`polynomial_access_to_given_supporting_face`, and would prove the polynomial
Hirsch conjecture — do not conflate the two).

**Correction (supersedes the deprecated theorem `Hirsch.slack_descent_to_exposed_face`,
id `b01e311a-c557-428c-a2e5-1296b0f3d60c`):** the deprecated statement omitted the
hypothesis that `P` is convex. `Adj P u v` requires the whole segment `[u,v] ⊆ P`
(via `IsExtreme.subset`), so without convexity a finite non-convex `P` (e.g. two
isolated points in `ℝ¹`) satisfies every other hypothesis while making part (2)
vacuously false — a machine-checked counterexample was built proving no term of
the deprecated statement's type can exist. The source math (`intrinsic_grok/attempt.md`
§2, "let `P` be a polytope") always assumed convexity; only the Lean transcription
dropped it. This restated theorem adds `(hPconv : Convex ℝ P)` and is otherwise
unchanged.
-/

Formal statement

namespace Hirsch

theorem slack_descent_to_exposed_face_convex
    {D : ℕ} (P : Set (EuclideanSpace ℝ (Fin D)))
    (hPconv : Convex ℝ P)
    (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); correction identified and formally verified in hirsch-campaign/route1/phase5_scratch/theoremII_falsifies_counterexample.lean (2026-09-18), superseding deprecated theorem b01e311a-c557-428c-a2e5-1296b0f3d60c

View graph