closure_identity
plain-language theorem explainer
The closure identity asserts that the Leopold-Maddock exponents b, f, m for width, depth, and velocity on a single-thread alluvial channel sum exactly to one. Fluvial geomorphologists cite it when enforcing discharge conservation in power-law models without fitted parameters. The proof is a direct field projection from the HydraulicExponents structure.
Claim. Let $(b, f, m)$ be positive real numbers that form the Leopold-Maddock at-a-station exponents for a single-thread alluvial channel under discharge conservation. Then $b + f + m = 1$.
background
The HydraulicExponents structure encodes the Leopold-Maddock triple $(b, f, m)$ for width, depth, and velocity exponents on a single-thread reach. It requires each component positive and the algebraic closure $b + f + m = 1$. This module derives the closure from σ-conservation on the discharge ledger $Q = w · d · v$, which implies ln Q = ln w + ln d + ln v and thus the exponent sum equals one.
proof idea
The proof is a one-line term that projects the closure field from the input HydraulicExponents structure.
why it matters
This identity supplies the algebraic constraint used by hydraulicGeometryCert and hydraulic_geometry_one_statement. It realizes the module proposition that σ-conservation alone forces the exponent sum to one, independent of the specific partition chosen. The result parallels ledger-derived conservation laws elsewhere in the framework and leaves open the quantitative bound on measurement error that would falsify observed deviations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.