linkRate_strict_anti
plain-language theorem explainer
linkRate_strict_anti establishes that the QKD link rate decreases strictly with increasing φ-rung distance. Engineers certifying coherence-protected quantum channels cite it to confirm the anti-monotonic dependence on fiber length. The tactic proof unfolds the rate definition, invokes power monotonicity from one_lt_phi, and applies a positive-division inequality.
Claim. Let $R(n) := R_0 / phi^n$ with $R_0 = 1$ the zero-distance reference rate and $phi > 1$ the golden ratio. For natural numbers $n < m$, $R(m) < R(n)$.
background
In the Coherence-Protected QKD Link Budget module the link rate at φ-rung $n$ is defined by linkRate $n = R_0 / phi^n$, where the reference rate $R_0$ is set to 1. This implements the attenuation model $R(L) = R_0 · phi^(-L/L_φ)$ for phantom-cavity-protected QKD, each $L_φ$ km of fiber multiplying the rate by $1/phi$. The upstream lemma one_lt_phi supplies the fact that $1 < phi$, quoted as “φ > 1: The golden ratio is strictly greater than 1.”
proof idea
The proof unfolds linkRate, obtains $0 < phi^n$ via pow_pos, derives $phi^n < phi^m$ from pow_lt_pow_right₀ applied to one_lt_phi and the hypothesis $n < m$, confirms $0 < R_0$ by unfolding and norm_num, then concludes with div_lt_div_of_pos_left.
why it matters
It supplies the strict anti-monotonicity required by coherenceProtectedQKDLinkBudgetCert and is invoked directly in qkd_one_statement to complete the one-statement summary of the QKD link budget, including the attenuation band $(0.617, 0.622)$. This closes the engineering derivation for RS_PAT_040 and applies the phi self-similarity fixed point to practical distance scaling in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.