linkRate_zero
plain-language theorem explainer
The theorem states that the link rate at zero φ-rungs equals the reference rate R_0. QKD link-budget engineers cite this base case when verifying the exponential attenuation model R(n) = R_0 / phi^n. The proof is a one-line wrapper that unfolds the linkRate definition and simplifies.
Claim. The link rate at rung zero satisfies $R(0) = R_0$, where $R(n) := R_0 / phi^n$ and $R_0 := 1$.
background
In the coherence-protected QKD link budget, the link rate at φ-rung n is defined by linkRate n = R_0 / phi^n, with R_0 fixed at 1 as the reference rate at zero distance. This encodes the bit rate after n · L_φ km of fiber, with each L_φ interval attenuating the rate by 1/phi. The module derives the full budget for phantom-cavity-protected QKD links achieving R(L) = R_0 · phi^(-L/L_φ).
proof idea
The proof is a one-line wrapper that unfolds the definition of linkRate and applies simp to reduce the n=0 case directly to R_0.
why it matters
This zero-distance anchor populates the rate_zero field of coherenceProtectedQKDLinkBudgetCert, which assembles the full set of rate properties (positivity, strict anti-monotonicity, successor step). It supplies the base case for the engineering derivation of RS_PAT_040 and aligns with the phi-ladder attenuation length in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.