horton_bifurcation_ratio_gt_one

formal source

  87
  88theorem horton_length_ratio_gt_one : 1 < horton_length_ratio := one_lt_phi
  89
  90theorem horton_bifurcation_ratio_gt_one : 1 < horton_bifurcation_ratio := by
  91  unfold horton_bifurcation_ratio
  92  have : (1 : ℝ) < phi := one_lt_phi
  93  nlinarith [phi_pos, one_lt_phi]
  94
  95/-- Two-step identity: `R_b = R_l^2`. The σ-conservation forcing in
  96  one statement: bifurcation per order is two length-steps per order. -/
  97theorem bifurcation_eq_length_squared :
  98    horton_bifurcation_ratio = horton_length_ratio ^ 2 := rfl
  99
 100/-! ## §2. Logarithms of the Horton ratios -/
 101
 102/-- `log R_l = log φ > 0`. -/
 103theorem log_length_ratio_pos : 0 < Real.log horton_length_ratio := by
 104  unfold horton_length_ratio
 105  exact Real.log_pos one_lt_phi
 106
 107/-- `log R_b = 2 · log φ > 0`. -/
 108theorem log_bifurcation_ratio_pos : 0 < Real.log horton_bifurcation_ratio := by
 109  unfold horton_bifurcation_ratio
 110  rw [Real.log_pow]
 111  have hlog : 0 < Real.log phi := Real.log_pos one_lt_phi
 112  positivity
 113
 114/-- `log R_b = 2 · log R_l`. -/
 115theorem log_bifurcation_eq_two_log_length :
 116    Real.log horton_bifurcation_ratio = 2 * Real.log horton_length_ratio := by
 117  unfold horton_bifurcation_ratio horton_length_ratio
 118  rw [Real.log_pow]
 119  ring
 120