Polynomial edge refinement of irredundant circuit walks — open research

Open

Hirsch.polynomial_edge_refinement_of_circuit_walks

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

convex-geometrypolytopes

For irredundant strictly feasible bounded H-polytope presentations, is there a uniform polynomial C(n+d)^k such that any length-L padded maximal circuit walk between vertices can be replaced by a graph-edge walk between the same vertices of length C(n+d)^k L? The replacement need not visit the original circuit intermediates, which can be nonvertices. It need not be monotone or preserve every already visited facet. This is an OPEN CONJECTURAL bridge, not a theorem of Natura and not a routine rounding lemma. Together with the circuit bound it retains the essential polynomial-Hirsch difficulty.

Preamble

import Definitions.Def_Hirsch_circuit_model
set_option autoImplicit false
open scoped RealInnerProductSpace
open Hirsch

Formal statement

theorem Hirsch.polynomial_edge_refinement_of_circuit_walks :
∃ C k : ℕ, ∀ (d n : ℕ)
      (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      Bornology.IsBounded (Hirsch.Hpoly a b) →
      Hirsch.RowPresentationIrredundant a b → Hirsch.StrictlyFeasibleRows a b →
      ∀ u ∈ Set.extremePoints ℝ (Hirsch.Hpoly a b),
      ∀ v ∈ Set.extremePoints ℝ (Hirsch.Hpoly a b),
      ∀ L : ℕ, Hirsch.RowCircuitWalk a b L u v →
        ∃ w : ℕ → EuclideanSpace ℝ (Fin d),
          w 0 = u ∧ w (C * (n + d) ^ k * L) = v ∧
          ∀ j < C * (n + d) ^ k * L,
            w j = w (j + 1) ∨
              Hirsch.Adj (Hirsch.Hpoly a b) (w j) (w (j + 1)) := by sorry

Source

Proposed research bridge for the Polynomial Hirsch mission; sufficiency proved in Solutions/Sol_Hirsch_leaf_circuit_split.lean. Motivation, not proof of this bridge: arXiv:2602.06958v2. No literature-priority claim.

View graph