module module

`IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (13)

def R_0 L31
def linkRate L34
theorem linkRate_zero L36
theorem linkRate_pos L39
theorem linkRate_strict_anti L43
theorem linkRate_succ L52
def attenuationPerRung L61
theorem attenuationPerRung_pos L63
theorem attenuationPerRung_lt_one L66
theorem attenuationPerRung_band L70
structure CoherenceProtectedQKDLinkBudgetCert L81
def coherenceProtectedQKDLinkBudgetCert L90
theorem qkd_one_statement L102