Conformal elementary decomposition with an ambient-coordinate bound

Proved

HirschCircuit.elementary_conformal_decomposition_ambient_bound

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

circuitsconformal-decompositionlinear-algebrapolyhedra

Every vector $z$ in a real linear subspace $K\subseteq\mathbb R^n$ can be written as a sum of at most $n$ nonzero support-minimal vectors of $K$ . Each summand has the same closed-orthant signs as $z$ and is coordinatewise no larger in absolute value. The zero vector is represented by the empty sum. This ambient-coordinate bound does not assert a maximal circuit-walk bound or the sharper dimension bound.

Preamble

import Definitions.Def_Hirsch_circuit_slack_model
set_option autoImplicit false

Formal statement

theorem HirschCircuit.elementary_conformal_decomposition_ambient_bound {n : ℕ}
    (K : Submodule ℝ (Fin n → ℝ)) (z : Fin n → ℝ) (hz : z ∈ K) :
    ∃ gs : List (Fin n → ℝ), gs.length ≤ n ∧
      (∀ g ∈ gs, HirschCircuit.IsElementaryIn K g ∧
        ∀ i, 0 ≤ g i * z i ∧ |g i| ≤ |z i|) ∧ gs.sum = z := by sorry

Source

Bento Natura, Circuit Diameter of Polyhedra is Strongly Polynomial, arXiv:2602.06958v2, Definition 2.1 and Lemma 2.2. Matrix-free ambient-coordinate relaxation, proved by support-cardinality induction; no novelty claim.

View graph