linkRate
plain-language theorem explainer
linkRate defines the QKD bit rate at the nth phi-rung as R_0 divided by phi to the power n. QKD engineers and Recognition Science modelers cite it when calculating distance-dependent rates under coherence protection. It is introduced as a direct definition that downstream theorems unfold to establish positivity, strict decrease, and the one-statement certification.
Claim. $R(n) = R_0 / phi^n$ for natural number $n$, where $R_0$ is the reference link rate at zero distance.
background
The Coherence-Protected QKD Link Budget module models fiber attenuation for phantom-cavity-protected QKD links (RS_PAT_040). Each phi-rung corresponds to L_φ km of fiber and attenuates the rate by 1/phi. The definition uses R_0, the reference link rate at zero distance set to 1 in RS-native units, implementing the discrete version of R(L) = R_0 · φ^(-L/L_φ).
proof idea
This is a direct definition with no proof steps. Downstream theorems such as linkRate_zero, linkRate_pos, and linkRate_succ unfold the definition and apply simp, div_pos, or pow_succ to obtain the required equalities and inequalities.
why it matters
This definition anchors the CoherenceProtectedQKDLinkBudgetCert structure and the qkd_one_statement theorem, which certifies strict anti-monotonicity and attenuationPerRung in (0.617, 0.622). It realizes the engineering derivation for track J7, connecting to the phi-forced self-similar fixed point (T6) and the eight-tick octave (T7) through the phi-ladder scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.