linkRate

formal source

  31def R_0 : ℝ := 1
  32
  33/-- Link rate at φ-rung `n` (after `n · L_φ` km of fiber). -/
  34def linkRate (n : ℕ) : ℝ := R_0 / phi ^ n
  35
  36theorem linkRate_zero : linkRate 0 = R_0 := by
  37  unfold linkRate; simp
  38
  39theorem linkRate_pos (n : ℕ) : 0 < linkRate n := by
  40  unfold linkRate R_0
  41  exact div_pos one_pos (pow_pos phi_pos _)
  42
  43theorem linkRate_strict_anti {n m : ℕ} (h : n < m) :
  44    linkRate m < linkRate n := by
  45  unfold linkRate
  46  have hp1 : 0 < phi ^ n := pow_pos phi_pos _
  47  have h_pow : phi ^ n < phi ^ m := pow_lt_pow_right₀ one_lt_phi h
  48  -- R_0 / φ^m < R_0 / φ^n  ↔  φ^n < φ^m (since R_0 > 0).
  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