linkRate_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the numerical value of the attenuation length L_φ in kilometers.
- Does not account for additional losses from quantum error correction.
- Does not prove the rate is strictly decreasing in n.
- Does not extend the positivity claim beyond natural-number rungs.
formal statement (Lean)
39theorem linkRate_pos (n : ℕ) : 0 < linkRate n := by
proof body
Term-mode proof.
40 unfold linkRate R_0
41 exact div_pos one_pos (pow_pos phi_pos _)
42