pith. machine review for the scientific record. sign in
structure definition def or abbrev

RiverNetworkCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (5)

Lean names referenced from this declaration's body.