Transport and cycle-gap bounds control a normalized inverse-column entry

Proved

Hirsch.gain_normalized_column_bound

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

conditioninggain-graphshirsch-conjecturepolyhedra

Suppose a transported coordinate is at most Gamma times a positive root magnitude, while the normalization denominator is at least eta times that root magnitude. If Gamma is nonnegative and eta is positive, then the normalized coordinate is at most Gamma/eta. This is the scalar core of the gain-lattice inverse-column bound.

Preamble

import Mathlib
set_option autoImplicit false
noncomputable section

Formal statement

theorem Hirsch.gain_normalized_column_bound (x root denominator Gamma eta : ℝ)
    (hGamma : 0 ≤ Gamma) (heta : 0 < eta) (hroot : 0 < |root|)
    (htransport : |x| ≤ Gamma * |root|)
    (hgap : eta * |root| ≤ |denominator|) :
    |x / denominator| ≤ Gamma / eta := by sorry

Source

Standalone Mathlib-only restatement of the gain-lattice normalization primitive developed in PR #210.

View graph