attenuationPerRung
plain-language theorem explainer
The definition introduces the per-rung attenuation factor as the reciprocal of the golden ratio. Engineers modeling coherence-protected QKD links cite this constant to express the exponential decay of bit rate with distance in the phi-ladder model. It is introduced as a direct abbreviation that supplies the numerical factor used throughout the module's certification theorems.
Claim. The per-rung attenuation factor is the real number $1/phi$, where $phi$ is the golden ratio.
background
The module develops an engineering model for phantom-cavity-protected QKD links under Recognition Science track J7. The link rate is given by $R(L) = R_0 · phi^(-L/L_phi)$, where each phi-rung of fiber multiplies the rate by the attenuation factor. This definition supplies the constant $1/phi ≈ 0.618$ that appears in the rate-succ relation and the certification structure. The module imports the golden ratio from Constants and the cost primitives from Cost; the local setting requires experimental fiber loss per attenuation length to stay within 5% of this value.
proof idea
The declaration is a direct definition that sets the attenuation factor to the quotient of 1 and the golden ratio constant.
why it matters
It supplies the attenuation value required by the CoherenceProtectedQKDLinkBudgetCert structure and the qkd_one_statement theorem. The definition completes the engineering derivation for the QKD link budget, realizing the per-rung loss prediction from the phi-ladder. It connects the abstract forcing-chain fixed point to a concrete falsifiable claim whose module falsifier demands experimental confirmation within 5%.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.