linkRate_pos
plain-language theorem explainer
Engineers modeling coherence-protected QKD links cite this result to confirm that bit rates stay positive at every φ-rung. The theorem states that linkRate n exceeds zero for all natural n. Its term proof unfolds the rate definition and invokes standard positivity lemmas for division and powers.
Claim. For every natural number $n$, $0 < 1/φ^n$, where $φ$ is the golden-ratio fixed point and the reference rate equals the constant 1.
background
The CoherenceProtectedQKDLinkBudget module encodes the link budget for phantom-cavity QKD protection. It defines the reference rate R_0 as the constant 1 and the rung-dependent rate as R_0 divided by phi to the power n. This matches the exponential decay form R(L) = R_0 · φ^(-L/L_φ) with per-rung factor 1/φ.
proof idea
The term-mode proof first unfolds the definitions of linkRate and R_0. It then applies div_pos to one_pos and the result of pow_pos applied to phi_pos.
why it matters
The result populates the rate_pos component of coherenceProtectedQKDLinkBudgetCert. This certifies the engineering model in the J7 track of Plan v5. It aligns with the self-similar fixed point phi forced in the unified chain and ensures the rate formula yields physically admissible positive values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.