Lemma 2, Eq.(107): worst-case concurrent rounding
OpenQAlgorithms.Papers.Independent.Intakethird100.P35.worst_concurrent_roundingLet be finite and undirected, with indexed terminal pairs , distinct within each pair. Pairs may share vertices. Fix positive integers and finite capacities , which may depend on them. Let count all simple directed -- paths, , and let be the maximum common lower bound on the net source flows of a single concurrent flow family. All commodities and both directions share each physical capacity. In the multigraph with labelled copies of edge , a single packing gives every pair paths, with disjointness across all pairs as well as within each pair, and
This preserves concurrency when rounding the fair-flow objective. Empty path domains are allowed.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P35
noncomputable section
namespace QAlgorithms.Papers.Independent.Intakethird100.P35
open scoped BigOperators
attribute [local instance] Classical.propDecidable Classical.decEq
/-- PDF pp.26--27, Lemma 2, (107): concurrent worst-case rounding.
N=max_i N_i is computed, and every commodity shares one edge-copy packing. -/
theorem worst_concurrent_rounding {n e r : ℕ} (G : EdgeGraph n (Fin e))
(hSimple : IsSimple G) (hr : 0 < r) (s t : Fin r → Fin n)
(hst : ∀ i, s i ≠ t i) (m k : ℕ) (hm : 0 < m) (hk : 0 < k)
(c : Fin e → ℝ) (hc : ∀ a, 0 ≤ c a) :
∃ P : Packing G (roundedCopies c m k (maxPathCount G s t)) s t,
∀ i, ((m * k * maxPathCount G s t : ℕ) : ℝ) *
(worstValue G c s t - 1 / (k : ℝ)) ≤ (P.count i : ℝ) := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P35
end
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For all natural numbers , let have vertex set and edge set , with distinct endpoints for every edge, and assume that two edge labels with the same endpoints in the same or reversed order must be equal. Assume , choose terminal maps with for every index , choose positive natural numbers , and choose nonnegative real capacities . For each , let count all choices of a length , an injective vertex sequence from to , and edge labels joining consecutive vertices in either orientation, and put . Define to be the total real supremum of all real for which there exist functions satisfying for all indices, edges, and direction indices; for each edge; for every ; and for every , where . Replace each edge by labeled copies with the same endpoints. Then there exists a packing with a natural count for each terminal index and selected paths from to , each having length less than , an injective vertex sequence, and copied edges joining consecutive vertices in either orientation, such that any two distinct selected occurrences share no copied edge, whether their terminal indices agree or differ, and for every , with natural numbers interpreted as reals in these inequalities. Terminal pairs may repeat or share vertices. The assumptions force but permit and ; if , there are no copied edges, all counts are zero, and every asserted inequality is . A nonpositive left side does not require a positive count.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.