Fractional transition packing lower-bounds route length
ProvedHirsch.weighted_transition_lower_boundgraph-distancehirsch-conjecturelinear-programmingpolyhedra
Consider a route of L transitions and a collection of required factor changes. Assign nonnegative weights to the factors. If each factor's required demand is no larger than the total amount it changes along the route, and every single route transition carries weighted change at most one, then the weighted total demand is at most L. This supplies a reusable fractional lower bound for ordinary-edge routes when one edge may change several overlapping Minkowski factors at once.
Preamble
import Mathlib open scoped BigOperators set_option autoImplicit false noncomputable section
Formal statement
theorem Hirsch.weighted_transition_lower_bound
{ι : Type*} [Fintype ι]
(L : ℕ) (weight demand : ι → ℝ) (change : ι → Fin L → ℝ)
(hw : ∀ i, 0 ≤ weight i)
(hd : ∀ i, demand i ≤ ∑ j, change i j)
(hstep : ∀ j, (∑ i, weight i * change i j) ≤ 1) :
(∑ i, weight i * demand i) ≤ (L : ℝ) := by sorrySource
Standalone Lean proof from PR #210 direction-local extraction work: https://github.com/jjoshua2/prove2me-work/blob/formal/dual-wall-carrier-routing/research/publication_packets/pr210_catchup/weighted_transition/solution.lean