qkd_one_statement
plain-language theorem explainer
Engineers modeling coherence-protected QKD over fiber cite this theorem for the precise rate scaling under the phi-ladder. It asserts that link rate satisfies the recurrence R(n+1) = R(n)/phi, decreases strictly with rung count n, and that the per-rung attenuation factor 1/phi lies in (0.617, 0.622). The proof is a term-mode conjunction that directly invokes the successor relation, the strict anti-monotonicity result, and the two numerical bounds on attenuationPerRung.
Claim. Let $R(n) = R_0 / phi^n$ with $R_0 = 1$. Then $R(n+1) = R(n)/phi$ for all natural numbers $n$, $R(m) < R(n)$ whenever $n < m$, and the per-rung attenuation satisfies $0.617 < 1/phi < 0.622$.
background
The module derives the link budget for phantom-cavity-protected QKD, where distance is measured in phi-rungs of fiber length $L_phi$. linkRate(n) is defined as $R_0 / phi^n$ with reference rate $R_0 = 1$. attenuationPerRung is defined as $1/phi$. Upstream, linkRate_succ shows the recurrence by unfolding the definition and applying pow_succ together with field_simp. linkRate_strict_anti proves strict decrease via pow_lt_pow_right_0 on the positive powers of phi. attenuationPerRung_band supplies the numerical interval by invoking the bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
proof idea
Term-mode proof that builds the three-way conjunction by applying linkRate_succ to the first conjunct, linkRate_strict_anti to the second, and the two projections of attenuationPerRung_band to the bounds on attenuationPerRung.
why it matters
This theorem supplies the consolidated one-statement summary for the QKD link budget in the engineering track. It directly encodes the module claim that each phi-rung attenuates the rate by 1/phi in the interval (0.617, 0.622), closing the derivation under the phi-ladder fixed point (T6) and eight-tick octave (T7). No downstream theorems are listed, indicating it functions as the terminal engineering statement for this track. The module falsifier is a deployed link whose measured attenuation per L_phi falls outside the stated band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.