def
definition
attenuationPerRung
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget on GitHub at line 61.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
58/-! ## §2. Attenuation factor per L_φ -/
59
60/-- Per-rung attenuation factor `= 1/φ ≈ 0.618`. -/
61def attenuationPerRung : ℝ := 1 / phi
62
63theorem attenuationPerRung_pos : 0 < attenuationPerRung :=
64 div_pos one_pos phi_pos
65
66theorem attenuationPerRung_lt_one : attenuationPerRung < 1 := by
67 unfold attenuationPerRung
68 rw [div_lt_one phi_pos]; exact one_lt_phi
69
70theorem attenuationPerRung_band :
71 (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622 := by
72 unfold attenuationPerRung
73 have h1 := phi_gt_onePointSixOne
74 have h2 := phi_lt_onePointSixTwo
75 refine ⟨?_, ?_⟩
76 · rw [lt_div_iff₀ phi_pos]; linarith
77 · rw [div_lt_iff₀ phi_pos]; linarith
78
79/-! ## §3. Master certificate -/
80
81structure CoherenceProtectedQKDLinkBudgetCert where
82 rate_zero : linkRate 0 = R_0
83 rate_pos : ∀ n, 0 < linkRate n
84 rate_strict_anti : ∀ {n m : ℕ}, n < m → linkRate m < linkRate n
85 rate_succ : ∀ n, linkRate (n + 1) = linkRate n / phi
86 attenuation_pos : 0 < attenuationPerRung
87 attenuation_lt_one : attenuationPerRung < 1
88 attenuation_band : (0.617 : ℝ) < attenuationPerRung ∧ attenuationPerRung < 0.622
89
90def coherenceProtectedQKDLinkBudgetCert :
91 CoherenceProtectedQKDLinkBudgetCert where