Cubic circuit routing after irredundant normalization

Proved

Hirsch.cubic_circuit_walk_bound

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

convex-geometrypolytopes

A uniform constant C exists so that any separated feasible extreme endpoints of a bounded n-row H-polytope admit a retained subfamily of m <= n original rows defining exactly the same polytope, with no redundant rows and a strict feasible point, and a padded maximal circuit walk between those endpoints of length C(m+d)^3. Source-backed FORMALIZATION TARGET: finite minimal row selection and the strict midpoint, followed by an injective slack identification and Natura Theorem 3.1/Corollary 3.2. The paper states O(r^2 log r); this cubic envelope is weaker. The d=m=0 case uses a constant walk. This is not a graph-diameter theorem.

Preamble

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

Formal statement

theorem Hirsch.cubic_circuit_walk_bound :
∃ C : ℕ, ∀ (d n : ℕ)
      (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ),
      Bornology.IsBounded (Hirsch.Hpoly a b) →
      ∀ u ∈ Set.extremePoints ℝ (Hirsch.Hpoly a b),
      ∀ v ∈ Set.extremePoints ℝ (Hirsch.Hpoly a b),
      (∀ j, a j ≠ 0 → ⟪a j, u⟫ ≠ b j ∨ ⟪a j, v⟫ ≠ b j) →
      ∃ m : ℕ, m ≤ n ∧ ∃ e : Fin m ↪ Fin n,
        Hirsch.Hpoly (fun j => a (e j)) (fun j => b (e j)) = Hirsch.Hpoly a b ∧
        Hirsch.RowPresentationIrredundant (fun j => a (e j)) (fun j => b (e j)) ∧
        Hirsch.StrictlyFeasibleRows (fun j => a (e j)) (fun j => b (e j)) ∧
        Hirsch.RowCircuitWalk (fun j => a (e j)) (fun j => b (e j))
          (C * (m + d) ^ 3) u v := by sorry

Source

Bento Natura, arXiv:2602.06958v2 (10 February 2026), Theorem 3.1 and Corollary 3.2, plus elementary irredundant-row and slack-coordinate reductions detailed in research/CircuitLeafSplit.md.

View graph