Unnumbered main claim: polynomial LP description size

Open

QAlgorithms.Papers.Independent.Intakethird100.P35.lp_polynomial_description_size

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

prove2quantum

Consider the four optimized flow programs (12), (19), (21), and (37) on a finite network with $n$ vertices, $e$ undirected edges, $d$ directed channel labels, $r\ge1$ terminal pairs, and a terminal group $S$ with $|S|\ge2$ . Each directed label is mapped to its underlying undirected edge; its supplied finite nonnegative channel coefficient is multiplied by its frequency. The explicit coefficient arrays include both orientations, flow nonnegativity and conservation, frequency normalization and bounds, shared or independent edge budgets as appropriate, and the slack constraints for worst-case and connectivity objectives. Write $D_j$ for the number of real scalar entries in the dense constraint matrix, right-hand side, and objective of program $j$ . There is an absolute positive integer $C$ such that, uniformly over all these data,

D_j\le C\,(n+e+d+r+|S|+1)^8,\qquad j\in\{12,19,21,37\}.

Thus their combinatorial descriptions have polynomial size. The deliberately loose polynomial bound concerns scalar-entry counts; exact solution time or bit complexity for arbitrary real coefficients is not asserted. Redundant zero endpoint-conservation rows and one fixed-zero unused slack in the single/total encodings preserve the feasible flows and objective.

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.2,16: the four actual LP coefficient arrays have polynomial size.
The universal constant precedes all network data. The generous degree-eight
bound avoids endorsing p.16's inconsistent exact slack counts. This is solely
the combinatorial description-size claim; no arbitrary-real polynomial-time
solver claim or operational-capacity claim is included. -/
theorem lp_polynomial_description_size :
    ∃ Csize : ℕ, 0 < Csize ∧
    ∀ (n e d r : ℕ) (G : EdgeGraph n (Fin e)) (hSimple : IsSimple G)
      (a b : Fin n) (hab : a ≠ b) (hr : 0 < r)
      (s t : Fin r → Fin n) (hst : ∀ i, s i ≠ t i)
      (S : Finset (Fin n)) (hS : 2 ≤ S.card)
      (edgeOf : Fin d → Fin e) (c : Fin d → ℝ) (hc : ∀ j, 0 ≤ c j),
      let bound := Csize * (n + e + d + r + S.card + 1) ^ 8
      descriptionSize (optimizedLP G (fun _ : Fin 1 => a)
        (fun _ : Fin 1 => b) edgeOf c false false) ≤ bound ∧
      descriptionSize (optimizedLP G s t edgeOf c false false) ≤ bound ∧
      descriptionSize (optimizedLP G s t edgeOf c false true) ≤ bound ∧
      descriptionSize (optimizedLP G (fun p : TerminalPair S => p.val.1)
        (fun p : TerminalPair S => p.val.2) edgeOf c true true) ≤ bound := 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. 2, Unnumbered main claim: polynomial LP description size

Read-back

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

There exists a positive natural number $C_{\mathrm{size}}$ with the following uniform property. Let $n,e,d,r$ be natural numbers, and let a graph have vertices $\{0,\ldots,n-1\}$ , edges $\{0,\ldots,e-1\}$ , and designated left and right endpoints for each edge. Assume each edge has distinct endpoints, and assume that whenever two edges have the same endpoints in either order, they are equal. Let $a,b$ be distinct vertices; assume $r>0$ ; let $s,t:\{0,\ldots,r-1\}\to\{0,\ldots,n-1\}$ satisfy $s(i)\ne t(i)$ for every $i$ ; let $S$ be a finite set of vertices with $q=|S|\ge2$ ; let $\operatorname{edgeOf}:\{0,\ldots,d-1\}\to\{0,\ldots,e-1\}$ be any function; and let $c:\{0,\ldots,d-1\}\to\mathbb R$ satisfy $c(j)\ge0$ for every $j$ . Write $p$ for the number of pairs $(u,v)$ with $u,v\in S$ and $u<v$ , and set

\begin{aligned} B&=C_{\mathrm{size}}(n+e+d+r+q+1)^8,\\ V_k&=2ke+d+1,\\ R_k&=2ke+2d+kn+e+2,\\ W_k&=2ke+2d+kn+e+k+1,\\ T_k&=3ke+2d+kn+k+1. \end{aligned}

Then all four inequalities hold:

\begin{aligned} V_1(R_1+1)+R_1&\le B,\\ V_r(R_r+1)+R_r&\le B,\\ V_r(W_r+1)+W_r&\le B,\\ V_p(T_p+1)+T_p&\le B. \end{aligned}

Here these expressions explicitly expand the description sizes of the four specified linear programs: each program with $k$ flow indices has $2ke$ real flow coordinates, $d$ real frequency coordinates, and one real slack coordinate, giving $V_k$ variables. Each includes $2ke$ flow-nonnegativity rows, $2d$ frequency-bound rows, one row setting the sum of frequencies to $1$ , and $kn$ conservation rows, including zero rows at the designated terminals. The first two programs additionally have $e$ shared-capacity rows and one row fixing slack to zero, giving respectively $R_1$ and $R_r$ rows; the third has $e$ shared-capacity rows and $r$ rows bounding slack by each source’s net outflow, giving $W_r$ rows; the fourth has $pe$ separate capacity rows and $p$ such slack-bound rows, giving $T_p$ rows. The fourth program’s flow indices are precisely the increasing pairs in $S$ . The assumptions exclude $n=0$ , $n=1$ , and $r=0$ ; they allow $e=0$ or $d=0$ whenever the required function $\operatorname{edgeOf}$ exists, and when $d=0$ the frequency-sum row is still counted even though it requires $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