depth_pos
The declaration extracts the strict positivity of the depth exponent f from any HydraulicExponents triple. Hydrologists working with single-thread alluvial channels cite it when confirming that depth scales positively with discharge under the algebraic σ-conservation constraint. The proof is a direct one-line field projection from the HydraulicExponents structure.
claimLet $(b,f,m)$ be a HydraulicExponents triple, i.e., real numbers satisfying $b+f+m=1$ together with the positivity conditions $b>0$, $f>0$, $m>0$. Then $f>0$.
background
The HydraulicExponents structure encodes the Leopold-Maddock at-a-station hydraulic geometry exponents for single-thread alluvial channels. It consists of real numbers b, f, m for width, depth, and velocity scaling, subject to the closure b + f + m = 1 from σ-conservation on discharge Q = w · d · v, together with the positivity conditions 0 < b, 0 < f, 0 < m. This module derives these properties directly from σ-conservation without fitted parameters. The upstream HydraulicExponents definition supplies the structure whose fields are projected here.
proof idea
The proof is a one-line wrapper that applies the depth_pos field of the HydraulicExponents structure.
why it matters in Recognition Science
This result supplies the positivity of f required by the HydraulicExponents structure and is invoked in the proofs that each exponent is strictly less than one, as well as in the construction of the hydraulicGeometryCert. It closes part of the structural theorem that the exponents sum to one while remaining positive, consistent with the equipartition and Leopold-Maddock partitions. In the Recognition framework it instantiates the σ-conservation closure for hydrology.
scope and limits
- Does not specify the numerical value of f.
- Does not extend to multi-thread or non-alluvial channels.
- Does not incorporate measurement error or regional variations.
- Does not prove the closure identity itself.
Lean usage
example (h : HydraulicExponents) : 0 < h.f := depth_pos hformal statement (Lean)
80theorem depth_pos (h : HydraulicExponents) : 0 < h.f := h.depth_pos