Tight rows outside a normal subspace cover its codimension

Proved

Hirsch.tight_rows_outside_subspace_cardinality_bound

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

face-coverformalizationgraph-diameterpolyhedra

Let $x$ be an extreme vertex of $P=\{x\in\mathbb R^d:\langle a_i,x\rangle\le b_i,\ i<n\}$ . For every linear subspace $U$ of the row-normal space,

\#\{i:a_i\notin U,\ \langle a_i,x\rangle=b_i\}\ge d-\dim U.

The count is of describing row indices, not a claim that all counted rows are mutually independent. Redundant and zero rows are allowed; no boundedness, strict feasibility, full-dimensionality, simplicity, or irredundancy assumption is made.

Preamble

import Mathlib
import Definitions.Def_Hirsch_model
open scoped BigOperators RealInnerProductSpace
open Set Hirsch
set_option autoImplicit false
attribute [local instance] Classical.propDecidable
set_option maxHeartbeats 12000000

Formal statement

namespace Hirsch

theorem tight_rows_outside_subspace_cardinality_bound {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (x : EuclideanSpace ℝ (Fin d))
    (hx : x ∈ extremePoints ℝ (Hpoly a b))
    (U : Submodule ℝ (EuclideanSpace ℝ (Fin d))) :
    d - Module.finrank ℝ U ≤
      (Finset.univ.filter (fun i => a i ∉ U ∧ ⟪a i, x⟫ = b i)).card := by sorry

end Hirsch

Source

https://github.com/jjoshua2/prove2me-work/blob/681314640b6f84792d8ae011c3534a6e8c456930/Solutions/PolynomialRankSensitiveFaceCover.lean ; declaration HirschRankFaceCover.tight_rows_outside_subspace_card_ge_codim; pinned CI run 34532572816.

View graph