each_lt_one_b
plain-language theorem explainer
The declaration shows that the width exponent b in any Leopold-Maddock hydraulic geometry triple is strictly less than one. Modelers of single-thread alluvial channels cite this bound when deriving scaling relations from discharge measurements. The proof extracts positivity of the other two exponents and the sum-to-one identity, then applies linear arithmetic.
Claim. Let $(b, f, m)$ be positive real numbers satisfying $b + f + m = 1$. Then $b < 1$.
background
The module derives at-a-station hydraulic geometry exponents from σ-conservation on the discharge ledger Q = w · d · v, which implies b + f + m = 1 after logarithmic differentiation. HydraulicExponents is the structure recording a positive triple (b, f, m) with this exact closure. The upstream lemmas depth_pos and velocity_pos simply project the positivity fields f > 0 and m > 0 from the structure.
proof idea
The term proof first obtains 0 < f and 0 < m by applying the depth_pos and velocity_pos projections to the hypothesis h. It then recalls the closure identity b + f + m = 1 from the structure. Linear arithmetic (linarith) immediately yields b < 1 from these three facts.
why it matters
This bound is one of three symmetric inequalities that together guarantee each exponent lies in (0,1). It completes the structural description of HydraulicExponents before the master certificate HydraulicGeometryCert is formed. The result follows directly from σ-conservation and supports empirical checks against Leopold-Maddock data without introducing fitted parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.