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

leopoldMaddockExponents

show as:
view Lean formalization →

leopoldMaddockExponents supplies the empirical central-tendency triple (0.26, 0.40, 0.34) as a concrete instance of the hydraulic exponents structure. Fluvial geomorphologists cite it when comparing observed at-a-station width-depth-velocity scaling in alluvial channels to the discharge closure constraint. The definition assigns the three fractions directly and discharges the positivity and summation obligations by norm_num.

claimThe empirical central-tendency hydraulic geometry exponents are the record with width exponent $b = 0.26$, depth exponent $f = 0.40$, velocity exponent $m = 0.34$, satisfying $0 < b$, $0 < f$, $0 < m$ and $b + f + m = 1$.

background

The hydraulic exponents structure encodes the at-a-station scaling exponents for channel width (b), depth (f) and velocity (m). These three real numbers must each be positive and sum exactly to one; the sum-to-one condition follows directly from the discharge identity Q = w · d · v by taking logarithms and differentiating with respect to a reference discharge.

proof idea

The definition constructs the record by assigning b := 26/100, f := 40/100, m := 34/100. The three positivity fields and the closure field are each discharged by a single norm_num tactic.

why it matters in Recognition Science

This definition supplies the empirical witness that, together with the equipartition triple, populates the master hydraulic geometry certificate. It shows that the algebraic closure forced by σ-conservation on the discharge ledger accommodates the central tendency reported in Leopold & Maddock 1953 USGS PP 252 without additional parameters.

scope and limits

formal statement (Lean)

 125noncomputable def leopoldMaddockExponents : HydraulicExponents where
 126  b := 26 / 100

proof body

Definition body.

 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

used by (1)

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

depends on (4)

Lean names referenced from this declaration's body.