All missions

Motivation

Large service systems such as call centres, hospital wards and cloud server farms route several customer classes to several server pools, with each pool trained for only some of the classes. Staffing such a network sits between two failure modes: too few servers make queues explode, and too many waste capacity. In the Halfin–Whitt (quality-and-efficiency-driven) regime, arrival rates and pool sizes grow like $n$ and the staffing surplus or deficit of each pool is of order $\sqrt n$. Whether those $O(\sqrt n)$ surpluses can be scheduled into a stable system is a question about the network as a whole: a surplus in one pool can serve a deficit elsewhere only through the compatibility graph.

Hmedi, Arapostathis and Pang (arXiv:2009.01942, v3, 2021; Operations Research 2023) answer this for networks whose compatibility graph is a tree and that have no abandonment. They introduce one number, the system-wide safety staffing (SWSS) $\vartheta_p$, the value of a small linear program. They prove that its sign decides stability.

Timeline.

• Atar (2005) derived the limiting diffusion of tree networks under complete resource pooling.
• Arapostathis and Pang (2016) obtained the triangular form of its drift.
• Hmedi, Arapostathis and Pang (2019) characterized uniform stability through the "spare capacity" $-\langle e,B_1^{-1}h\rangle$, for networks with one non-leaf pool.
• The present paper (2021) treats general trees and identifies the spare capacity with $\vartheta_p$.

Setting

There are $I$ classes and $J$ pools. Write $i\sim j$ if pool $j$ can serve class $i$, and assume the bipartite graph $G$ with these edges is a tree. The first-order rates are $\lambda_i>0$, $\nu_j>0$ and $\mu_{ij}>0$, and the second-order corrections are $\hat\lambda_i,\hat\nu_j,\hat\mu_{ij}\in\mathbb R$. Complete resource pooling (CRP) means that the linear program "minimize $\max_j\sum_i\xi_{ij}$ subject to $\sum_j\mu_{ij}\nu_j\xi_{ij}=\lambda_i$, $\xi\ge0$ on the edges" has a unique solution $\xi^*$, with $\sum_i\xi^*_{ij}=1$ and $\xi^*>0$ on every edge. Put $z^*_{ij}=\xi^*_{ij}\nu_j$ and $\theta_j=\hat\nu_j+\sum_i(\hat\mu_{ij}/\mu_{ij})z^*_{ij}$.

For a positive probability vector $p$, the SWSS parameter $\vartheta_p$ is the optimal value of

$$\text{(LP}')\quad \max\ \vartheta\quad\text{s.t.}\quad \hat\lambda_i\le\sum_{j}\mu_{ij}\kappa_{ij}-\vartheta p_i\ \ \forall i,\qquad \sum_i\kappa_{ij}=\theta_j\ \ \forall j,$$

over $\vartheta\in\mathbb R$ and $\kappa$ supported on the edges.

Let $\Psi(\alpha,\beta)$ be the unique array on the edges with row sums $\alpha$ and column sums $\beta$ (defined when $\langle e,\alpha\rangle=\langle e,\beta\rangle$). Let $h_i=\hat\lambda_i-\sum_j(\mu_{ij}\xi^*_{ij}\hat\nu_j+\hat\mu_{ij}z^*_{ij})$. The limiting controlled diffusion is

$$dX_t=b(X_t,U_t)\,dt+\Sigma\,dW_t,\qquad b_i(x,u)=h_i-\sum_j\mu_{ij}\Psi_{ij}\big(x-\langle e,x\rangle^+u^c,\,-\langle e,x\rangle^-u^s\big),$$

with $\Sigma=\mathrm{diag}(\sqrt{2\lambda_i})$ and $W$ a standard Brownian motion. Here $\langle e,x\rangle^+$ is the total queue, $\langle e,x\rangle^-$ the number of idle servers, and the control $u=(u^c,u^s)\in\Delta_I\times\Delta_J$ says how queued customers are split among classes and idle servers among pools. A stationary Markov control is a Borel map $v:\mathbb R^I\to\Delta_I\times\Delta_J$, used as $U_t=v(X_t)$.

Formalization targets

Goal: Theorem 1 (limiting-diffusion clauses), p. 9

(a) If $\vartheta_p>0$, then for every edge $(\hat\imath,\hat\jmath)$, under the constant control $\bar v=(e_{\hat\imath},e_{\hat\jmath})$, the diffusion has a unique invariant probability measure $\pi$. Moreover there are $c\in\mathbb R^I$, $S\succ0$ and $\varepsilon>0$ such that, with $V(x)=\exp\big(\varepsilon\|x-c\|_S^2(1+\|x-c\|_S^2)^{-1/2}\big)$,

$$\int V\,d\pi<\infty,\qquad \|P_t(x,\cdot)-\pi\|_V\le C\,V(x)\,e^{-\gamma t}\quad\forall x,\ t\ge0 .$$

(b) If $\vartheta_p<0$, then under every stationary Markov control $|X_t|\to\infty$ almost surely. If $\vartheta_p=0$, then under every stationary Markov control there is no invariant probability measure.

Milestones

• Atar's uniqueness of $\Psi$ on a tree (p. 17).
• Proposition 2: the drift equals $h-B_1(x-\langle e,x\rangle^+u^c)+\langle e,x\rangle^-B_2u^s$, with $B_1$ triangular.
• Theorem 2: closed form of $\vartheta_p$ through path gains $d$.
• Remark 1: the sign of $\vartheta_p$ does not depend on $p$.
• Theorem 3: $d(i,\ell)=(e^{\mathsf T}B_1^{-1})_\ell/(e^{\mathsf T}B_1^{-1})_i$.
• Theorem 4: $\vartheta_p=-\langle e,B_1^{-1}h\rangle/\langle e,B_1^{-1}p\rangle$.
• Lemma 1.
• Theorem 5: the instability half of the goal.
• Remark 8: the recentring shift $\zeta$.
• The Dieker–Gao Lyapunov matrix (p. 25).
• Theorem 7: the Foster–Lyapunov inequality (57) and exponential ergodicity (58).

Significance

The theorem turns a stochastic stability question into the sign of a linear-program value computable from the network data. Positive SWSS is the condition under which a staffing rule with $O(\sqrt n)$ safety capacity can be made stable by scheduling, and the proof exhibits a simple stabilizing control. The identity $\vartheta_p\langle e,B_1^{-1}p\rangle=-\langle e,B_1^{-1}h\rangle$ links the LP value to the drift of the diffusion. It extends earlier uniform-stability results from networks with a single non-leaf pool to arbitrary trees.

The results are proved on paper. This mission produces machine-checked statements, and eventually proofs, of the limiting-diffusion half. That requires:

• a general tree-network model;
• its flow map $\Psi$ and drift;
• the linear-algebraic identities between path gains and $B_1^{-1}$;
• a notion of transience for diffusions;
• an exponential-ergodicity statement for a piecewise-linear drift.

No part of this is formalized elsewhere. The existing platform layers for Halfin–Whitt diffusions concern single-pool networks.

Difficulty

The linear-algebra half is a genuine induction on trees, not an unfolding of definitions. Theorem 2 eliminates leaves class by class. Theorem 3 identifies the gains with the entries of $e^{\mathsf T}B_1^{-1}$, which forces $B_1$ to be invertible and $e^{\mathsf T}B_1^{-1}$ to be positive. Theorem 4 then rewrites the LP value through the drift.

The probabilistic half is harder:

• Transience for $\vartheta_p<0$ must hold under every Borel control. The drift is then discontinuous, so the argument must work with a bounded test function whose generator has a sign uniformly in the control, and with the recurrence–transience dichotomy for nondegenerate diffusions.
• The case $\vartheta_p=0$ is a borderline case that no single Lyapunov function settles.
• For $\vartheta_p>0$, the drift under $\bar v$ is linear on each of two half-spaces. One quadratic form must decrease along both pieces, and one piece has a zero eigenvalue. A naive choice of $S$ (for instance the identity) fails there.
• The ergodic statement needs a Foster–Lyapunov theorem for diffusions, which is not available in Mathlib.

Formalization scope

Classes are Fin I and pools Fin J, and the tree is SimpleGraph.IsTree on Fin I ⊕ Fin J. States are EuclideanSpace ℝ (Fin I), and control values are pairs of vectors in Mathlib's stdSimplex. Strong solutions, standard Brownian motion, invariant measures, the generator and the weighted total-variation norm are the published EthierKurtz, GPhNGIDiffusion.EMError and UnifErgHW.Diffusion definitions. The weighted norm uses the weight $1+V$, which is equivalent to the paper's $V$-norm up to a factor $2$.

Conventions committed to:

• $\vartheta_p$ is the supremum of the feasible values of (LP′); it is never defined by a closed formula.
• $\Psi$ is chosen as the unique solution of (37), with junk value $0$ off $D$.
• $B_1$, $B_2$ are defined for a chosen pool $\hat\jmath$ by eliminating $\beta_{\hat\jmath}$.
• The drift is (42) of the network data. Its triangular form (43) is Proposition 2, a theorem.
• Transience is $|X_t|\to\infty$ a.s. for every strong solution.
• "Not positive recurrent" is the absence of an invariant probability measure.

The statement admits trivializations, each ruled out:

• (a) asserts the existence of strong solutions, so its transition probability is not an arbitrary choice.
• (b) quantifies over every Borel control and every strong solution.
• The ergodic bound has its constants ordered $\exists c,S,\varepsilon$, then $\exists\gamma,C$, then $\forall t,x$, with $S\succ0$ and $\varepsilon>0$.

For the instability clauses, strong solutions exist and are pathwise unique for every Borel control (a theorem of Veretennikov, 1981, and its locally bounded extensions; the drift is locally bounded with linear growth and the noise is additive and nondegenerate). This is background, not a claim of the mission.

Out of scope: the clauses of Theorem 1 about the diffusion-scaled $n$th systems (Theorems 6 and 8), and the $\vartheta^n_p$ half of Theorem 4. They need a controlled continuous-time Markov chain layer with work-conserving action sets, which does not exist on the platform.

Welcome contributions:

• proofs of the tree identities (Theorems 2–4, Lemma 1, Proposition 2);
• a reusable Foster–Lyapunov-to-exponential-ergodicity theorem for diffusions with additive noise;
• a reusable transience criterion via bounded submartingales.

Selected references

• H. Hmedi, A. Arapostathis, G. Pang, On system-wide safety staffing of large-scale parallel server networks, arXiv:2009.01942v3, 2021; Operations Research (2023). https://arxiv.org/abs/2009.01942
• R. Atar, A diffusion model of scheduling control in queueing systems with many servers, Annals of Applied Probability 15(1B) (2005). https://doi.org/10.1214/105051604000000963
• R. Atar, Scheduling control for queueing systems with many servers: asymptotic optimality in heavy traffic, Annals of Applied Probability 15(4) (2005). https://doi.org/10.1214/105051605000000601
• A. Arapostathis, G. Pang, Ergodic diffusion control of multiclass multi-pool networks in the Halfin–Whitt regime, Annals of Applied Probability 26(5) (2016). https://doi.org/10.1214/16-AAP1171
• A. B. Dieker, X. Gao, Positive recurrence of piecewise Ornstein–Uhlenbeck processes and common quadratic Lyapunov functions, Annals of Applied Probability 23(4) (2013). https://doi.org/10.1214/12-AAP870
• H. Hmedi, A. Arapostathis, G. Pang, Uniform stability of a class of large-scale parallel server networks, arXiv:1907.04793, 2019. https://arxiv.org/abs/1907.04793
• S. P. Meyn, R. L. Tweedie, Stability of Markovian processes III: Foster–Lyapunov criteria for continuous-time processes, Advances in Applied Probability 25 (1993). https://doi.org/10.2307/1427522

Motivation

In 1923 Hardy and Littlewood proposed two conjectures about the distribution of primes that have shaped a century of analytic number theory. The first — the prime $k$-tuple conjecture — predicts that every admissible prime constellation $(p, p + m_1, \dots, p + m_k)$ occurs with a precise asymptotic density: the number $\pi_P(n)$ of constellations with base point $p \le n$ grows like $C_P \int_2^n dt/(\log t)^{k+1}$, where the singular series constant $C_P$ is an explicit Euler product over the residues of the offsets modulo the primes. For the twin offsets this specializes to the twin prime conjecture with the twin-prime constant $2C_2 \approx 1.3203$. The second conjecture asserts that the prime-counting function is subadditive: $\pi(x+y) \le \pi(x) + \pi(y)$. Richards proved in 1974 that the two conjectures are incompatible — at most one of them is true. The source file states all three results in Lean 4: the two conjectures as open problems, and the incompatibility as a theorem.

The mission takes the first conjecture — the file's title statement, and the one widely believed — as its goal. It formalizes the conjecture's definitional core (prime constellations, admissibility, counting functions, the singular series), and curates as milestones the structural facts any proof must engage: the translation-invariance of admissibility, its necessity for primality, the vanishing count for inadmissible tuples, the divergence of the logarithmic-integral model, the positivity of the singular series, the infinitude consequences down to the twin prime conjecture, and Richards' incompatibility with the second conjecture.

Timeline

• 1923 — G. H. Hardy and J. E. Littlewood state the prime $k$-tuple conjecture and the subadditivity conjecture for the prime-counting function in Some problems of "Partitio numerorum"; III, Acta Mathematica 44, pp. 1–70.
• 1974 — Ian Richards proves that the two conjectures are incompatible: the first, asserted for all tuples, implies the failure of the second for some pair $x, y$.
• 2025 — the Formal Conjectures project formalizes both conjectures and Richards' theorem in Lean 4; the present mission is built directly on that file (HardyLittlewood.lean).

The fragment and its conventions

The arena is the set of prime constellations: tuples $(p, p + 2m_1, \dots, p + 2m_k)$ of primes with even gaps, encoded by a function $m : \{0, \dots, k\} \to \mathbb{N}$ of offsets with $m_0 = 0$. A constellation is admissible when its entries do not form a complete set of residue classes modulo any prime; the counting function $\pi_P(n)$ counts admissible constellations with base point at most $n$; the singular series $C_P$ is $2^k \prod_{q \ge 3} \frac{1 - w(q;m)/q}{(1 - 1/q)^{k+1}}$ with $w(q; m)$ the number of residues occupied by the offsets modulo $q$; and the conjecture asserts $\pi_P(n) \sim C_P \int_2^n \frac{dt}{(\log t)^{k+1}}$ for tuples with distinct offsets.

Nine conventions deserve disclosure. First, the platform publishes definitions as modules Definitions.Def_<definition_name>, so the three definition bundles — constellations and admissibility, counting functions, and the asymptotic layer with the singular series — are published as platform definitions (HardyLittlewood_constellation, HardyLittlewood_counting, HardyLittlewood_series) and attached to the proposal as reference items; the theorem drafts import them. Second, asymptotic equivalence is phrased through a self-contained definition — f ~ g when the difference is little-o of g — rather than an external asymptotic-equivalence notation; the formulation coincides with the classical ratio limit when the model sequence is eventually positive and unbounded, and it degenerates correctly: for an inadmissible tuple the singular series is zero, the model vanishes identically, and the conjecture asserts exactly that the counting function is eventually zero, which is the true degenerate content. Third, the counting functions are defined as the cardinalities of finite sets of natural numbers (noncomputable, Classical), with $\pi$ counting primes up to and including $n$, matching the source's phrasing. Fourth, admissibility is split: the source's constellation-level condition is kept verbatim, and the parameter-free condition on the doubled offsets (IsAdmissibleTuple) is added beside it; the equivalence — residue coverage is invariant under translation by the base point — is the mission's first milestone, so nothing is assumed that is not proved. Fifth, the residue count $w(q; m)$ is taken on the offsets themselves, exactly as the source's numResidues; at every odd prime this agrees with the count for the doubled offsets $2m_i$, and the product runs over the primes $q \ge 3$ with the source's normalization and $2^k$ prefactor. Sixth, the singular series constant is defined through the unconditional infinite product; its convergence and positivity are not assumed anywhere — they are the content of a milestone, and the hypothesis that makes the product converge (pairwise distinct offsets) is stated there explicitly, since a repeated offset forces every factor to be $1 + O(1/q)$ and the product to diverge. Seventh, a curation decision: the goal is the first conjecture; the second conjecture is deliberately not drafted as a provable item, because Richards' theorem — itself a milestone — shows that the two cannot both hold; the second conjecture appears as a definition and inside the incompatibility milestone. Eighth, the goal is stated for every tuple, with the conjecture's own hypotheses ($m_0 = 0$ and pairwise distinct offsets) inside the predicate, exactly as the source file states it. Ninth, the read-backs attached to the drafts were written by the same model that produced the statements (readback_model glm-5-latest-short), not by an independent auditor; the human item-by-item comparison against the source remains the main defense against an unfaithful formalization.

Formalization targets

The goal is the first Hardy–Littlewood conjecture for every tuple. The supporting chain, in attack order, each step a milestone except the last:

• Translation invariance: a prime constellation at p is admissible exactly when it is a prime constellation and the doubled offsets are admissible.
• Necessity: if the residues of the entries cover all classes modulo a prime q < p, the tuple is not a prime constellation at p — some entry is a multiple of q larger than q.
• Vanishing: an inadmissible tuple has an identically zero counting function.
• Divergence: for every multiplicity, the model integral of $1/(\log t)^{k+1}$ from 2 to n tends to infinity.
• Positivity: for an admissible tuple of distinct offsets, the singular series constant is a strictly positive real.
• Infinitude: the conjecture, for an admissible tuple of distinct offsets, yields prime constellations at arbitrarily large base points.
• Twin admissibility: the twin offsets (0, 1) are admissible.
• Twin primes: the conjecture for the twin offsets yields infinitely many twin primes.
• Richards: the first conjecture (for all tuples) and the second conjecture (for all pairs $x, y \ge 2$) cannot both be true.

The chain assembles: admissibility is the gatekeeper (necessity and vanishing), the model integral and the singular series are the two analytic quantities the conjecture relates, positivity and divergence turn the asymptotic into infinitude, the twin case is the celebrated concrete consequence, and Richards' theorem fences off the second conjecture.

Significance

The prime $k$-tuple conjecture is the strongest concrete prediction about the distribution of primes that is consistent with current knowledge: it implies the twin prime conjecture, the Sophie Germain-type infinitudes, and every admissible pattern one can write down, each with a precise constant. It sits at the edge of the circle method — the same machinery that yields the ternary Goldbach theorem for additive patterns — and its obstruction is exactly the correlation between primes that current technology cannot rule in. A Lean formalization of the conjecture's statement, together with the surrounding structural facts, fixes the target unambiguously and gives solvers an attack path whose every waypoint is independently valuable: each milestone is a theorem of lasting interest in the theory of prime constellations, and the Richards incompatibility is a landmark result of 1974 that the community can be proud to carry.

Difficulty

The milestones span elementary number theory (residue coverage, admissibility, the twin-configuration check), real analysis (the divergence of the logarithmic integral), analytic number theory at the research frontier (the convergence and positivity of the singular series, via Mertens-type estimates), and combinatorial asymptotics for Richards' incompatibility. The admissibility lemmas are of moderate difficulty; the divergence of the model integral is a standard exercise in integral comparison; the positivity of the singular series requires the classical estimate that the Euler product converges on distinct offsets; the Richards milestone requires constructing, from the conjectured density of a suitable long admissible constellation, an interval carrying more primes than subadditivity permits — a research-grade formalization. The goal itself is one of the great open problems of number theory; the mission's value lies in the precisely stated target and the independently valuable waypoints, exactly the role of an OpenProblem mission.

Formalization scope

Every item quantifies only over the objects it needs — offset tuples, base points, primes, bounds; no item carries a vacuous hypothesis: the twin configuration is admissible, the conjunctions of the conjecture are satisfiable, and the vanishing and incompatibility statements are the intended degenerate truths. The fragment excludes the second Hardy–Littlewood conjecture as a provable target (Richards' theorem makes it a trap), excludes no case of the first conjecture (it is stated for every tuple, exactly as the source), and adds no hypothesis to the conjecture beyond the source's own. Nothing in the mission asserts the truth of the first conjecture or of the twin prime conjecture; it formalizes the statements precisely, together with the implications among them that are known.

Selected references

• G. H. Hardy and J. E. Littlewood, Some problems of "Partitio numerorum"; III: On the expression of a number as a sum of primes, Acta Mathematica 44 (1923), pp. 1–70 — the two conjectures and the singular series.
• I. Richards, On the Incompatibility of Two Conjectures Concerning Primes, Bulletin of the American Mathematical Society 80 (1974), pp. 419–438 — the incompatibility theorem.
• Formal Conjectures project, HardyLittlewood.lean (2025) — the mission's source file, Apache 2.0.
• Wikipedia, First Hardy–Littlewood conjecture and Second Hardy–Littlewood conjecture — the source file's own reference links.

Motivation

The entanglement-assisted classical capacity of a noisy quantum channel is the amount of information per channel use that can be sent over the channel in the limit of many uses of the channel, assuming that the sender and receiver have access to the resource of shared quantum entanglement, which may be used up by the communication protocol. We show that this capacity is given by an expression parallel to that for the capacity of a purely classical channel: i.e., the maximum, over channel inputs $\rho$, of the entropy of the channel input plus the entropy of the channel output minus their joint entropy, the latter being defined as the entropy of an entangled purification of $\rho$ after half of it has passed through the channel. We calculate entanglement-assisted capacities for two interesting quantum channels, the qubit amplitude damping channel and the bosonic channel with amplification/attenuation and Gaussian noise. We discuss how many independent parameters are required to completely characterize the asymptotic behavior of a general quantum channel, alone or in the presence of ancillary resources such as prior entanglement. In the classical analog of entanglement assisted communication--communication over a discrete memoryless channel (DMC) between parties who share prior random information--we show that one parameter is sufficient, i.e., that in the presence of prior shared random information, all DMC's of equal capacity can simulate one another with unit asymptotic efficiency.

This mission is the statement-level formalization of Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem (arXiv:quant-ph/0106052v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

12 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Theorem 1: entanglement-assisted classical capacity (Theorem 1: entanglement-assisted classical capacity, PDF p. 8). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

10 results of the paper are not stated yet, because the library lacks an interface they need:

• §I: a channel with Q > 0 but C = C_E: Counted noisy-channel steps interleaved with accepted finite LOCC, and source-compatible operational quantum-transmission capacities Q2, Q and unassisted C (hard)
• §III: finite-dimensional approximation for energy-constrained Gaussian channels: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• §III.A Eq.(78): large-noise enhancement factor: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• Fig.6: small-signal Gaussian capacity asymptotics: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• §III.A Eqs.(79)–(80): coherent-state bounds, with corrected regimes: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• §III.A: fixed signal-to-noise high-energy classical limit: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• §III.A Eqs.(82),(86): teleportation and dense-coding bounds: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• §III.A Eqs.(83)–(85),(87): optimized squeezed-state bounds: Positive trace-one multimode Fock states, spectral entropy/purification, reference-extended Gaussian CPTP maps, photon-energy constraints, and energy-constrained operational assisted capacity (hard)
• Corollary 2: constrained sources (source obstruction): A true source hypothesis sufficient for constrained-source tail efficiency (source-ambiguity)
• §V: proposed feedback consequence of the QRSC: Source-pinned composable quantum simulation criterion for adaptive feedback substitution (source-ambiguity)

Selected references

• Entanglement-assisted capacity of a quantum channel and the reverse Shannon theorem, arXiv:quant-ph/0106052v2, https://arxiv.org/abs/quant-ph/0106052v2

Motivation

We give a detailed proof of the conjecture that the asymptotic entanglement cost of preparing a bipartite state \rho is equal to the regularized entanglement of formation of \rho.

This mission is the statement-level formalization of The asymptotic entanglement cost of preparing a quantum state (arXiv:quant-ph/0008134v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

11 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement cost equals regularized entanglement of formation (Theorem 1 / Eq.(7), continued on PDF p.3, PDF p. 2). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Introduction, general monotone paragraph after Eq.(5): A specified normalization or asymptotic singlet-unit upper bound for the general function f. (source-ambiguity)

Selected references

• The asymptotic entanglement cost of preparing a quantum state, arXiv:quant-ph/0008134v1, https://arxiv.org/abs/quant-ph/0008134v1

Motivation

We develop entanglement-of-formation potentials for feedback-assisted classical communication and one-way randomness distillation. For a finite-dimensional quantum channel without initial shared entanglement, an exact amortization theorem bounds the increase of message information plus entanglement remaining across the communicating laboratories. This proves a classical-feedback capacity bound using a mixed-convex-roof expression previously studied by Winter and Yang in the context of potential capacities. We determine the capacity of flagged mixtures of noiseless and entanglement-breaking channels, improve a published depolarizing-channel converse, and evaluate the new bound exactly for the amplitude damping channel. A state analogue gives a finite-blocklength upper bound on the net shared randomness obtainable with one-way classical communication. Amplitude-damping Choi states provide exact benchmarks, while a full-rank generalized amplitude-damping Choi state demonstrates a useful improvement where we do not evaluate the operational rate exactly. We also distinguish one-way from two-way randomness distillation: a two-round weak-measurement protocol strictly exceeds the exact one-way rate of every nontrivial qubit isotropic state. The protocol preserves quantum side information during its first decoding and extracts additional randomness in the reverse direction. This shows why the one-way state potential is not a general two-way converse. Together, these results establish a common entanglement-based approach to sharper communication and randomness bounds, while revealing how retained quantum correlations enable two-way distillation to surpass one-way limits. △ Less

This mission is the statement-level formalization of Entanglement-of-formation potentials for feedback-assisted classical communication and randomness distillation (arXiv:2610.04831v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

27 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Proposition 2.1: cardinality and attainment (Proposition 2.1: cardinality and attainment, PDF p. 12). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

26 results of the paper are not stated yet, because the library lacks an interface they need:

• Theorem 4.3: classical-feedback capacity bound (abstract seed): A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Lemma 3.1: monotonicity under free operations: Message/transcript cq states, lawful message-controlled Alice and transcript-controlled Bob free operations, and their composition relation (hard)
• Proposition 5.3: tensor products and regularization: A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Theorem 6.1: exact flagged-channel capacity: A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Theorem 8.2: exact damping evaluation: A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Theorem 9.2: finite-blocklength one-way randomness: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Proposition 10.1: damping-source potential: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Proposition 11.1: one-way isotropic benchmark: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Theorem 12.1: two-round isotropic rate: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Corollary 12.2: strict two-way separation: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Flagged depolarizing simulation bound: A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Analytic depolarizing converse improvement: The channel beta feasible set (B.1) and limiting channel Upsilon minimization over arbitrary completely positive comparison maps; A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Fixed positive formation weights cannot close the depolarizing gap: The eta-weighted message/transcript potential and a computed near-pure Pauli-orbit one-use experiment; Message/transcript cq states, lawful message-controlled Alice and transcript-controlled Bob free operations, and their composition relation (hard)
• Jump-flagged damping transmits a perfect bit: A semantic n-use feedback code and its maximum-error finite-use capacity and inf-error liminf capacity (hard)
• Sharper converse with exactly uniform Alice key: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Derived forward/reverse damping-source rates: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Thermal operational interval and finite-error bound: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Old state-Upsilon lower certificates at thermal source: The state Upsilon_A/Upsilon_B comparison sets (10.38)-(10.39), with support-aware bit-valued Umegaki divergence on nonnormalized positive comparison operators (hard)
• Exact-component upper bound for thermal family: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Perturbation potential bound and achievable rate: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Explicit perturbed-source improvement: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates; The state Upsilon_A/Upsilon_B comparison sets (10.38)-(10.39), with support-aware bit-valued Umegaki divergence on nonnormalized positive comparison operators (hard)
• One-way potential cannot upper-bound two-way extraction: One-way and finite-round two-way LOCC randomness protocols, their squared-fidelity acceptance law, alphabet-size communication charge, and inf-error liminf rates (hard)
• Appendix B.1: beta for twirled comparison maps: Source ambiguity: redundant orthogonal Choi sector when d=1 (source-ambiguity)
• Appendix B.2: general depolarizing Upsilon formula: The channel beta feasible set (B.1) and limiting channel Upsilon minimization over arbitrary completely positive comparison maps (hard)
• Appendix E.1: state-converse supporting hyperplanes: The state Upsilon_A/Upsilon_B comparison sets (10.38)-(10.39), with support-aware bit-valued Umegaki divergence on nonnormalized positive comparison operators and the natural-matrix-log derivative/supporting functional (hard)
• Appendix E.3: transport of certificates under noise: The state Upsilon_A/Upsilon_B comparison sets (10.38)-(10.39), with support-aware bit-valued Umegaki divergence on nonnormalized positive comparison operators and the reference certificate operators under perturbation (hard)

Selected references

• Entanglement-of-formation potentials for feedback-assisted classical communication and randomness distillation, arXiv:2610.04831v1, https://arxiv.org/abs/2610.04831v1

Motivation

A new protocol for quantum broadcast channels based on the fully quantum Slepian-Wolf protocol is presented. The protocol yields an achievable rate region for entanglement-assisted transmission of quantum information through a quantum broadcast channel that can be considered the quantum analogue of Marton's region for classical broadcast channels. The protocol can be adapted to yield achievable rate regions for unassisted quantum communication and for entanglement-assisted classical communication; in the case of unassisted transmission, the region we obtain has no independent constraint on the sum rate, only on the individual transmission rates. Regularized versions of all three rate regions are provably optimal.

This mission is the statement-level formalization of A father protocol for quantum broadcast channels (arXiv:quant-ph/0612155v4). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

10 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Entanglement-assisted broadcast father inner region (Theorem 2 / Eq. (9), PDF p. 4). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• VI.C, asserted multiparty one-shot extension: A numerical multiparty one-shot trace-norm error functional, its aggregation constants, and the complete quantifier/decoder conclusion. (source-ambiguity)

Selected references

• A father protocol for quantum broadcast channels, arXiv:quant-ph/0612155v4, https://arxiv.org/abs/quant-ph/0612155v4

This mission formalizes the question whether the group $\mathrm{IET}$ of interval exchange transformations is amenable, Question 1.6 of Juschenko, Matte Bon, Monod and de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, p. 4 (doi:10.1017/etds.2016.32), together with the landmark results of the literature on the question.

Motivation

An interval exchange transformation cuts the circle $\mathbf R/\mathbf Z$ into finitely many arcs and puts them back in a different order. These maps model the dynamics of polygonal billiards with rational angles, and since Katok–Stepin (1967) and Keane (1975) they have been a central object of ergodic theory. Under composition they form a group, $\mathrm{IET}$. Two questions about this group are open: whether it contains a non-abelian free subgroup (Katok's question), and whether it is amenable, that is, whether it carries a finitely additive, translation-invariant probability measure on all of its subsets. Amenability would answer Katok's question in the negative, since an amenable group has no non-abelian free subgroup.

Timeline.

• 1967: Katok and Stepin first consider exchanges of three or more intervals (JMMS, p. 4).
• 1975: Keane introduces interval exchange transformations systematically and the terminology (doi:10.1007/BF01236981).
• 2009: Novak shows that cyclic subgroups of $\mathrm{IET}$ are undistorted (doi:10.3934/jmd.2009.3.379).
• 2013: Dahmani, Fujiwara and Guirardel show that two generic interval exchange transformations do not generate a free group (doi:10.4171/GGD/209).
• 2013: Juschenko and Monod prove that the topological full group of every minimal Cantor system is amenable, which gives the first finitely generated infinite simple amenable groups (doi:10.4007/annals.2013.178.2.7). The technical core is the case $X = \mathbf Z$ of the lamplighter question for the wobbling group below (Juschenko–de la Salle, p. 2).
• 2013: de Cornulier's Bourbaki exposé records that “La question de la moyennabilité du groupe entier IET est ouverte” (p. 1064-04; published 2014, arXiv:2002.09342).
• 2013: Juschenko, Nekrashevych and de la Salle prove that recurrent actions are extensively amenable (arXiv 2013; published 2016, doi:10.1007/s00222-016-0664-6).
• 2013: Juschenko and de la Salle prove that the lamplighter action of the wobbling group of a recurrent metric space of bounded geometry, for instance $\mathbf Z$ or $\mathbf Z^2$, is amenable, and that it is not when the space contains a Lipschitz injective image of the binary tree; the case $\mathbf Z^d$, $d \ge 3$, is left open (arXiv 2013; published 2015, doi:10.36045/bbms/1432840864).
• 2015: Juschenko, Matte Bon, Monod and de la Salle introduce extensive amenability of group actions, show that a subgroup of $\mathrm{IET}$ is amenable if and only if its action on $\mathbf R/\mathbf Z$ is extensively amenable, prove that every subgroup of rational rank at most $2$ is amenable, and show that finitely supported random walks are Liouville in rank $1$ and are not in rank at least $3$ (arXiv 2015; published 2018, doi:10.1017/etds.2016.32).
• 2017: Dahmani, Fujiwara and Guirardel prove that every finitely generated torsion-free solvable subgroup of $\mathrm{IET}$ is virtually abelian (arXiv 2017; published 2020, doi:10.5802/afst.1641).
• 2018: Garban shows that the action of the wobbling group of a bounded degree graph is diffuse-extensively amenable if and only if the graph is recurrent, and conjectures that $W(\mathbf Z^d) \curvearrowright \mathbf Z^d$ is not extensively amenable for $d \ge 3$ (arXiv 2018; published 2020, doi:10.4171/GGD/567).
• 2026: Guelman and Liousse record (p. 2) that “there is no known example of non amenable or torsion-free non virtually abelian finitely generated iet-group” (arXiv:2601.23054). The question remains open as of 2026.

Setting

Write $\mathbf R/\mathbf Z$ for the circle (UnitAddCircle). A permutation $g$ of $\mathbf R/\mathbf Z$ is an interval exchange transformation (IntervalExchange.IsIntervalExchange g) when it is right-continuous, has finitely many points of discontinuity, and has finitely many angles $g(x) - x$. Equivalently, $g$ cuts the circle into finitely many half-open arcs and translates each of them. The group $\mathrm{IET}$ (IntervalExchange.IET) is the subgroup of permutations of $\mathbf R/\mathbf Z$ that they generate; a milestone states that it consists of the interval exchange transformations themselves. For a subgroup $G \le \mathrm{IET}$, the angle group $\Lambda(G)$ (angleGroup G) is the subgroup of $\mathbf R/\mathbf Z$ generated by all angles of elements of $G$, and the rational rank $\mathrm{rk}_{\mathbf Q}$ (rationalRank) of a subgroup of $\mathbf R/\mathbf Z$ is the supremum of the $d$ such that $\mathbf Z^d$ embeds in it. For a subgroup $\Lambda$ of $\mathbf R/\mathbf Z$, $\mathrm{IET}(\Lambda)$ (IETOf Λ) consists of the elements of $\mathrm{IET}$ all of whose angles lie in $\Lambda$.

A mean on a set $S$ is a function $m$ from the subsets of $S$ to $[0, \infty]$ with $m(\emptyset) = 0$, $m(A \cup B) = m(A) + m(B)$ for disjoint $A, B$, and $m(S) = 1$. A group $G$ is amenable (Garrido.IsAmenable G) when it carries a mean with $m(gA) = m(A)$ for all $g \in G$ and $A \subseteq G$. An action of $G$ on a set $X$ is amenable (IsAmenableAction G X) when $X$ carries a $G$-invariant mean, and extensively amenable (IsExtensivelyAmenable G X) when the finite subsets of $X$ carry a $G$-invariant mean that, for each finite $E_0 \subseteq X$, gives full weight to the finite sets containing $E_0$.

The milestones use further notions, defined precisely in the definitions item and in their own statements:

• A finitely supported probability measure $\mu$ on $G$ drives the left random walk $g_n = h_n \cdots h_1$; the inverted orbit of $x_0 \in X$ is $O_n = \{x_0, g_1^{-1}x_0, \dots, g_n^{-1}x_0\}$. The action is recurrent (IsRecurrentAction) when for every symmetric such $\mu$ and every $x_0$, the induced walk $g_n x_0$ returns to $x_0$ with probability $1$.
• For a functor $F$ from finite sets with injections to amenable groups, $F(X)$ (extend F X) is its extension to an arbitrary set $X$ by direct limits, and an action of $G$ on $X$ gives the semidirect product $F(X) \rtimes G$ (FunctorProduct F G X) acting on $F(X)$. The lamplighter case is $F(X) = (\mathbf Z/2\mathbf Z)^{(X)}$ (Lamplighter G X).
• The wobbling group $W(X)$ (wobbling X) of a metric space $X$ consists of the permutations $g$ of $X$ with $\sup_x d(x, gx) < \infty$.

Formalization targets

Goal

$$\mathrm{IsAmenable}(\mathrm{IET}).$$

The question is open. A proof settles it positively and, through von Neumann's theorem, answers Katok's question in the negative; a disproof shows that $\mathrm{IET}$ is not amenable.

Landmarks

The milestones are results from the literature, stated as their sources state them. From Juschenko–Matte Bon–Monod–de la Salle: $\mathrm{IET}$ is a group (p. 4); Lemmas 2.1 and 2.2 on extensive amenability; Theorem 1.3 and Corollary 1.4, the functorial criterion; Proposition 5.3, that a subgroup of $\mathrm{IET}$ is amenable if and only if its action on $\mathbf R/\mathbf Z$ is extensively amenable; Proposition 4.1 and Lemma 4.3, the inverted-orbit reformulations; Theorem 4.2, recurrence implies extensive amenability; Lemma 5.2 and Theorems 5.1 and 1.9, amenability in rational rank at most $2$; and Theorem 1.10, the Liouville dichotomy, with the steps of its proof: Lemma 5.10, Proposition 5.11 with Lemma 5.13 (realizing $\mathrm{IET}(\Lambda; \Sigma)$ as the topological full group of a minimal subshift of polynomial complexity), and Matte Bon's theorem for virtually cyclic groups. The external results these proofs cite are milestones too: Kesten's criterion for a graph (Woess, Theorem 10.6), Lyons–Peres Theorem 2.17 on rough embeddings, Pólya's theorem (already proved on the platform as MarkovMixing.polya_recurrence), the Baldi–Lohoué–Peyrière comparison lemma, and Matte Bon's Theorem 1.2 on topological full groups of subshifts of slow complexity. From Juschenko–de la Salle: Theorem 1.4 on the wobbling group, with coarse embeddings defined by non-decreasing control functions.

Two further open statements

Garban's question, whether $W(\mathbf Z^d) \curvearrowright \mathbf Z^d$ is extensively amenable for every $d$, and Question 1.11 of Juschenko–Matte Bon–Monod–de la Salle, whether a polynomially growing Schreier graph forces extensive amenability, are stated as open milestones. Each comes with a milestone stating that a positive answer implies the goal.

Significance

The result. A proof would make $\mathrm{IET}$ a natural amenable group containing, by Juschenko–Monod and Juschenko–Matte Bon–Monod–de la Salle, finitely generated infinite simple amenable groups, and would answer Katok's question. A disproof would give the first non-amenable finitely generated group of interval exchange transformations; by Theorem 1.9 it would have rational rank at least $3$.

Formalizing it. The definitions of extensive amenability, of the functorial semidirect products $F(X) \rtimes G$, of inverted orbits and recurrent actions, and of wobbling groups are reusable beyond this mission, as are the external probabilistic results (Kesten's criterion, rough embeddings and recurrence). Pólya's theorem is already formalized and proved on the platform (MarkovMixing.polya_recurrence). None of the other landmarks is formalized.

Difficulty

Every known amenability proof for subgroups of $\mathrm{IET}$ passes through Proposition 5.3 and then needs extensive amenability of the action on the circle. The available criterion for extensive amenability is recurrence of the Schreier graphs, which embed into lattices $\mathbf Z^d$ with $d$ the rational rank; for $d \ge 3$ these graphs can be transient, so recurrence is unavailable. Garban's theorem shows that the natural strengthening of extensive amenability fails for all transient wobbling actions, and Theorem 1.10 shows that the Liouville route fails in rank at least $3$.

Formalization scope

$\mathbf R/\mathbf Z$ is UnitAddCircle, and permutations act on it by evaluation. $\mathrm{IET}$ is defined as the subgroup generated by the interval exchange transformations, so that its group structure needs no proof inside the definitions; a milestone states that nothing else lies in it. The source's precise definition (“a right-continuous permutation $g$ of $\mathbf R/\mathbf Z$ such that the set $\{gx - x, x \in \mathbf R/\mathbf Z\}$, called the set of angles of $g$, is finite”) is read together with its opening phrase, “cutting this circle into finitely many intervals”, so the definition also requires finitely many points of discontinuity: without that requirement a right-continuous permutation with two angles can have infinitely many discontinuities, and the cocycle of Proposition 5.3 would not be finitely supported. Means take values in $[0, \infty]$ and are normalized to total mass $1$. Random walks have finitely supported step distributions $\mu : G \to_0 \mathbf R$ where the sources say “finitely supported”, and probabilities of events of a walk are finite sums over the step sequences. Recurrence of a Markov chain is return to the starting point with probability $1$, expressed through first-return probabilities. Functors $I \to \mathrm{Amen}$ are Mathlib functors from the wide subcategory of FintypeCat on the injective maps to GrpCat with amenable values, extended to a set $X$ by the filtered colimit over its finite subsets.

The goal admits no trivializing reading: $\mathrm{IET}$ contains the irrational rotations and the non-rotation exchanges, and Garrido.IsAmenable is the standard notion. The external milestones (Kesten, Lyons–Peres, Baldi–Lohoué–Peyrière) are cited results, stated in the form the sources apply; proofs of them are welcome contributions in their own right.

Selected references

• K. Juschenko, N. Matte Bon, N. Monod and M. de la Salle, Extensive amenability and an application to interval exchanges, Ergodic Theory Dynam. Systems 38 (2018) 195–219, doi:10.1017/etds.2016.32, arXiv:1503.04977.
• K. Juschenko and M. de la Salle, Invariant means for the wobbling group, Bull. Belg. Math. Soc. Simon Stevin 22 (2015) 281–290, doi:10.36045/bbms/1432840864.
• K. Juschenko, V. Nekrashevych and M. de la Salle, Extensions of amenable groups by recurrent groupoids, Invent. Math. 206 (2016) 837–867, doi:10.1007/s00222-016-0664-6.
• K. Juschenko and N. Monod, Cantor systems, piecewise translations and simple amenable groups, Ann. of Math. 178 (2013) 775–787, doi:10.4007/annals.2013.178.2.7.
• C. Garban, Inverted orbits of exclusion processes, diffuse-extensive-amenability, and (non-?)amenability of the interval exchanges, Groups Geom. Dyn. 14 (2020) 871–897, doi:10.4171/GGD/567.
• Y. de Cornulier, Groupes pleins-topologiques [d'après Matui, Juschenko, Monod, ...], Séminaire Bourbaki, exposé 1064, Astérisque 361 (2014) 183–223, arXiv:2002.09342.
• F. Dahmani, K. Fujiwara and V. Guirardel, Free groups of interval exchange transformations are rare, Groups Geom. Dyn. 7 (2013) 883–910, doi:10.4171/GGD/209.
• F. Dahmani, K. Fujiwara and V. Guirardel, Solvable groups of interval exchange transformations, Ann. Fac. Sci. Toulouse Math. 29 (2020) 595–618, doi:10.5802/afst.1641.
• M. Keane, Interval exchange transformations, Math. Z. 141 (1975) 25–31, doi:10.1007/BF01236981.
• C. F. Novak, Discontinuity-growth of interval-exchange maps, J. Mod. Dyn. 3 (2009) 379–405, doi:10.3934/jmd.2009.3.379.
• R. Lyons and Y. Peres, Probability on Trees and Networks, Cambridge University Press, 2016, doi:10.1017/9781316672815.
• W. Woess, Random Walks on Infinite Graphs and Groups, Cambridge University Press, 2000, doi:10.1017/CBO9780511470967.
• N. Matte Bon, Subshifts with slow complexity and simple groups with the Liouville property, Geom. Funct. Anal. 24 (2014) 1637–1659, doi:10.1007/s00039-014-0293-4.
• P. Baldi, N. Lohoué and J. Peyrière, Sur la classification des groupes récurrents, C. R. Acad. Sci. Paris Sér. A–B 285 (1977) A1103–A1104 (no DOI).
• N. Guelman and I. Liousse, Some elementary amenable subgroups of interval exchange transformations, arXiv:2601.23054 (2026).

Motivation

The problem of converting noisy quantum correlations between two parties into noiseless classical ones using a limited amount of one-way classical communication is addressed. A single-letter formula for the optimal trade-off between the extracted common randomness and classical communication rate is obtained for the special case of classical-quantum correlations. The resulting curve is intimately related to the quantum compression with classical side information trade-off curve $Q^*(R)$ of Hayden, Jozsa and Winter. For a general initial state we obtain a similar result, with a single-letter formula, when we impose a tensor product restriction on the measurements performed by the sender; without this restriction the trade-off is given by the regularization of this function. Of particular interest is a quantity we call ``distillable common randomness'' of a state: the maximum overhead of the common randomness over the one-way classical communication if the latter is unbounded. It is an operational measure of (total) correlation in a quantum state. For classical-quantum correlations it is given by the Holevo mutual information of its associated ensemble, for pure states it is the entropy of entanglement. In general, it is given by an optimization problem over measurements and regularization; for the case of separable states we show that this can be single-letterized.

This mission is the statement-level formalization of Distilling common randomness from bipartite quantum states (arXiv:quant-ph/0304196v2). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

22 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Regularization of the one-way common-randomness trade-off (Abstract and §3: regularized one-way common-randomness trade-off, PDF p. 15). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Deferred results

1 results of the paper are not stated yet, because the library lacks an interface they need:

• Appendix (30): A valid conditional typical-projector extension with a restriction controlling all local subblock lengths and conditional frequency tolerances. (source-ambiguity)

Selected references

• Distilling common randomness from bipartite quantum states, arXiv:quant-ph/0304196v2, https://arxiv.org/abs/quant-ph/0304196v2

Motivation

Can entangled noise erase entanglement more efficiently than separable noise? Standard robustness restricts the added noise to separable states; generalized robustness allows any state. We prove that the two costs coincide for every two-qubit state and give an explicit full-rank qubit--qutrit state with a strict gap. Positivity under partial transpose (PPT) characterizes separability in both dimensions, so the boundary is not caused by a failure of the PPT criterion. Instead, product-vector geometry permits a rank-one bridge between the two-qubit dual optimizations and supplies a two-dimensional completely entangled subspace for the qubit--qutrit separation. Local isometric embeddings complete the finite-dimensional bipartite classification, also for any fixed multipartite cut. Combined with known three-qubit separation, the result classifies universal equality relative to full separability in all finite multipartite systems. △ Less

This mission is the statement-level formalization of The Minimal Dimension of Entangled-Noise Advantage (arXiv:2609.28367v1). Every numbered result of the paper was scanned. The results stated here are open sorry goals, ready for solvers to prove.

What is formalized

45 statements of the paper are in Lean 4 (Mathlib 0df444a). The goal theorem is Main-text Theorem 1; seed announced in abstract (Main-text Theorem 1; seed announced in abstract, PDF p. 1). The milestones are the other numbered results, in the paper's order, each quoting the paper.

The paper's own objects are the definition item of this mission. Objects shared across papers come from the prove2quantum library and from earlier papers' missions, listed as references.

Provenance: prove2quantum's pipeline drafted each statement (gpt-6.1-sol on Stanford's Sherlock cluster). A blind read-back, written without seeing the paper, is attached to every item. An independent moderator compared each statement against the paper and passed the whole paper without edits.

Selected references

• The Minimal Dimension of Entangled-Noise Advantage, arXiv:2609.28367v1, https://arxiv.org/abs/2609.28367v1

Opportunistic returns and restocking fees

Generous return policies raise demand, but they also invite opportunistic returns: customers who buy a product intending to use it briefly and return it for a refund. Retail-industry surveys put the share of such "wardrobing" or renting customers near a tenth of all customers, and retailers answer with restocking fees, return windows, or analytics services that flag suspected renters. Altug, Aydinliyim and Jain (SSRN 3283334; Management Science, 2021, doi:10.1287/mnsc.2020.3777) compare three ways a retailer can set prices and refunds in this situation. Their model extends Su's newsvendor model of consumer returns (Su 2009), in which every customer is an honest returner who returns only after learning that the product does not suit him, and the optimal refund equals the salvage value. The question is whether a retailer who cannot tell renters from honest customers can still do as well as one who can.

Setting

A retailer stocks $Q$ units at unit cost $c$, sells at price $p$, refunds $r$ per returned unit, and salvages leftover units at $s < c$. Aggregate demand $D$ is random. A fraction $X \in (0,1)$ of customers are renters, the rest are honest returners.

• An honest returner has a long-term valuation $u_L$ with distribution $G_L$ on $[0, V_L]$. He buys if $\mathbb E\max\{u_L, r\} \ge p$, learns $u_L$, and returns the product iff $u_L < r$; so a fraction $G_L(r)$ of honest buyers return.
• A renter has a short-term valuation $u_S$ with distribution $G_S$ on $[0, V_S]$. He buys and returns iff $u_S \ge p - r$, the rental fee; so a fraction $1 - G_S(p-r)$ of renters transact.

The fraction of customers who transact is $N(p, r) = 1 - XG_S(p - r)$. A decision with marginal net revenue $M$ earns

$$M\,\mathbb E\min\Bigl\{\frac{Q}{N}, D\Bigr\} - (c - s)Q.$$

The three proposals are:

1. Uniform refunds, program (3): one pair $(p, r)$ for everybody, with $M^u(p,r) = (p-r)(1 - XG_S(p-r)) + (r-s)(1-X)(1-G_L(r))$ and $p \le \mathbb E\max\{u_L, r\}$. The main-body results concerning $r^u$ treat the case where this inequality binds at the optimum.
2. Targeted refunds, program (9): the retailer identifies each customer's type and gives renters refund $r_R$ and honest returners refund $r_H$ at a common price $p$, with $M^t(p, r_R, r_H) = X(p - r_R)(1 - G_S(p - r_R)) + (1-X)\bigl((p-s) - (r_H - s)G_L(r_H)\bigr)$, $0 \le p - r_R \le V_S$ and $p = \mathbb E\max\{u_L, r_H\}$.
3. Menu of refunds, program (11): the retailer offers two pairs $(p_H, r_H)$, $(p_R, r_R)$ and lets customers self-select, subject to the honest returners preferring their pair with nonnegative surplus, $\mathbb E\max\{u_L, r_H\} - p_H \ge \max\{\mathbb E\max\{u_L, r_R\} - p_R, 0\}$, and the renters preferring theirs, $p_R - r_R \le \min\{p_H - r_H, V_S\}$.

Write $\Pi^u, \Pi^t, \Pi^m$ for the three optimal profits and $r^u$ for an optimal uniform refund. Without renters the optimal refund is the benchmark $r^b = s$.

Formalization targets

Goal: Proposition 6, corrected

$$\Pi^u \le \Pi^m \le \Pi^t, \qquad \bigl(\Pi^t > \Pi^m = \Pi^u \iff r^u < s\bigr), \qquad r^u > s \Rightarrow \Pi^t = \Pi^m > \Pi^u, \qquad r^u = s \Rightarrow \Pi^t = \Pi^m,$$

together with the existence of an optimal uniform decision. Hence $\Pi^m = \Pi^t \iff r^u \ge s$. This is a corrected Proposition 6 (p. 17). As printed, part (b) is an equivalence and part (c) says $\Pi^t = \Pi^m = \Pi^u$ when $r^u = s$. That fails: in the setting of the paper's Figure 1 with $G_L = U[0,100]$, $G_S = U[0,20]$ and $s = 30$, the uniform optimum has $r^u = s$ and prices renters out, while targeted refunds earn strictly more, and so does the menu.

Milestones

In attack order: the closed form (5b) of the binding price; the first two claims of Lemma 1; the benchmark refund $r^b = s$ as a strict maximizer of the honest margin; the upper bounds $\Pi^u, \Pi^m \le \Pi^t$; Proposition 4's (10b)–(10c); the strict gain $\Pi^u < \Pi^t$ when $r^u \ne s$; Proposition 4's last sentence, $r^t_R \ge s \iff r^u \ge s$; the §7.1 claim that $r^t_R \ge s$ gives $\Pi^m = \Pi^t$; and Proposition 5's price-refund choice in (12b)–(12c), with its consequence for optimal profit.

Significance

The result says when screening by a price-refund menu is as good as identifying customers. A retailer that can segment customers only by paying an analytics firm learns that the payment buys nothing exactly when its optimal uniform refund is at least the salvage value, and that otherwise the menu degenerates to a single uniform policy. Figure 1 of the paper maps the regions in $(V_S, s)$ where each case occurs.

The proofs of Propositions 1 to 11 sit in an electronic companion that is not part of the working paper, and the printed Proposition 6 is false at the boundary $r^u = s$. A machine-checked proof therefore settles the corrected statement independently of the missing appendix. No part of the paper has been formalized before.

Difficulty

Each program is a joint optimization over stock, price and refunds, with the stock entering through a newsvendor term whose coefficient depends on the refunds. The comparisons are between suprema of different programs, not between first-order conditions. The obvious approach, comparing the closed forms of Propositions 1, 4 and 5, does not work: Proposition 1 rests on the hypothesis that $xG_S'(x)$ is decreasing, which no distribution with a density on $[0, V_S]$ satisfies, and its threshold $V_S^{LB}$ is only asserted to exist. The case $r^u < s$ is the hard one: it requires showing that the menu's incentive constraints force it back to a uniform policy, which depends on the shape of the targeted profit in the rental fee and hence on the IGFR assumption.

Formalization scope

• Everything is real-valued. Valuation laws are probability measures with support exactly $[0, V_L]$, $[0, V_S]$, a regular density and the IGFR property (LariviereIGFR.Char.IsIGFR). Demand is a probability law on $(0, \infty)$ with finite mean, and $\mathbb E\min\{Q, D\}$ is SupplyChainTheory.expSales.
• Tie rules follow the page (keep iff $u_L \ge r$, rent iff $u_S \ge p - r$).
• The uniform program (3) keeps its constraint $\mathbb E\max\{u_L, r\} - p \ge 0$, and the statements about the optimal uniform refund $r^u$ (Proposition 4's last sentence, Propositions 5 and 6) are made in the case the paper's main body treats (p. 11): that constraint binds at every optimal uniform decision. Program (3) does not carry its cap $p - r \le V_S$: the paper's own optimum can have a rental fee above $V_S$.
• Refunds are nonnegative in all programs, and $r \le p$ for both menu pairs.
• Hypotheses added to the page: $0 < s$ (at $s = 0$ Proposition 6 fails), $c < \mathbb E\max\{u_L, s\}$ (the page's $p > c$ at the benchmark price), and positive demand with finite mean.
• $\Pi^u, \Pi^t, \Pi^m$ are suprema over each program's feasible set; their boundedness is a milestone. $\Pi^m$ is never defined by Proposition 5's case split, and $r^u$ is an arbitrary optimal uniform refund, not a closed form; a formalization that defines either by the case split is trivial and is ruled out.
• Not formalized: the first-order conditions (5a), (5c), (10a), (10d), (12a); Proposition 1 and Lemma 1's third claim (false); Propositions 2, 3, 7–11.
• Reusable infrastructure: the expected-maximum identity (5b), the strict optimality of $r = s$ for honest returners, and attainment of optima for newsvendor programs with continuous valuation laws.

Selected references

• M. S. Altug, T. Aydinliyim, A. Jain, Managing Opportunistic Consumer Returns in Retail Operations, SSRN working paper 3283334 (revision of June 26, 2020); Management Science, 2021. https://ssrn.com/abstract=3283334, https://doi.org/10.1287/mnsc.2020.3777
• X. Su, Consumer Returns Policies and Supply Chain Performance, Manufacturing & Service Operations Management 11(4), 595–612, 2009. https://doi.org/10.1287/msom.1080.0240
• M. A. Lariviere, A Note on Probability Distributions with Increasing Generalized Failure Rates, Operations Research 54(3), 2006. https://doi.org/10.1287/opre.1060.0282

Motivation

Customer abandonment, or reneging, is a basic feature of service systems: call centres, emergency departments and online platforms all lose customers who give up waiting. The number of reneging customers is a natural performance measure, and in many-server and single-server models alike it is the quantity managers monitor and are penalised for. Typical (law-of-large-numbers) behaviour of reneging is well understood; the question here is how unlikely atypical amounts of reneging are, over long horizons.

R. Atar, A. Budhiraja, P. Dupuis and R. Wu (arXiv:1903.06870; Mathematics of Operations Research, 2022) answer this for the single-server queue with exponential patience, in the many-arrivals scaling. They prove a sample-path large deviation principle for the pair (queue length, cumulative reneging) and then solve the associated long-horizon variational problem in closed form. The answer has a counter-intuitive feature, which the authors call the reneging paradox: the exponential decay rate of the probability of observing reneging at an atypical long-run rate $\gamma$ does not depend on the reneging rate $\theta$. Customers who are very patient and customers who are very impatient produce, over long horizons, the same large-deviation cost for the same atypical reneging rate.

Setting

Fix rates $\lambda,\mu,\theta>0$ (arrival, service, per-customer reneging), an initial queue length $x_0\ge0$ and a horizon $T>0$. Throughout the mission $\lambda\ge\mu$ (the paper's standing assumption from §2.2 on). The Skorohod map on $[0,T]$ is

$$\Gamma(\psi)(t)=\psi(t)-\inf_{0\le s\le t}[\psi(s)\wedge0],$$

and the local cost is $\ell(x)=x\log x-x+1$ for $x\ge0$.

A path is a pair $(\xi,\zeta)$ of continuous functions $[0,T]\to\mathbb R_+$; $\xi$ is the queue length and $\zeta$ the cumulative number of reneged customers, both on the fluid scale. A control is a triple $\varphi=(\varphi_1,\varphi_2,\varphi_3)$ of measurable maps $[0,T]\to\mathbb R_+$ that perturb the arrival, service and reneging rates; it is admissible for $(\xi,\zeta)$, written $\varphi\in\mathcal U(\xi,\zeta)$, if for all $t\in[0,T]$

$$\xi(t)=\Gamma\Big(x_0+\lambda\!\int_0^{\cdot}\!\varphi_1-\mu\!\int_0^{\cdot}\!\varphi_2-\theta\!\int_0^{\cdot}\!\varphi_3\,\xi\Big)(t),\qquad\zeta(t)=\theta\int_0^t\varphi_3(s)\xi(s)\,ds .$$

The rate function is

$$I_T(\xi,\zeta)=\inf_{\varphi\in\mathcal U(\xi,\zeta)}\Big\{\lambda\!\int_0^T\!\ell(\varphi_1)+\mu\!\int_0^T\!\ell(\varphi_2)+\theta\!\int_0^T\!\xi\,\ell(\varphi_3)\Big\},$$

equal to $\infty$ when no control is admissible. The cost of seeing $\gamma T$ reneged customers by time $T$ is

$$I^*_{\gamma,T}=\inf\{I_T(\xi,\zeta):\zeta(T)=\gamma T\},$$

with the one-sided versions $I_{\gamma,T}$ (constraint $\zeta(T)\ge\gamma T$) and $\tilde I_{\gamma,T}$ (constraint $\zeta(T)\le\gamma T$). Finally

$$z_\gamma=\frac{\sqrt{\gamma^2+4\lambda\mu}-\gamma}{2\mu},\qquad C(\gamma)=\lambda\big(1-z_\gamma^{-1}\big)+\mu(1-z_\gamma)-\gamma\log z_\gamma .$$

Formalization targets

Goal: Theorem 2.3

$$\lim_{T\to\infty}\frac{I^*_{\gamma,T}}{T}=C(\gamma)\ (\gamma\ge0),\qquad\lim_{T\to\infty}\frac{I_{\gamma,T}}{T}=C(\gamma)\ (\gamma\ge\lambda-\mu),\qquad\lim_{T\to\infty}\frac{\tilde I_{\gamma,T}}{T}=C(\gamma)\ (0\le\gamma\le\lambda-\mu).$$

The limit depends on $\lambda,\mu,\gamma$ only; $\theta$ and $x_0$ appear in the hypotheses and inside $I_T$, never in $C$.

Milestones

The milestones follow the paper's proof, in order:

1. the reduction of $I_T$ to the class $\mathcal C_T$ of absolutely continuous paths with $\xi(0)=x_0$, $\zeta(0)=0$, $\zeta$ nondecreasing and $\zeta'=0$ a.e. on $\{\xi=0\}$ (§4, p. 18);
2. the representation $I_T(\xi,\zeta)=\int_0^TL(\xi,\xi',\zeta')\,ds$ with an explicit local rate $L$ (Lemma 4.1);
3. convexity of $L$ and of $I_T$ on $\mathcal C_T$ (Lemma 4.4);
4. existence and uniqueness of the constant $A$ solving the transcendental equation (5.9), and its asymptotics (Lemma 5.2);
5. the explicit candidate $(\bar\xi,\bar\zeta)$ of Construction 5.3: its terminal value $\bar\zeta(T)=\gamma T$ (Lemma 5.4), positivity and membership in $\mathcal C_T$ (Lemma 5.5), its cost and $I_T(\bar\xi,\bar\zeta)/T\to C(\gamma)$ (Lemma 5.6), and its optimality for $x_0>0$ (Lemma 5.7);
6. convexity of $\gamma\mapsto I^*_{\gamma,T}$ and its zero at the law-of-large-numbers rate $\gamma^*_T$ (Lemma 6.1);
7. (6.1) and the elementary properties of $C$; the upper bound $\limsup I^*_{\gamma,T}/T\le C(\gamma)$ (Proposition 6.2) and the lower bounds for $\gamma>0$ (Proposition 6.3) and $\gamma=0$ (Proposition 6.4).

Significance

The theorem gives the exact long-horizon decay rate of the probability of atypical reneging in the $M/M/1+M$ queue, in closed form, together with the explicit optimal path for $x_0>0$. It shows that the patience parameter, which governs typical reneging, is invisible in the long-run large-deviation cost of atypical reneging. The paper treats the many-server analogue $M/M/n+M$ in its §7; that part is not in this mission.

The result is proved in the paper. None of it is formalized: Mathlib has no sample-path large deviations and no Skorohod problem, and the platform has no rate function for a reflected, state-dependent jump process. This mission formalizes the deterministic, variational half (§§4–6) of the paper; the probabilistic LDP itself (Theorem 2.1, proved in §3) is not a target.

Difficulty

The variational problem has a state-dependent cost ($\xi\,\ell(\varphi_3)$) and a reflection constraint, so the obvious approach of guessing a constant-rate tilt and checking it fails: the optimal path is not linear, its constants solve the transcendental equation (5.9), and the minimizer must be shown to stay in the interior $\{\xi>0\}$ for large $T$, which happens only beyond a horizon $T_0$ that genuinely grows with the data. The case $x_0=0$, where the explicit candidate is not shown to be optimal, and $\gamma=0$, where the reflection at zero is active, need separate arguments (Propositions 6.3 and 6.4). The final passage from $I^*$ to the one-sided problems relies on the shape of $\gamma\mapsto I^*_{\gamma,T}$ (Lemma 6.1).

Formalization scope

All declarations live in the namespace RenegingLD.MM1, in two definition files (Model for §2, Variational for §§4–6) and one theorem file per statement. The conventions are:

• lam, mu stand for $\lambda,\mu$. The standing assumptions $\lambda,\mu,\theta>0$, $\mu\le\lambda$, $x_0\ge0$ and $T>0$ are explicit hypotheses of every statement that needs them.
• Paths and controls are functions $\mathbb R\to\mathbb R$ of which only $[0,T]$ is used; a path is required to be continuous and nonnegative on $[0,T]$. Infima over the paper's $\mathcal D([0,T]:\mathbb R^2_+)$ are taken over all functions, which agrees because $I_T=\infty$ off continuous paths.
• Admissible controls are additionally required to make $\varphi_1$, $\varphi_2$ and $\varphi_3\xi$ integrable on $[0,T]$, which the page's integrals presuppose.
• $I_T$, $I^*$, $I$, $\tilde I$ and $L$ take values in $[0,\infty]$. The cost is a lower Lebesgue integral of nonnegative functions. Limits, $\limsup$ and $\liminf$ of $I/T$ are taken in $[0,\infty]$, against $C(\gamma)$ embedded there; $C(\gamma)\ge0$, so nothing is clamped.
• Derivatives are Lean's deriv, the a.e. derivative on $\mathcal C_T$.
• The root of (5.9) is never chosen by a choice function: each statement about the candidate quantifies over every $A<e^{-\theta T}$ solving (5.9), with $B=1/(1-Ae^{\theta T})$.
• Lemma 5.6 uses the closed form of display (5.15). The printed lemma has $\bar\zeta(T)$ where (5.15) has $\bar\xi(T)$, and a numerical check confirms (5.15).

A trivializing formalization is ruled out: the costs are lower integrals, so a non-integrable control cannot have cost zero; $I_T$ is $\infty$ off continuous paths; and the goal quantifies over every path through $I^*$, $I$ and $\tilde I$, not over the explicit candidate, for every $x_0\ge0$ and every $\gamma$ in the paper's ranges.

A complete development needs absolutely continuous functions and the fundamental theorem of calculus for them (present in Mathlib), the one-dimensional Skorohod problem, convexity of perspective functions, and a first-variation argument for convex integral functionals. The Skorohod-map and perspective-convexity lemmas are reusable beyond this mission. Contributions of proofs of any milestone, including partial results such as the $\lambda=\mu$ or $x_0>0$ cases of the goal, are welcome.

Selected references

• R. Atar, A. Budhiraja, P. Dupuis, R. Wu, Large deviations for the single server queue and the reneging paradox, Mathematics of Operations Research, 2022; preprint arXiv:1903.06870v2 (2020). https://arxiv.org/abs/1903.06870
• A. Dembo, O. Zeitouni, Large Deviations Techniques and Applications, 2nd ed., Springer, 1998. https://doi.org/10.1007/978-1-4612-5320-4
• P. Dupuis, R. S. Ellis, A Weak Convergence Approach to the Theory of Large Deviations, Wiley, 1997. https://doi.org/10.1002/9781118165904

Motivation

In a communication network, file transfers ("flows") share the capacity of the links on their routes, and the bandwidth-sharing policy decides how much rate each flow receives. The connection-level model of Massoulié and Roberts (2000) treats flows as customers that arrive at random, carry a random amount of data, and leave once it is transferred. Under weighted proportional fairness (Kelly 1997; Mo and Walrand 2000), the rates maximise $\sum_r\kappa_rn_r\log x_r$ subject to the link capacities. Its delay performance in steady state, measured by the expected numbers of flows on the routes, is the quantity a network operator cares about.

Most heavy-traffic results for this model are diffusion approximations: Kang, Kelly, Lee and Williams (2009) under a local-traffic assumption, Ye and Yao (2012) under a full-rank routing matrix, with interchange of limits by Shah, Tsitsiklis and Zhong (2014) and Ye and Yao (2016); all assume exponential file sizes. Vlasiou, Zhang and Zwart (2014) obtained the diffusion limit for phase-type sizes. Whether the stationary flow counts depend on the file-size distribution beyond its mean (insensitivity) is the central practical question, since real file sizes are far from exponential. Wang, Maguluri, Srikant and Ying (arXiv:1808.02120, 2021; Math. Oper. Res. 2022) answer it in heavy traffic with explicit bounds, using the Lyapunov drift method instead of diffusion limits.

Setting

There are links $\ell=1,\dots,L$ with capacities $C_\ell>0$ and routes $r=1,\dots,R$; the routing matrix $H=(h_{\ell r})$ has $h_{\ell r}=1$ if link $\ell$ is on route $r$ and $0$ otherwise, has full row rank, and every route uses some link. Flows arrive on route $r$ as a Poisson process of rate $\lambda_r$. Their sizes are i.i.d. with a phase-type law in the class $\mathcal D$: the absorption time of a Markov chain whose transient phases form Erlang blocks with pairwise distinct rates $\mu^{(b)}_r$, started with positive probability in the first phase of every block. With subgenerator $S_r$ and initial law $\pi_r$, the mean size is $1/\mu_r=\pi_r(-S_r)^{-1}\mathbf 1$ and the route load is $\rho_r=\lambda_r/\mu_r$. The class $\mathcal D$ is dense in the distributions on $[0,\infty)$.

Given the numbers $n_r$ of flows on the routes, the weighted proportionally fair allocation with weights $\kappa_r>0$ gives each flow on route $r$ the rate $x_r$ solving

$$\max\ \sum_r\kappa_rn_r\log x_r\quad\text{s.t.}\quad\sum_{r:\ell\in r}n_rx_r\le C_\ell\ \ \forall\ell,\quad x_r=0\text{ if }n_r=0 .$$

The state $\mathbf n=(n_{r,k})$ counts the flows of route $r$ in phase $k$; it is a continuous-time Markov chain: arrivals into phase $k$ at rate $\lambda_r\pi_{r,k}$, phase changes $k_1\to k_2$ at rate $n_{r,k_1}x_r(S_r)_{k_1,k_2}$, and completions from phase $k$ at rate $n_{r,k}x_r\sum_{k'}(-S_r)_{k,k'}$.

Heavy traffic. Fix $\boldsymbol\lambda^{(0)}>0$ on the boundary of the capacity region: $\sum_{r:\ell\in r}\rho^{(0)}_r\le C_\ell$ for all links, with equality exactly on the nonempty set $\mathcal L_s$ of critically loaded links, $L_s=|\mathcal L_s|$. The $\epsilon$-th system has arrival rates $\boldsymbol\lambda^{(\epsilon)}=(1-\epsilon)\boldsymbol\lambda^{(0)}$, $0<\epsilon<1$, and $\overline{\mathbf N}^{(\epsilon)}$ denotes a random vector distributed as its stationary distribution, with route totals $\overline N^{(\epsilon)}_r$.

Formalization targets

Goal: Theorem 4 (p. 25)

$$\frac{L_s\cdot\min_r\kappa_r}{\epsilon}+o\Big(\frac1\epsilon\Big)\ \le\ \mathbb E\Big[\sum_r\kappa_r\overline N^{(\epsilon)}_r\Big]\ \le\ \frac{L_s\cdot\max_r\kappa_r}{\epsilon}+o\Big(\frac1\epsilon\Big)\qquad(\epsilon\to0^+).$$

The leading constants depend only on the number of critical links and the weights, not on the file-size laws in $\mathcal D$.

Milestones

The proof is organised around a new inner product $\langle\mathbf y,\mathbf z\rangle=\mathbf y^TM\mathbf z$ on the phase-level state space (67). In attack order:

• (5), p. 6: the allocation exists, is unique, and has Lagrange multipliers.
• Lemma 11, p. 39: $M$ is well defined and positive definite. Lemmas 5–6, p. 27: two matrix properties of $M_r$ and $S_r$.
• (P1') and (P2'), p. 26: the two properties of the inner product that replace those of the exponential case.
• Lemma 10, p. 37: tail and moment bounds from drift for continuous-time chains.
• Lemma 7, p. 27: drift of $\|\mathbf n\|$, positive recurrence, exponential tail of the weighted flow count.
• Lemma 8, pp. 27–28, and Theorem 3, p. 25: state-space collapse, $\mathbb E[\|\overline{\mathbf N}^{(\epsilon)}_\perp\|^m]=O(\epsilon^{-m/2})$ for the distance to an $L_s$-dimensional cone.
• (80), p. 30; Lemma 9, p. 31; $\mathbb E[U_\ell]=\epsilon C_\ell$, p. 32; (86), p. 33: the three terms of the steady-state drift identity that assemble Theorem 4.

Significance

The result. The bound is linear in the number of critical links, not routes, and holds without the local-traffic assumption. With equal weights the two sides coincide and give the exact heavy-traffic limit $\epsilon\,\mathbb E[\sum_r\overline N_r]\to L_s$ for every file-size law in $\mathcal D$: proportional fairness is heavy-traffic insensitive. As a by-product, state-space collapse yields the interchange of limits for the diffusion approximation of Vlasiou, Zhang and Zwart (Theorem 5 of the paper, not part of this mission).

Formalizing it. The paper's results are proved on paper; no part of this argument is machine-checked. A formalization yields reusable pieces beyond this paper: the continuous-time Bertsimas–Gamarnik–Tsitsiklis tail bound (Lemma 10), steady-state "zero expected drift" arguments for countable-state chains, and the matrix analysis of phase-type laws (Lemmas 5, 6, 11). The paper's own proof of Lemma 6 contains an incorrect step (a hazard-rate claim that fails for Erlang blocks), so a checked proof of that lemma is itself a contribution.

Difficulty

The drift method needs a Lyapunov function whose drift is negative along the directions the process actually moves. For exponential sizes the diagonal inner product of (9) suffices. With phase-type sizes the natural Euclidean or diagonal inner products fail: the rotation by $-S^T$ produced by phase changes can make $\langle\mathbf b^{(\ell)}-\widehat{\mathbf b}^{(\ell)},(-S^T)(\boldsymbol\rho^{(0)}-\mathbf n\mathbf x)\rangle$ negative, so (P2') breaks. The integral construction (67) of $M$ is what restores it, and checking that $M$ is positive definite requires a controllability (PBH) argument. On the probabilistic side, every step "in steady state the expected drift is zero" requires integrability of an unbounded Lyapunov function under the stationary law of a countable-state chain, which must first be established from the tail bounds; Mathlib has no ready theory for this.

Formalization scope

All objects are in the namespace HTInsensBW.PhaseType. A class-$\mathcal D$ law is a structure (PhaseTypeD) with blocks, lengths, distinct rates and an initial law; phases are pairs (block, position), 0-based. The network (BWNetwork) carries $H$, $C$, $\kappa$, $\boldsymbol\lambda^{(0)}$ and one law per route; the standing assumptions are explicit theorem hypotheses: 0/1 entries and full row rank of $H$, every route uses a link, $C_\ell>0$, $\kappa_r>0$, $\lambda^{(0)}_r>0$, (7)–(8) with $\mathcal L_s\neq\emptyset$. The allocation is a predicate on route totals, and theorems take an allocation function satisfying it (it exists and is unique by milestone (5)). The chain's rates are exactly (60) with zero diagonal; a stationary distribution is a nonnegative, total-mass-one solution of the global balance equations (the published KellyStochasticNetworks.FullBalance), and statements hold for every such solution. $o(1/\epsilon)$ and $O(\cdot)$ are explicit $\epsilon$–$\delta$ statements with constants chosen before $\epsilon$, and every expectation carries a summability clause.

The goal's statement uses only the model layer; $M$, $\mathbf b^{(\ell)}$, the cone distance and the projections live in a second definitions module used by the milestones. The goal cannot be satisfied trivially: the allocation exists (milestone (5)), stationary distributions exist for every $0<\epsilon<1$ (Lemma 7), the expectation must be finite, and none of the network, the weights or the file-size laws is specialised.

Paper slips handled in the statements: Lemma 7 is stated for $0<\epsilon<1$ (the page says "nonnegative"); Lemma 8 quantifies over all $\xi_1,\xi_2>0$ with $\xi_2-\xi_1=2$, as its proof does; $\mathbb E[U_\ell]=\epsilon C_\ell$ is stated for critical links only, which is what its derivation shows; Lemma 9 holds for every multiplier vector, since multipliers need not be unique; the closing brackets missing in (80) are restored.

Needed infrastructure: the matrix exponential of block-bidiagonal matrices and its integrals; positive definiteness through the PBH test; countable-state continuous-time Markov chains (irreducibility, stationarity, uniformisation, zero expected drift for integrable Lyapunov functions); finite-dimensional convex optimisation with KKT conditions. Contributions to any of these, and proofs of any milestone, are welcome.

Selected references

• W. Wang, S. T. Maguluri, R. Srikant, L. Ying, Heavy-traffic insensitive bounds for weighted proportionally fair bandwidth sharing policies, arXiv:1808.02120v2, 2021; Math. Oper. Res. 2022. https://arxiv.org/abs/1808.02120
• L. Massoulié, J. W. Roberts, Bandwidth sharing and admission control for elastic traffic, Telecommunication Systems 15(1):185–201, 2000.
• W. N. Kang, F. P. Kelly, N. H. Lee, R. J. Williams, State space collapse and diffusion approximation for a network operating under a fair bandwidth sharing policy, Ann. Appl. Probab. 19(5):1719–1780, 2009.
• H.-Q. Ye, D. D. Yao, A stochastic network under proportional fair resource control — diffusion limit with multiple bottlenecks, Oper. Res. 60(3):716–738, 2012.
• M. Vlasiou, J. Zhang, B. Zwart, Insensitivity of proportional fairness in critically loaded bandwidth sharing networks, arXiv:1411.4841, 2014. https://arxiv.org/abs/1411.4841
• A. Eryilmaz, R. Srikant, Asymptotically tight steady-state queue length bounds implied by drift conditions, Queueing Systems 72(3–4):311–359, 2012.
• D. Bertsimas, D. Gamarnik, J. N. Tsitsiklis, Performance of multiclass Markovian queueing networks via piecewise linear Lyapunov functions, Ann. Appl. Probab. 11(4):1384–1428, 2001.
• L. Massoulié, Structural properties of proportional fairness: stability and insensitivity, Ann. Appl. Probab. 17(3):809–839, 2007.

Motivation

A constrained optimization problem often has an objective of the form $\varphi(x)=\vartheta(f(x))$: a smooth map $f$ describes the model, while an extended-real function $\vartheta$ gives the cost and can assign $+\infty$ to infeasible outputs. Such a description covers polyhedral constraints, quadratic penalties on pieces, and many nonsmooth composite objectives. Solvers need to know how the local first and second order behavior of $\varphi$ depends on the two parts of the model. The usual chain rules in Rockafellar and Wets, Variational Analysis use qualification conditions stronger than an error bound at the point of interest. Mohammadi, Mordukhovich, and Sarabi develop chain rules under a metric subregularity qualification condition (MSQC), including the second order result targeted here.

The paper was circulated as arXiv:1905.08837v2 in 2019 and published in Mathematics of Operations Research in 2022. This mission follows the pinned arXiv version, whose theorem and page numbering is used throughout. The result is known in mathematics; the open task here is its formalization in Lean. The paper also derives optimality conditions and statements about KKT systems from its second order analysis, but those later applications are outside this mission's target. Source: §§1, 5, 6, 8.

Setting

Fix finite dimensional Euclidean spaces $\mathbb R^n$ and $\mathbb R^m$. An extended-real function $\varphi:\mathbb R^n\to(-\infty,+\infty]$ has finite domain $\operatorname{dom}\varphi=\{x:\varphi(x)<+\infty\}$. Assigning $+\infty$ outside a feasible set lets an ordinary function and a constraint be treated together. A convex piecewise linear-quadratic function (PWLQ) $\vartheta$ has a finite collection of polyhedral convex pieces $\Omega_i$ whose union is its domain. On each piece its value is $\tfrac12\langle A_i y,y\rangle+\langle a_i,y\rangle+\alpha_i$, where $A_i$ is symmetric. The separate formulas must agree where pieces meet, because all describe the same function. Source: (2.9), p. 5.

A function $\varphi$ is fully subamenable at $\bar x$ when it agrees with $\vartheta\circ f$ on a neighborhood of $\bar x$, with $f$ twice differentiable at $\bar x$, $\vartheta$ convex PWLQ, and MSQC satisfied there. Write $\Omega=\{x:f(x)\in\operatorname{dom}\vartheta\}$. MSQC says that for some $\kappa\ge0$ and all $x$ near $\bar x$, $\operatorname{dist}(x,\Omega)\le\kappa\operatorname{dist}(f(x),\operatorname{dom}\vartheta)$. This controls how far a nearby point is from feasibility through its residual in the outer domain. It is the paper's condition (3.5), not metric regularity. Source: Definition 3.2 and (3.5), pp. 9–10; Definition 4.2, p. 16.

The subderivative $d\varphi(\bar x)(w)$ is a lower limit of first order difference quotients as positive time tends to zero and the direction tends to $w$. Given a limiting subgradient $\bar v\in\partial\varphi(\bar x)$, the second subderivative $d^2\varphi(\bar x,\bar v)(w)$ uses the quotient after subtracting the linear term $t\langle\bar v,w\rangle$ and dividing by $\tfrac12t^2$. Proper twice epi-differentiability means these quotients epi-converge to a second subderivative that never equals $-\infty$ and is finite somewhere. The paper gives an equivalent test using recovery directions for every positive null sequence; that test is used in Lean. Source: (2.11), (2.15), (2.16), pp. 6–7.

Formalization targets

Main theorem

For every $\bar v\in\partial\varphi(\bar x)$, a fully subamenable $\varphi$ is properly twice epi-differentiable at $\bar x$ for $\bar v$. With

$$\Lambda(\bar x,\bar v)=\{\lambda\in\partial\vartheta(f(\bar x)):\nabla f(\bar x)^*\lambda=\bar v\},$$

its second subderivative satisfies, for every $w\in\mathbb R^n$,

$$d^2\varphi(\bar x,\bar v)(w)=\max_{\lambda\in\Lambda(\bar x,\bar v)}\bigl\{d^2\vartheta(f(\bar x),\lambda)(\nabla f(\bar x)w)+\langle\lambda,\nabla^2f(\bar x)(w,w)\rangle\bigr\}.$$

The maximum is attained; a supremum alone is a weaker claim. This is Theorem 5.2 and (5.3), p. 22.

Supporting statements

The milestones are the paper's equality rules for first order subderivatives and subgradients (Theorems 3.4 and 3.6), its identification of critical directions with the finite domain of the second subderivative (Theorem 4.4), the PWLQ outer-function formula (4.8), the lower bound (4.10), and the parabolic limit formula (Lemma 5.1). Each names a separate mathematical claim needed to connect the composite model to the goal. Source: §§3–5.

Significance

Theorem 5.2 gives a data-level way to evaluate the second order behavior of a nonsmooth composite: the outer function contributes its own second subderivative, the inner map contributes its Hessian, and multipliers connect the two. Its properness and epi-differentiability clauses make the formula suitable for the paper's later no-gap second order optimality conditions and parametric analysis. Without those clauses, an equality of extended-real expressions alone would not establish the stability of the difference quotients. Source: Theorem 5.2 and §6.

A formal development of this result would add reusable definitions and lemmas for extended-real difference quotients, second-order tangent geometry, PWLQ functions, and local composite error bounds. The present draft contains statements and definitions that compile; it does not yet contain proofs of the open theorem items. The published limiting-subdifferential definition is reused, while the paper-specific local representation and multiplier set are defined here.

Difficulty

A first order expansion of $f$ does not settle the second order claim. Near a polyhedral boundary, the direction $w$ may be tangent while a fixed straight path $\bar x+tw$ leaves the domain; the second-order correction and the outer function's active piece matter. MSQC controls distance to feasibility but does not itself identify a feasible second-order path or a maximizing multiplier. The source therefore needs separate results about critical directions, PWLQ second subderivatives, parabolic limits, and dual attainment before the full formula can be stated with a maximum. Source: §§4–5, especially pp. 17–23.

Formalization scope

Lean uses EuclideanSpace ℝ (Fin n) and EReal. The paper's codomain excludes $-\infty$; the relevant hypotheses enforce that exclusion, while the subderivatives themselves may take either infinite value. The finite domain is defined by exclusion of $+\infty$. A PWLQ representation records finite closed half-space intersections, symmetric operators, and the exact $\tfrac12$ quadratic coefficient. Twice differentiability includes differentiability near the base point and differentiability of the derivative at the point. The composite identity holds on a neighborhood rather than globally. MSQC uses the paper's local distance estimate with $\kappa\ge0$. Positive null sequences represent $t\downarrow0$; a filter lower limit represents the varying direction. The second quotient retains the paper's $\tfrac12t^2$ denominator.

The subdifferentials are the published analytic regular and limiting subdifferentials. Their use matches the paper's geometric subdifferentials at the lower semicontinuous functions in these statements. The goal computes the second subderivative from the lower-limit definition, rather than defining it by (5.3). Full subamenability retains MSQC and a genuine PWLQ representation; it is neither an empty-domain case nor a stronger metric-regularity special case. Contributions toward proofs of the milestone theorems, their needed tangent-set geometry, and the goal are in scope.

Selected references

• A. Mohammadi, B. S. Mordukhovich, M. E. Sarabi, Variational Analysis of Composite Models with Applications to Continuous Optimization, arXiv:1905.08837v2, 2019; published in Mathematics of Operations Research, 2022. https://arxiv.org/abs/1905.08837v2
• R. T. Rockafellar and R. J.-B. Wets, Variational Analysis, Springer, 1998. https://doi.org/10.1007/978-3-642-02431-3