hack_exponent

formal source

 122
 123/-- Hack's exponent under self-similar Hortonian scaling:
 124  `h = log R_l / log R_b`. -/
 125def hack_exponent : ℝ :=
 126  Real.log horton_length_ratio / Real.log horton_bifurcation_ratio
 127
 128/-- The headline identity: `h = 1/2` exactly. -/
 129theorem hack_exponent_eq_half : hack_exponent = 1 / 2 := by
 130  unfold hack_exponent
 131  rw [log_bifurcation_eq_two_log_length]
 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