Bounded H-polytope row map is injective

Proved

HirschCircuit.rowMap_injective_of_bounded

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

circuitshirsch-conjecturepolyhedraslack-coordinates

For a nonempty bounded H-polytope, the linear map sending a direction to all row inner products is injective. Otherwise a nonzero kernel direction would generate an entire feasible affine line, contradicting boundedness.

Preamble

import Definitions.Def_Hirsch_circuit_slack_model

set_option autoImplicit false
open scoped RealInnerProductSpace
open Hirsch

Formal statement

namespace HirschCircuit

theorem rowMap_injective_of_bounded
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (hb : Bornology.IsBounded (Hpoly a b))
    (x : EuclideanSpace ℝ (Fin d)) (hx : x ∈ Hpoly a b) :
    Function.Injective (rowMap a) := by sorry

end HirschCircuit

Source

Standard recession-space argument for bounded polyhedra; used in the slack-coordinate reduction of Bento Natura, arXiv:2602.06958v2, Sections 2–3.

View graph