attenuationPerRung_lt_one
plain-language theorem explainer
Engineers modeling coherence-protected QKD links cite this result to confirm that the per-rung attenuation factor lies strictly below unity. It guarantees exponential decay of the link rate with distance while keeping the rate positive. The proof is a one-line term reduction that unfolds the definition and applies the known inequality 1 < phi together with the division rule for positive reals.
Claim. The per-rung attenuation factor satisfies $1/phi < 1$.
background
The module derives engineering bounds for a phantom-cavity-protected QKD link whose rate follows R(L) = R_0 · φ^(-L/L_φ), with each L_φ of fiber multiplying the rate by the factor 1/φ. attenuationPerRung is the definition 1/phi that encodes this multiplicative loss per phi-rung. The upstream lemma one_lt_phi (appearing in Constants, PhiSupport, and PhiSupport.Lemmas) establishes phi > 1, which is the key arithmetic fact needed to bound the attenuation.
proof idea
The term proof unfolds attenuationPerRung to obtain the goal 1/phi < 1, rewrites via div_lt_one (using phi_pos), and closes with exact one_lt_phi.
why it matters
This inequality feeds the coherenceProtectedQKDLinkBudgetCert definition that certifies the full link budget. It closes the J7 engineering track by confirming sub-unity attenuation per rung, consistent with the phi-ladder and the eight-tick octave structure of Recognition Science. The module falsifier requires observed fiber loss to stay within 5% of 1/phi per L_φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.