linkRate_strict_anti

formal source

  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
  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