 122`(0.26, 0.40, 0.34)`: the cluster centre across U.S. Geological
 123Survey single-thread alluvial reaches surveyed in Leopold & Maddock
 1241953 *USGS PP 252* table 4. -/
 125noncomputable def leopoldMaddockExponents : HydraulicExponents where
 126  b := 26 / 100
 127  f := 40 / 100
 128  m := 34 / 100
 129  width_pos := by norm_num
 130  depth_pos := by norm_num
 131  velocity_pos := by norm_num
 132  closure := by norm_num
 133
 134/-! ## §3. Master certificate -/
 135
 136structure HydraulicGeometryCert where
 137  width_pos_of : ∀ h : HydraulicExponents, 0 < h.b
 138  depth_pos_of : ∀ h : HydraulicExponents, 0 < h.f
 139  velocity_pos_of : ∀ h : HydraulicExponents, 0 < h.m
 140  closure_of : ∀ h : HydraulicExponents, h.b + h.f + h.m = 1
 141  equipartition_inhabits : Nonempty HydraulicExponents
 142  empirical_inhabits : Nonempty HydraulicExponents
 143
 144noncomputable def hydraulicGeometryCert : HydraulicGeometryCert where
 145  width_pos_of := width_pos
 146  depth_pos_of := depth_pos
 147  velocity_pos_of := velocity_pos
 148  closure_of := closure_identity
 149  equipartition_inhabits := ⟨equipartitionExponents⟩
 150  empirical_inhabits := ⟨leopoldMaddockExponents⟩
 151
 152/-! ## §4. One-statement summary -/
 153
 154/-- **HYDRAULIC GEOMETRY ONE-STATEMENT.**
 155

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.