Common rows do not contribute effective common-face inequalities

Proved

Hirsch.common_face_effective_count_le_rows_minus_common

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

faceshirsch-conjecturelinear-algebrapolyhedra

Every nonzero row active at both defining points becomes a zero normal after restriction to their common-direction space. Therefore common rows and effective restricted rows are disjoint, and the effective row count is at most the total number of describing rows minus the number of common rows.

Preamble

import Definitions.Def_Hirsch_common_face_geometry

open scoped RealInnerProductSpace
open Set Hirsch

Formal statement

namespace Hirsch

theorem common_face_effective_count_le_rows_minus_common
    {d n : ℕ}
    (a : Fin n → EuclideanSpace ℝ (Fin d)) (b : Fin n → ℝ)
    (p q : EuclideanSpace ℝ (Fin d)) :
    HirschCommonFace.commonFaceEffectiveCount a b p q ≤
      n - (HirschCommonFace.commonSourceRows a b p q).card := by sorry

end Hirsch

Source

Verified effective-row count lemma from the Polynomial Hirsch formalization, jjoshua2/prove2me-work PR #33.

View graph