CoherenceProtectedQKDLinkBudgetCert
plain-language theorem explainer
A structure bundles the zero-distance rate, positivity, strict decrease, recursive scaling by the golden ratio, and bounds on the per-rung attenuation factor for the quantum key distribution link model. Researchers in quantum optics and communication engineering would cite this when confirming the phi-ladder decay law in protected fiber channels. The declaration is a plain structure definition whose fields receive their values from explicit formulas and elementary inequalities on the golden ratio.
Claim. Let $R : ℕ → ℝ$ be the link rate after $n$ rungs and let $α$ be the attenuation per rung. The certificate requires $R(0) = 1$, $R(n) > 0$ for every natural number $n$, $R$ is strictly decreasing, $R(n+1) = R(n)/φ$, $0 < α$, $α < 1$, and $0.617 < α < 0.622$.
background
The module models a phantom-cavity-protected QKD link whose bit rate follows $R(L) = R_0 · φ^{-L/L_φ}$, with each $L_φ$ of fiber multiplying the rate by $1/φ$. Here $R_0$ is the reference rate at zero distance, defined as 1, and the link rate at rung $n$ is given explicitly by $R_0 / φ^n$. The per-rung attenuation is defined as $1/φ ≈ 0.618$ (from the upstream definition of attenuationPerRung). Upstream results establish positivity of the attenuation, its strict upper bound below 1, and the numerical interval (0.617, 0.622) via direct comparison with the golden-ratio bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo. The module documentation states the falsifier as a deployed link whose attenuation deviates from $1/φ$ per $L_φ$ by more than 5 percent.
proof idea
This is a structure definition with no proof body. Its fields are satisfied by substituting the closed-form expression for the link rate and the definition of the attenuation factor, then invoking the already-proved lemmas on positivity, the recursive step, and the golden-ratio bounds.
why it matters
The structure supplies the type for the master certificate that closes the engineering derivation of the coherence-protected QKD link budget. It directly encodes the Recognition Science prediction that fiber attenuation occurs in exact multiples of the golden ratio per characteristic length, consistent with the phi-ladder and T6 fixed-point constructions. The downstream instantiation assembles the certificate from the link-rate lemmas, leaving open the experimental test of whether real phantom-cavity devices realize the precise numerical band on attenuation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.