Lemma 3, Eq.(121): total concurrent rounding

Open

QAlgorithms.Papers.Independent.Intakethird100.P35.total_concurrent_rounding

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

prove2quantum

Let $G'=(V,E')$ be finite and undirected, with $r\ge1$ indexed pairs $(s_i,t_i)$ , distinct within each pair. Fix positive integers $m,k$ and finite nonnegative capacities $c_e$ , allowing dependence on $m,k$ . Let $N_i$ count all simple directed paths for pair $i$ and put $N=\sum_iN_i$ . Let $f_{\mathrm{total}}^{\max}(c)$ maximize the sum of net source flows under conservation, nonnegativity, and one shared physical edge budget across all commodities and both orientations. In the multigraph having $\lfloor mkNc_e\rfloor$ labelled copies of each edge $e$ , there is one concurrently edge-disjoint packing with $F_i$ paths for each pair such that

\sum_{i=1}^r F_i\ge mkN\left(f_{\mathrm{total}}^{\max}(c)-\frac1k\right).

The estimate rounds the total throughput objective. The sum defining $N$ differs from the maximum in Lemma 2; if every path set is empty, the empty packing applies.

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.27--28, Lemma 3, (121): concurrent total rounding, N=sum_i N_i.
Printed proof (128) says worst; the statement (121), objective (122), and estimate
(127) all say total. We state the lemma's total objective without using (128). -/
theorem total_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 (sumPathCount G s t)) s t,
      ((m * k * sumPathCount G s t : ℕ) : ℝ) *
        (totalValue G c s t - 1 / (k : ℝ)) ≤ ∑ i, (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. 27, Lemma 3, Eq.(121): total concurrent rounding

Read-back

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

For all natural numbers $n,e,r$ , consider a graph $G$ with vertices $\{0,\ldots,n-1\}$ , edges $\{0,\ldots,e-1\}$ , and designated endpoints $L(a)\ne R(a)$ for each edge $a$ ; assume that two edges with the same endpoints, in either order, must be equal. Suppose $r>0$ , and choose vertices $s_i\ne t_i$ for every $i\in\{0,\ldots,r-1\}$ , positive natural numbers $m,k$ , and nonnegative real capacities $c_a$ . For a collection of real directed edge quantities $f_{i,a,0},f_{i,a,1}$ , define the net outflow of collection $i$ at vertex $v$ by

D_i(v)=\sum_{a=0}^{e-1}\left( \mathbf 1_{L(a)=v}(f_{i,a,0}-f_{i,a,1}) +\mathbf 1_{R(a)=v}(f_{i,a,1}-f_{i,a,0}) \right).

Let $V$ be the supremum of all values $\sum_iD_i(s_i)$ arising from collections satisfying $f_{i,a,b}\ge0$ , $\sum_i(f_{i,a,0}+f_{i,a,1})\le c_a$ for each edge, and $D_i(v)=0$ whenever $v\ne s_i,t_i$ . Let $N$ be the sum, over all $i$ , of the number of paths from $s_i$ to $t_i$ specified by a length $\ell\in\{0,\ldots,n-1\}$ , an injective vertex sequence $v_0,\ldots,v_\ell$ with the stated endpoints, and an edge sequence whose $j$ -th edge joins $v_j$ and $v_{j+1}$ in either endpoint order. Replace each original edge $a$ by $\lfloor mkN c_a\rfloor_+$ individually labelled copies, where the natural-number floor is zero for negative inputs. There exist natural numbers $p_i$ and $p_i$ such paths for each pair $(s_i,t_i)$ in the copied graph, with no labelled edge copy shared by two distinct selected paths, such that

mkN\left(V-\frac1k\right)\le\sum_{i=0}^{r-1}p_i.

No connectivity or positive-capacity hypothesis is imposed: $e=0$ and $N=0$ are allowed; when $N=0$ , there are no copied edges, all selected path counts are zero, and the displayed inequality is $0\le0$ . The terminal hypotheses exclude $n=0,1$ .

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