IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget
This module defines the reference link rate R_0 at zero distance together with the linkRate function and per-rung attenuation for coherence-protected QKD systems. Engineers applying Recognition Science to quantum communication link budgets would cite these objects when sizing feasible distances. The module consists of direct definitions followed by elementary lemmas establishing positivity, monotonicity, and band constraints on the attenuation factor.
claimLet $R_0$ be the reference link rate at zero distance. Define the link rate at rung distance $r$ by linkRate$(r) = R_0 a^r$ where $a =$ attenuationPerRung satisfies $0 < a < 1$. The module certifies these quantities via CoherenceProtectedQKDLinkBudgetCert.
background
The module sits in the engineering domain and imports the RS time quantum τ₀ = 1 tick from Constants together with cost primitives from Cost. It introduces R_0 as the zero-distance reference rate, linkRate as a distance-dependent function on the phi-ladder rungs, and attenuationPerRung as the multiplicative factor per rung. Sibling declarations establish linkRate_zero, linkRate_pos, linkRate_strict_anti, attenuationPerRung_pos, attenuationPerRung_lt_one, and attenuationPerRung_band to fix the parameter ranges.
proof idea
This is a definition module. R_0 and linkRate are introduced by direct definition; attenuationPerRung is likewise defined with an explicit band constraint. The listed lemmas (linkRate_zero, linkRate_pos, attenuationPerRung_lt_one, etc.) are one-line wrappers that apply the definitions together with the imported positivity and ordering facts from Constants and Cost.
why it matters in Recognition Science
The module supplies the concrete link-budget primitives required for coherence-protected QKD calculations inside the Recognition Science framework. It feeds engineering applications that combine the eight-tick octave and phi-ladder structure with practical distance scaling, although no downstream uses are recorded yet. It closes the engineering interface between the core constants (τ₀, phi) and deployable QKD hardware budgets.
scope and limits
- Does not derive a numerical value for R_0 from first principles.
- Does not incorporate quantum noise or security proofs.
- Does not model wavelength-dependent or hardware-specific losses.
- Does not compute end-to-end key rates for concrete fiber lengths.
depends on (2)
declarations in this module (13)
-
def
R_0 -
def
linkRate -
theorem
linkRate_zero -
theorem
linkRate_pos -
theorem
linkRate_strict_anti -
theorem
linkRate_succ -
def
attenuationPerRung -
theorem
attenuationPerRung_pos -
theorem
attenuationPerRung_lt_one -
theorem
attenuationPerRung_band -
structure
CoherenceProtectedQKDLinkBudgetCert -
def
coherenceProtectedQKDLinkBudgetCert -
theorem
qkd_one_statement