Prove2Me

Nonnegative linear packing regions are downward closed

Proved
Hirsch.nonnegative_packing_region_downward_closed

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

hirsch-conjectureminkowski-sumspacking-polytopepolyhedra

Let a feasible scale vector t satisfy a finite family of linear packing inequalities whose coefficients are all nonnegative. Any other nonnegative vector s bounded coordinatewise by t is feasible as well. This elementary downward-closure property is used for exact simultaneous Minkowski-summand extraction regions: once a collection of candidate scales can be removed, reducing any subset of those scales preserves feasibility.

Preamble
import Mathlib
open scoped BigOperators
set_option autoImplicit false
noncomputable section
Formal statement
theorem Hirsch.nonnegative_packing_region_downward_closed
    {ι κ : Type*} [Fintype ι] [Fintype κ]
    (Γ : κ → ι → ℝ) (b : κ → ℝ)
    (hΓ : ∀ j i, 0 ≤ Γ j i) {s t : ι → ℝ}
    (ht_nonnegative : ∀ i, 0 ≤ t i)
    (ht_rows : ∀ j, (∑ i, Γ j i * t i) ≤ b j)
    (hs_nonnegative : ∀ i, 0 ≤ s i)
    (hst : ∀ i, s i ≤ t i) :
    (∀ i, 0 ≤ s i) ∧ ∀ j, (∑ i, Γ j i * s i) ≤ b j := by sorry
Source
Standalone Lean proof from PR #210 finite-summand packing work: https://github.com/jjoshua2/prove2me-work/blob/formal/dual-wall-carrier-routing/research/publication_packets/pr210_catchup/packing_downward/solution.lean

View graph