qkd_one_statement
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute absolute bit rates for concrete fiber lengths or detector parameters.
- Does not incorporate additional losses from coupling, dispersion, or detector dark counts.
- Does not address entanglement distribution or multi-mode QKD protocols.
- Does not prove the physical realizability of the phantom-cavity protection.
formal statement (Lean)
102theorem qkd_one_statement :
103 (∀ n, linkRate (n + 1) = linkRate n / phi) ∧
104 (∀ {n m : ℕ}, n < m → linkRate m < linkRate n) ∧
105 (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622 :=
proof body
Term-mode proof.
106 ⟨linkRate_succ, @linkRate_strict_anti,
107 attenuationPerRung_band.1, attenuationPerRung_band.2⟩
108
109end
110
111end CoherenceProtectedQKDLinkBudget
112end Engineering
113end IndisputableMonolith