Positive chip loss imposes a finite usable protection depth

Proved

QAlgorithms.Papers.Independent.Intakenext100.P89.loss_protection_ceiling

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

In the source's independent-loss construction, let $\eta_s,\eta_d,\eta_c\in(0,1]$ , $\alpha>0$ , $\beta,\tau_s,\tau_f\ge0$ and $c_{\rm ch},c_f>0$ , with consistent units. Assume positive attenuation during a chip feedforward step, $\beta\tau_s>0$ . Put $a=e^{-\beta\tau_s c_{\rm ch}}$ , $f=e^{-\alpha\tau_f c_f}$ , $h=\eta_s\eta_d/(2-\eta_s\eta_d)$ . For a fusion depth $k$ , node count $n\ge1$ and range $L\ge0$ , the traveling and retained photon survival probabilities are

s_{\rm trav}=e^{-\alpha L/(2n)}a^{k+2}h\eta_c,\qquad s_{\rm stat}=e^{-\alpha L/n}a^{k+2}fh\eta_c.

There is an integer $K$ , depending only on the devices, such that

\forall k\ge K\;\forall n\ge1\;\forall L\ge0,\qquad s_{\rm trav}<\tfrac12\quad\text{and}\quad s_{\rm stat}<\tfrac12.

Thus this construction eventually leaves the tree code's operating regime as protection depth grows. This is the mechanism used by the source's finite-protection discussion; it does not assert that clusters cannot be created or that arbitrary optical computing is impossible. Positive per-step chip attenuation is essential; the allowed zero-delay or zero-attenuation boundary is excluded here.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P89

Formal statement

namespace QAlgorithms.Papers.Independent.Intakenext100.P89

open scoped BigOperators ComplexConjugate

-- Accepted probability primitives: symbol true is success; choose n x is zero for x > n.

open QAlgorithms.Papers.Independent.Information100.P54 (binomialMass)

open QAlgorithms.Papers.Independent.Information100.P56 (bernoulli)

noncomputable section

/-- Source p.14: positive loss per chip feedforward step eventually puts photon survival
below the tree code's 1/2 operating threshold, uniformly over range and node count.
Zero per-step attenuation is excluded. This bounds usable protection in this construction;
it does not assert physical noncreation or an impossibility for arbitrary optical computing. -/
theorem loss_protection_ceiling (d : Devices) (hLoss : 0 < d.beta * d.tauS) :
    ∃ K : ℕ, ∀ k : ℕ, K ≤ k → ∀ (n : ℕ), 0 < n → ∀ (L : ℝ), 0 ≤ L →
      travelingSurvival d k n L < (1 : ℝ) / 2 ∧
      stationarySurvival d k n L < (1 : ℝ) / 2 := by sorry

end

end QAlgorithms.Papers.Independent.Intakenext100.P89

Source

Rate-distance tradeoff and resource costs for all-optical quantum repeaters, arXiv:1603.01353v4, PDF p. 14, V: finite usable protection depth under on-chip loss

Read-back

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

For every $d$ consisting of real parameters $\eta_S,\eta_D,\eta_C,\alpha,\beta,\tau_S,\tau_F,c_{\mathrm{Chip}},c_{\mathrm{Fiber}}$ satisfying $0<\eta_S,\eta_D,\eta_C\le1$ , $\alpha>0$ , $\beta,\tau_S,\tau_F\ge0$ , and $c_{\mathrm{Chip}},c_{\mathrm{Fiber}}>0$ , assume additionally that $\beta\tau_S>0$ . There exists a natural number $K$ such that, for every natural number $k\ge K$ , every positive natural number $n$ , and every real $L\ge0$ , both inequalities hold:

e^{-\alpha L/(2n)} \left(e^{-\beta\tau_Sc_{\mathrm{Chip}}}\right)^{k+2} \frac{\eta_S\eta_D}{2-\eta_S\eta_D}\,\eta_C <\frac12, \qquad e^{-\alpha L/n} \left(e^{-\beta\tau_Sc_{\mathrm{Chip}}}\right)^{k+2} \frac{\eta_S\eta_D}{2-\eta_S\eta_D}\,\eta_C e^{-\alpha\tau_Fc_{\mathrm{Fiber}}} <\frac12.

The same $K$ works for all such $n$ and $L$ , including $L=0$ ; $n=0$ is excluded.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph