linkRate_succ
plain-language theorem explainer
The recurrence states that the QKD link rate at rung n+1 equals the rate at rung n divided by phi. Coherence-protected QKD engineers cite this to confirm the exact per-rung attenuation factor of 1/phi. The proof is a term-mode reduction that unfolds the explicit definition of linkRate and rewrites the power via pow_succ before field simplification.
Claim. For every natural number $n$, if the link rate is defined by $R(n) := R_0 / phi^n$, then $R(n+1) = R(n) / phi$.
background
The module treats the link budget for phantom-cavity-protected QKD, where the rate at phi-rung $n$ is defined by linkRate $n = R_0 / phi^n$. This encodes attenuation of $1/phi$ per $L_phi$ of fiber, matching the module statement that each $L_phi$ reduces the rate by approximately 0.618. Upstream results supply the linkRate definition directly; the various rung definitions from mass anchors and asteroid spectroscopy establish the broader phi-ladder context without appearing in the present step.
proof idea
The term proof unfolds linkRate, rewrites the exponent with pow_succ, and closes with field_simp.
why it matters
The theorem supplies the successor clause for coherenceProtectedQKDLinkBudgetCert and for the qkd_one_statement that packages the full anti-monotonic decay together with the attenuation band (0.617, 0.622). It realizes the phi-ladder attenuation required by the Recognition Science forcing chain at the self-similar fixed point phi. The module falsifier asks for experimental confirmation of the exact 1/phi factor to within 5 percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.