attenuationPerRung_pos
plain-language theorem explainer
The theorem proves positivity of the per-rung attenuation factor in the coherence-protected QKD link budget. Quantum link designers cite it to guarantee that the exponential decay model R(L) = R_0 · φ^(-L/L_φ) never produces non-positive rates. The proof is a one-line wrapper invoking div_pos on the unit and the positive golden-ratio constant.
Claim. $0 < 1/φ$ where $φ$ is the golden-ratio fixed point.
background
The Coherence-Protected QKD Link Budget module models phantom-cavity-protected links with bit rate decaying by the factor 1/φ per φ-rung length of fiber. The upstream definition attenuationPerRung sets this factor explicitly as 1/φ ≈ 0.618. Recognition Science supplies φ as the self-similar fixed point forced in the T6 step of the unified forcing chain.
proof idea
The proof is a one-line wrapper that applies the div_pos lemma to one_pos and phi_pos.
why it matters
Positivity feeds directly into coherenceProtectedQKDLinkBudgetCert, which certifies the full link-rate properties. It closes the engineering derivation for the φ-ladder attenuation in the Recognition Science framework, consistent with the eight-tick octave and D = 3 spatial structure. The module falsifier requires deployed links to match 1/φ attenuation to within 5%.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.