Existence of a positive maximal nonnegative augmentation

Proved

HirschCircuit.exists_positive_maximal_nonnegative_step

by jjosh · Sep 8, 2026 · Mathlib c5ea003 (Lean v4.30.0)

augmentationcircuitsnonnegative-orthantpolyhedra

Let $x\in\mathbb R^n_{\ge0}$ and let $g$ be a direction that is nonnegative at every coordinate where $x$ is zero, but is negative in at least one coordinate. Then there is a strictly positive maximal step length $\alpha$ : $x+\alpha g$ remains nonnegative, at least one decreasing coordinate becomes zero, and every larger step violates nonnegativity. The step is the minimum blocking ratio over the finitely many negative coordinates of $g$ .

Preamble

import Mathlib

set_option autoImplicit false

Formal statement

namespace HirschCircuit

theorem exists_positive_maximal_nonnegative_step {n : ℕ}
    (x g : Fin n → ℝ) (hx : ∀ i, 0 ≤ x i)
    (hzero : ∀ i, x i = 0 → 0 ≤ g i)
    (hneg : ∃ i, g i < 0) :
    ∃ α : ℝ, 0 < α ∧ (∀ i, 0 ≤ x i + α * g i) ∧
      (∃ q, g q < 0 ∧ x q + α * g q = 0) ∧
      ∀ β : ℝ, α < β → ∃ i, x i + β * g i < 0 := by sorry

end HirschCircuit

Source

Elementary finite-minimum maximal-augmentation lemma used in the support-safe adaptation of Bento Natura, Circuit Diameter of Polyhedra is Strongly Polynomial, arXiv:2602.06958v2, Section 1.1 and Algorithm 1.

View graph