coherenceProtectedQKDLinkBudgetCert
plain-language theorem explainer
This definition assembles a concrete certificate for the coherence-protected QKD link budget by populating the required structure fields from sibling lemmas on link rate and per-rung attenuation. Engineers deriving fiber-based quantum key distribution rates in the Recognition Science framework would cite it to confirm geometric decay with factor 1/phi. The construction is a direct structure builder that assigns each field to its corresponding theorem without additional reasoning.
Claim. The coherence-protected QKD link budget certificate is the structure asserting $R(0)=R_0$, $R(n)>0$ for all $n$, $R(m)<R(n)$ for $n<m$, $R(n+1)=R(n)/phi$, and $0.617<1/phi<0.622$ where $R$ is the link rate function and $phi$ is the golden ratio.
background
The module treats phantom-cavity-protected QKD links whose bit rate decays as $R(L)=R_0cdot phi^(-L/L_phi)$ with each phi-rung of fiber contributing attenuation $1/phiapprox0.618$. The structure CoherenceProtectedQKDLinkBudgetCert packages the zero-rate identity, positivity, strict anti-monotonicity, successor recurrence, and the three attenuation bounds. Upstream results supply the definitions attenuationPerRung:=1/phi together with its positivity, upper bound less than one, and the explicit interval (0.617,0.622) obtained from the golden-ratio bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
proof idea
The definition constructs the certificate by direct field assignment: rate_zero to linkRate_zero, rate_pos to linkRate_pos, rate_strict_anti to linkRate_strict_anti, rate_succ to linkRate_succ, attenuation_pos to attenuationPerRung_pos, attenuation_lt_one to attenuationPerRung_lt_one, and attenuation_band to attenuationPerRung_band.
why it matters
This supplies the terminal certificate realizing the engineering claim for RS_PAT_040 in the coherence-protected QKD track. It closes the derivation of the geometric rate law with attenuation inside the stated band, consistent with the phi-ladder and eight-tick octave of the Recognition Science forcing chain. No downstream uses are recorded, leaving the object available for later link-budget calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.