width_pos
plain-language theorem explainer
The declaration states that the width exponent b is strictly positive for any Leopold-Maddock triple of positive reals that sum to one under σ-conservation. Hydrologists deriving at-a-station scaling relations for single-thread alluvial channels cite it to enforce positivity before bounding the remaining exponents. The proof is a direct field projection from the HydraulicExponents structure.
Claim. Let $(b, f, m)$ be real numbers satisfying $b > 0$, $f > 0$, $m > 0$ and $b + f + m = 1$. Then $b > 0$.
background
The module encodes the Leopold-Maddock at-a-station hydraulic geometry as a triple of scaling exponents $(b, f, m)$ for width, depth and velocity. These satisfy the algebraic closure $b + f + m = 1$ forced by σ-conservation on the discharge ledger $Q = w · d · v$. HydraulicExponents packages exactly this data: three positive reals summing to one, with the positivity axioms and closure recorded as structure fields.
proof idea
The proof is a one-line field projection that returns the width_pos component of the supplied HydraulicExponents record.
why it matters
width_pos supplies the positivity hypothesis required by each_lt_one_f, each_lt_one_m and the master hydraulicGeometryCert. It therefore participates in the structural theorem that all three exponents lie strictly between zero and one while summing to one. The result closes the positivity half of the σ-conservation argument before the module exhibits the equipartition and Leopold-Maddock witnesses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.