hack_exponent_pos

formal source

 132  have hpos : 0 < Real.log horton_length_ratio := log_length_ratio_pos
 133  field_simp
 134
 135theorem hack_exponent_pos : 0 < hack_exponent := by
 136  rw [hack_exponent_eq_half]
 137  norm_num
 138
 139/-- `h` sits in the empirical Hack band `(0.45, 0.65)`. The lower end of
 140the empirical range is the strict self-similar value; the upper end
 141catches fractal-basin-area corrections not formalized here. -/
 142theorem hack_exponent_in_empirical_band :
 143    (0.45 : ℝ) < hack_exponent ∧ hack_exponent < 0.65 := by
 144  rw [hack_exponent_eq_half]
 145  refine ⟨?_, ?_⟩
 146  · norm_num
 147  · norm_num
 148
 149/-! ## §4. Master certificate -/
 150
 151structure RiverNetworkCert where
 152  length_ratio_pos : 0 < horton_length_ratio
 153  bifurcation_ratio_pos : 0 < horton_bifurcation_ratio
 154  length_ratio_gt_one : 1 < horton_length_ratio
 155  bifurcation_ratio_gt_one : 1 < horton_bifurcation_ratio
 156  bifurcation_eq_length_squared :
 157    horton_bifurcation_ratio = horton_length_ratio ^ 2
 158  log_length_pos : 0 < Real.log horton_length_ratio
 159  log_bifurcation_pos : 0 < Real.log horton_bifurcation_ratio
 160  log_bifurcation_eq_two_log_length :
 161    Real.log horton_bifurcation_ratio = 2 * Real.log horton_length_ratio
 162  hack_eq_half : hack_exponent = 1 / 2
 163  hack_in_band : (0.45 : ℝ) < hack_exponent ∧ hack_exponent < 0.65
 164
 165def riverNetworkCert : RiverNetworkCert where