`linkRate_succ`

proved

show as: view math explainer →

module: IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget
domain: Engineering
line: 52 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Engineering.CoherenceProtectedQKDLinkBudget on GitHub at line 52.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  49  have h_R_pos : (0 : ℝ) < R_0 := by unfold R_0; norm_num
  50  exact div_lt_div_of_pos_left h_R_pos hp1 h_pow
  51
  52theorem linkRate_succ (n : ℕ) :
  53    linkRate (n + 1) = linkRate n / phi := by
  54  unfold linkRate
  55  rw [pow_succ]
  56  field_simp
  57
  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.