def
definition
coherenceProtectedQKDLinkBudgetCert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget on GitHub at line 90.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
87 attenuation_lt_one : attenuationPerRung < 1
88 attenuation_band : (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622
89
90def coherenceProtectedQKDLinkBudgetCert :
91 CoherenceProtectedQKDLinkBudgetCert where
92 rate_zero := linkRate_zero
93 rate_pos := linkRate_pos
94 rate_strict_anti := @linkRate_strict_anti
95 rate_succ := linkRate_succ
96 attenuation_pos := attenuationPerRung_pos
97 attenuation_lt_one := attenuationPerRung_lt_one
98 attenuation_band := attenuationPerRung_band
99
100/-- **QKD ONE-STATEMENT.** Link rate `R(n) = R_0 · φ^(-n)`,
101strictly anti-monotonic; per-rung attenuation `1/φ ∈ (0.617, 0.622)`. -/
102theorem qkd_one_statement :
103 (∀ n, linkRate (n + 1) = linkRate n / phi) ∧
104 (∀ {n m : ℕ}, n < m → linkRate m < linkRate n) ∧
105 (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622 :=
106 ⟨linkRate_succ, @linkRate_strict_anti,
107 attenuationPerRung_band.1, attenuationPerRung_band.2⟩
108
109end
110
111end CoherenceProtectedQKDLinkBudget
112end Engineering
113end IndisputableMonolith