Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

A sharp lower bound for entanglement-buffer availability

Abstract

The always-failing purification policy at q equal to one attains the minimum buffer availability.

Definition 1.1 (Admissible purification coefficients).

Formalization. D5/S3/Quantum/Decoherence/EntanglementBufferAvailabilityLowerBound.admissible (✓ std3).

Citation. Álvaro G. Iñesta; Bethany Davies; Sounak Kar; Stephanie Wehner (2026). Entanglement buffering with multiple quantum memories. DOI: 10.1038/s41534-025-01161-3. URL: https://arxiv.org/abs/2502.20240v1.

Commentary.

For each k in Fin n, the success probability c(k)(f − 1/4) + d(k) lies between zero and one for every input fidelity f between 1/4 and one. The unnormalized excess fidelity a(k)(f − 1/4) + b(k) lies between zero and three quarters of that probability. These are the probability and output-fidelity conditions of Appendix C, main.tex lines 1735–1757. The index k represents k.val + 1 newly generated links, so Fin n represents the source’s indices one through n. The inequalities also include protocols with zero success probability.

Definition 1.2 (The closed-form availability).

Formalization. D5/S3/Quantum/Decoherence/EntanglementBufferAvailabilityLowerBound.availability (✓ std3).

Citation. Álvaro G. Iñesta; Bethany Davies; Sounak Kar; Stephanie Wehner (2026). Entanglement buffering with multiple quantum memories. DOI: 10.1038/s41534-025-01161-3. URL: https://arxiv.org/abs/2502.20240v1.

Commentary.

The expression is the availability formula of Theorem 1, main.tex lines 378–409. Here pg is the generation probability per short-lived memory, pc is the consumption probability, q is the purification probability, gam is the decay parameter, and fnew is the newly generated fidelity. The auxiliary values ta, tb, tc and td are the four normalized, binomially weighted coefficient sums. The weight binomialMass pg n (k.val + 1) is (↑(n.choose (k.val + 1)) : ℝ) · pg^(k.val + 1) · (1 − pg)^(n − (k.val + 1)); the upward arrow includes the natural binomial coefficient in the real numbers. The values tgen and tocc are the expected empty and occupied durations in the source’s model. The definition is a real-valued expression for all parameters, with real division defined even at zero; the comparison below imposes the parameter conditions that make the relevant denominators positive. The source identifies this expression with the limiting fraction of consumption requests that find a link, defined at main.tex lines 344–350.

Definition 1.3 (Comparison with the always-failing policy).

Formalization. D5/S3/Quantum/Decoherence/EntanglementBufferAvailabilityLowerBound.claim (✓ std3).

Source. Repository-derived.

Acknowledgement. Álvaro G. Iñesta; Bethany Davies; Sounak Kar; Stephanie Wehner (2026). Entanglement buffering with multiple quantum memories. DOI: 10.1038/s41534-025-01161-3. URL: https://arxiv.org/abs/2502.20240v1.

Commentary.

Fix a positive number n of generation memories, pg and pc in (0,1], gam at least zero, and fnew in (1/4,1]. Every admissible coefficient family and every q in [0,1] has availability at least that of the zero coefficient families at q equal to one. This is the formula-based reading of the conjecture at main.tex lines 500–502. When c and d vanish, admissibility at fidelities 1/4 and one forces b and then a to vanish, so the four zero families describe the always-failing policy.

Theorem 1.4 (The always-failing policy attains the lower bound).

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/EntanglementBufferAvailabilityLowerBound.result (✓ std3). ∎

Resolves. Problems/inesta-davies-kar-wehner-2026-entanglement-buffer-availability-lower-bound (proved) by D5/S3/Quantum/Decoherence/EntanglementBufferAvailabilityLowerBound.result.

Source. Repository-derived.

Acknowledgement. Álvaro G. Iñesta; Bethany Davies; Sounak Kar; Stephanie Wehner (2026). Entanglement buffering with multiple quantum memories. DOI: 10.1038/s41534-025-01161-3. URL: https://arxiv.org/abs/2502.20240v1.

Commentary.

First set g = 1 − (1 − pg)^n. The binomial expansion shows that the weights binomialMass pg n (k.val + 1), summed over Fin n, have total g. Since n is positive and 0 < pg ≤ 1, one has 0 < g ≤ 1, and every weight is nonnegative.

Let aa, bb, cc and dd be the weighted sums of a, b, c and d with these weights. Multiply each admissibility inequality by its nonnegative weight and sum. Evaluating at f = 1/4 and f = 1 gives 0 ≤ dd ≤ g, 0 ≤ (3/4)cc + dd ≤ g, 0 ≤ bb ≤ (3/4)dd, and 0 ≤ (3/4)aa + bb ≤ (3/4)((3/4)cc + dd).

The required estimate for two coordinates uses real u, v, w, z, ell, mu and h with v,w ≥ 0, mu > 0, 0 ≤ h ≤ 1, and both column sums u + w and v + z between ell and 1 − mu. The transpose of I minus the matrix with rows (u,v) and (w,z) has positive diagonal and is strictly diagonally dominant. Its determinant det = (1 − u)(1 − z) − vw is therefore positive. Put y0 = (1 − z)h + v(1 − h) and y1 = wh + (1 − u)(1 − h). Both are nonnegative. The identity (1 − ell)(y0 + y1) − det = (u + w − ell)y0 + (v + z − ell)y1 then gives det ≤ (1 − ell)num, where num = y0 + y1.

To apply this estimate to the four aggregate coefficients, temporarily call them a,b,c,d, write mu for pc, and take real g,q,e,h with 0 < g ≤ 1, 0 ≤ q ≤ 1, e ≥ 1 and 0 ≤ h ≤ 3/4. Set t = q(1 − mu), ell = (1 − qg)(1 − mu), p = mu + qg(1 − mu), and r = 1/e. Thus 0 ≤ r ≤ 1, t,ell ≥ 0, p > 0, p = 1 − ell and ell + tg = 1 − mu. Use u = (ell + t(a + (4/3)b))r + t((4/3)b)(1 − r), v = t((4/3)b), w = t(d + (3/4)c − a − (4/3)b)r + (ell + t(d − (4/3)b))(1 − r), and z = ell + t(d − (4/3)b).

The aggregate endpoint inequalities give d + (3/4)c − a − (4/3)b ≥ 0 and d − (4/3)b ≥ 0, so v and w are nonnegative. Moreover, u + w = ell + t(r((3/4)c + d) + (1 − r)d) and v + z = ell + td. The convex combination in the first expression, and d in the second, lie in [0,g]. Both column sums therefore lie in [ell,1 − mu]. Apply the two-coordinate estimate with initial first coordinate (4/3)h. For its determinant det and numerator num, direct algebra gives e·det = (e − ell − t·a)(p − t·d) − t²bc and e·num = e − ell − t·a + t·c·h. Thus x = e − ell is positive, D = (x − t·a)(p − t·d) − t²bc is positive, and 1 ≤ p((x − t·a + t·c·h)/D).

Now take e = Real.exp gam, h = fnew − 1/4 and the weighted coefficients aa,bb,cc,dd. The parameter assumptions give e ≥ 1 and 0 ≤ h ≤ 3/4. Put x = Real.exp gam − (1 − q + q(1 − pg)^n)(1 − pc), p = pc + qg(1 − pc), t = q(1 − pc), det = (x − t·aa)(p − t·dd) − t²bb·cc, num = x − t·aa + t·cc(fnew − 1/4), and s = num/det. The preceding estimate gives x,p,det > 0 and 1 ≤ p·s, hence s > 0. The normalized denominator (1 − t·aa/x)(1 − t·dd/p) − (t·bb/p)(t·cc/x) equals det/(xp) and is positive. Substituting into the occupied-duration formula and cancelling these nonzero denominators identifies tocc with s. Consequently the availability is s/(1/g + s).

Since q ≤ 1, p ≤ pc + (1 − pc)g; multiplying by s yields 1 ≤ s(pc + (1 − pc)g). Both denominators in g/(pc + (2 − pc)g) ≤ s/(1/g + s) are positive. Cross multiplication, followed by g(1/g + s) = 1 + gs, reduces the comparison to that last inequality. This proves the stated numerical lower bound for every admissible policy.

Finally substitute q = 1 and the four zero coefficient families. All four normalized coefficient sums vanish. With p = pc + g(1 − pc) > 0, the availability simplifies to (1/p)/(1/g + 1/p) = g/(g + p) = g/(pc + (2 − pc)g). Replacing the left side of the desired policy comparison by this value and applying the numerical lower bound proves the claim. The zero families are admissible, so they attain the bound.

References