attenuationPerRung_band
plain-language theorem explainer
The theorem establishes that the per-rung attenuation factor equals 1/phi and lies strictly inside the interval (0.617, 0.622). Engineers certifying coherence-protected QKD links cite this bound to confirm the fiber-loss scaling in the link-budget model. The proof is a short term-mode argument that unfolds the definition, imports the two numerical bounds on phi, and closes the resulting division inequalities with linear arithmetic.
Claim. Let $phi$ denote the golden ratio. The per-rung attenuation factor satisfies $0.617 < 1/phi < 0.622$.
background
The Coherence-Protected QKD Link Budget module models the link rate as $R(n) = R_0 · phi^{-n}$, where each increment of the rung index corresponds to one attenuation length $L_phi$. The per-rung attenuation factor is defined by the equation attenuationPerRung := 1/phi. This construction sits inside the Recognition Science forcing chain, with phi fixed as the self-similar solution. The upstream lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo supply the concrete numerical bounds $1.61 < phi < 1.62$ that drive the interval for 1/phi.
proof idea
The proof unfolds attenuationPerRung to obtain 1/phi. It obtains the lower bound from phi_gt_onePointSixOne and the upper bound from phi_lt_onePointSixTwo. It then rewrites the target inequalities using lt_div_iff₀ and div_lt_iff₀ (both under phi_pos) and finishes both goals with linarith.
why it matters
The bound is invoked directly by qkd_one_statement to assemble the full one-statement certificate and by coherenceProtectedQKDLinkBudgetCert to populate the master engineering record. It completes the numerical check required by the module's falsifier for RS_PAT_040, confirming that observed fiber attenuation per phi-rung must fall inside the predicted interval around 1/phi. The result anchors the phi-ladder scaling inside the engineering track of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.