each_lt_one_f
plain-language theorem explainer
The theorem proves that the depth exponent f is strictly less than one for any positive triple (b, f, m) obeying the unit-sum closure. Hydrologists modeling single-thread alluvial channels cite the bound when checking power-law fits to at-a-station discharge data. The argument extracts positivity of b and m from the structure, recalls the closure identity, and concludes via linear arithmetic.
Claim. Let $b, f, m > 0$ be real numbers satisfying $b + f + m = 1$. Then $f < 1$.
background
The module derives Leopold-Maddock at-a-station exponents from sigma-conservation on discharge: $Q = w · d · v$ implies the exact algebraic closure $b + f + m = 1$ under logarithmic differentiation. HydraulicExponents is the structure that packages a positive triple $(b, f, m)$ together with this closure identity; its fields width_pos, depth_pos and velocity_pos record the three positivity assertions. The upstream results width_pos and velocity_pos are simply the projections of those fields out of the structure.
proof idea
The proof obtains $0 < b$ from width_pos and $0 < m$ from velocity_pos, recalls the closure $b + f + m = 1$, and applies linarith to deduce $f < 1$.
why it matters
This result is one of the three symmetric lemmas each_lt_one_b, each_lt_one_f, each_lt_one_m that together certify every exponent lies in $(0,1)$. The lemmas populate the HydraulicGeometryCert and confirm that both the equipartition $(1/3,1/3,1/3)$ and the empirical Leopold-Maddock partition $(0.26,0.40,0.34)$ are admissible. In the Recognition Science setting the bound illustrates how an algebraic closure forced by conservation alone produces concrete dimensional restrictions without fitted parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.