hydraulicGeometryCert
plain-language theorem explainer
The hydraulicGeometryCert assembles positivity of the width, depth, and velocity exponents together with their sum-to-one closure and two canonical partitions into a single certificate structure. Fluvial geomorphologists modeling single-thread alluvial channels would cite it to guarantee that sigma-conservation on discharge enforces the Leopold-Maddock relation without fitted parameters. The definition proceeds by direct record construction that references the module's sibling lemmas on positivity and closure.
Claim. The certificate asserts that for any HydraulicExponents triple $(b, f, m)$, one has $0 < b$, $0 < f$, $0 < m$, and $b + f + m = 1$, while also witnessing the existence of the equipartition triple $(1/3, 1/3, 1/3)$ and the empirical central-tendency triple $(0.26, 0.40, 0.34)$.
background
In the Recognition Science hydrology extension, sigma-conservation on the discharge ledger $Q = w · d · v$ forces the logarithmic derivatives (exponents $b$ for width, $f$ for depth, $m$ for velocity) to obey $b + f + m = 1$. The HydraulicExponents structure encodes positive reals satisfying this algebraic closure. Upstream results supply the individual positivity theorems width_pos, depth_pos, velocity_pos and the closure_identity theorem that directly yields the sum constraint from sigma-conservation alone.
proof idea
The definition is a direct record construction that populates the six fields of HydraulicGeometryCert by referencing the corresponding sibling definitions: width_pos_of is assigned width_pos, depth_pos_of is assigned depth_pos, velocity_pos_of is assigned velocity_pos, closure_of is assigned closure_identity, equipartition_inhabits is assigned the nonempty witness from equipartitionExponents, and empirical_inhabits is assigned the witness from leopoldMaddockExponents.
why it matters
This declaration supplies the master certificate completing the module's structural theorem on Leopold-Maddock exponents under sigma-conservation. It directly supports the one-statement summary that sigma-conservation forces every exponent triple to satisfy $b + f + m = 1$ with the equipartition and empirical partitions as inhabitants. In the framework it extends the forcing chain to hydrology by deriving exponent relations from conservation alone, consistent with the Recognition Composition Law and the absence of free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.