IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget
This module defines reference link rates at zero distance along with rung-dependent attenuation and positivity properties for coherence-protected QKD in RS-native units. Quantum communication engineers would cite these when assembling link budgets from the imported constants and cost structures. The module consists of sequential definitions and basic lemmas establishing monotonicity without a central theorem.
claimLet $R_0$ denote the reference link rate at zero distance. The link rate function $R(r)$ and attenuation per rung are defined such that $R(0) = R_0$, $R(r) > 0$, and the rate is strictly decreasing in the rung index.
background
The module sits in the Engineering domain and imports the RS time quantum from Constants together with cost functions from the Cost module. Constants supplies the fundamental time quantum with the property that it equals one tick in RS-native units. The sibling definitions introduce rung-indexed rates and attenuation factors that align with the self-similar ladder structure of the broader framework.
proof idea
this is a definition module, no proofs
why it matters in Recognition Science
The module supplies the rate and attenuation primitives that support coherence-protected QKD link budget certification within the Recognition Science framework. It connects the imported constants and cost foundations to engineering calculations that rely on the phi-ladder and eight-tick octave structure.
scope and limits
- Does not incorporate security proofs or eavesdropping models for QKD.
- Does not compute explicit numerical budgets for finite distances.
- Does not address classical channel losses or detector inefficiencies.
- Does not extend to multi-link network topologies.
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