each_lt_one_m
plain-language theorem explainer
The theorem shows that the velocity exponent m in any Leopold-Maddock hydraulic geometry triple is strictly less than one. Hydrologists fitting at-a-station relations on single-thread alluvial channels cite the bound to enforce discharge scaling consistency under σ-conservation. The argument is a direct linarith reduction that pulls positivity of the width and depth exponents together with the sum-to-one closure from the HydraulicExponents structure.
Claim. Let $(b,f,m)$ be real numbers with $b>0$, $f>0$, $m>0$ and $b+f+m=1$. Then $m<1$.
background
HydraulicExponents is the structure that packages the Leopold-Maddock at-a-station triple for single-thread alluvial channels: three positive reals b (width scaling), f (depth scaling), m (velocity scaling) together with the algebraic closure b + f + m = 1 forced by σ-conservation on the discharge ledger Q = w · d · v. The module derives this closure directly from the logarithmic form of the continuity equation and then proves each exponent is strictly less than one. The local theoretical setting is the plan-v7 extension of Recognition Science to hydrology, where σ-conservation supplies the only constraint and no fitted parameters are introduced.
proof idea
The term proof first obtains 0 < b from the width_pos field and 0 < f from the depth_pos field. It then extracts the equality b + f + m = 1 from the closure field. Linarith is applied to these three facts to conclude m < 1.
why it matters
The result supplies one of the three strict inequalities required by the master HydraulicGeometryCert and confirms that both the equipartition witness (1/3,1/3,1/3) and the Leopold-Maddock central-tendency witness (0.26,0.40,0.34) remain admissible. It instantiates the σ-conservation identity at the level of empirical channel geometry and closes the individual bounds that follow from the T0-T8 forcing chain once the discharge ledger is recognized. No open scaffolding remains for this specific bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.