Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Lemma 2, Eq.(107): worst-case concurrent rounding

Open
QAlgorithms.Papers.Independent.Intakethird100.P35.worst_concurrent_rounding

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let G′=(V,E′)G'=(V,E')G′=(V,E′) be finite and undirected, with r≥1r\ge1r≥1 indexed terminal pairs (si,ti)(s_i,t_i)(si​,ti​), distinct within each pair. Pairs may share vertices. Fix positive integers m,km,km,k and finite capacities ce≥0c_e\ge0ce​≥0, which may depend on them. Let NiN_iNi​ count all simple directed sis_isi​--tit_iti​ paths, N=max⁡iNiN=\max_iN_iN=maxi​Ni​, and let fworstmax⁡(c)f_{\mathrm{worst}}^{\max}(c)fworstmax​(c) 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 ⌊mkNce⌋\lfloor mkNc_e\rfloor⌊mkNce​⌋ labelled copies of edge eee, a single packing gives every pair FiF_iFi​ paths, with disjointness across all pairs as well as within each pair, and

∀i,Fi≥mkN(fworstmax⁡(c)−1k).\forall i,\qquad F_i\ge mkN\left(f_{\mathrm{worst}}^{\max}(c)-\frac1k\right).∀i,Fi​≥mkN(fworstmax​(c)−k1​).

This preserves concurrency when rounding the fair-flow objective. Empty path domains are allowed.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P35
Formal statement
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
Source
Linear programs for entanglement and key distribution in the quantum internet, arXiv:1809.03120v3, PDF p. 26, Lemma 2, Eq.(107): worst-case concurrent rounding
Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For all natural numbers n,e,rn,e,rn,e,r, let GGG have vertex set V={0,…,n−1}V=\{0,\ldots,n-1\}V={0,…,n−1} and edge set F={0,…,e−1}F=\{0,\ldots,e-1\}F={0,…,e−1}, with distinct endpoints ℓ(a),ρ(a)\ell(a),\rho(a)ℓ(a),ρ(a) for every edge, and assume that two edge labels with the same endpoints in the same or reversed order must be equal. Assume r>0r>0r>0, choose terminal maps s,t:{0,…,r−1}→Vs,t:\{0,\ldots,r-1\}\to Vs,t:{0,…,r−1}→V with si≠tis_i\ne t_isi​=ti​ for every index iii, choose positive natural numbers m,km,km,k, and choose nonnegative real capacities c(a)c(a)c(a). For each iii, let pip_ipi​ count all choices of a length d<nd<nd<n, an injective vertex sequence from sis_isi​ to tit_iti​, and ddd edge labels joining consecutive vertices in either orientation, and put N=max⁡ipiN=\max_i p_iN=maxi​pi​. Define WWW to be the total real supremum of all real zzz for which there exist functions hi:F×{0,1}→Rh_i:F\times\{0,1\}\to\mathbb Rhi​:F×{0,1}→R satisfying hi(a,b)≥0h_i(a,b)\ge0hi​(a,b)≥0 for all indices, edges, and direction indices; ∑i(hi(a,0)+hi(a,1))≤c(a)\sum_i(h_i(a,0)+h_i(a,1))\le c(a)∑i​(hi​(a,0)+hi​(a,1))≤c(a) for each edge; Δhi(v)=0\Delta_{h_i}(v)=0Δhi​​(v)=0 for every v≠si,tiv\ne s_i,t_iv=si​,ti​; and z≤Δhi(si)z\le\Delta_{h_i}(s_i)z≤Δhi​​(si​) for every iii, where Δh(v)=∑a∈F(1ℓ(a)=v(h(a,0)−h(a,1))+1ρ(a)=v(h(a,1)−h(a,0)))\Delta_h(v)=\sum_{a\in F}\bigl(\mathbf1_{\ell(a)=v}(h(a,0)-h(a,1))+\mathbf1_{\rho(a)=v}(h(a,1)-h(a,0))\bigr)Δh​(v)=∑a∈F​(1ℓ(a)=v​(h(a,0)−h(a,1))+1ρ(a)=v​(h(a,1)−h(a,0))). Replace each edge aaa by L(a)=⌊(mkN)c(a)⌋NL(a)=\lfloor(mkN)c(a)\rfloor_{\mathbb N}L(a)=⌊(mkN)c(a)⌋N​ labeled copies with the same endpoints. Then there exists a packing with a natural count qiq_iqi​ for each terminal index and qiq_iqi​ selected paths from sis_isi​ to tit_iti​, each having length less than nnn, 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 (mkN)(W−1/k)≤qi(mkN)(W-1/k)\le q_i(mkN)(W−1/k)≤qi​ for every iii, with natural numbers interpreted as reals in these inequalities. Terminal pairs may repeat or share vertices. The assumptions force n≥2n\ge2n≥2 but permit e=0e=0e=0 and N=0N=0N=0; if N=0N=0N=0, there are no copied edges, all counts are zero, and every asserted inequality is 0≤00\le00≤0. A nonpositive left side does not require a positive count.

Human review
  • Endorsed by Shuze Chen · Nov 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Gohan · Nov 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me