hydraulic_geometry_one_statement
plain-language theorem explainer
σ-conservation on the discharge ledger forces every Leopold-Maddock exponent triple (b, f, m) to satisfy b + f + m = 1, and the set of such triples is nonempty. Fluvial geomorphologists cite the result to enforce algebraic closure in at-a-station hydraulic geometry without fitted parameters. The proof is a one-line term that pairs the closure identity lemma with the equipartition witness.
Claim. Every Leopold-Maddock exponent triple of positive reals (b, f, m) satisfies b + f + m = 1, and the set of all such triples is nonempty.
background
The module derives Leopold-Maddock hydraulic geometry from σ-conservation on the discharge ledger Q = w · d · v, which yields the logarithmic identity ln Q = ln w + ln d + ln v and therefore the exponent closure b + f + m = 1. HydraulicExponents is the structure of positive real triples (b, f, m) obeying this closure together with the three positivity conditions. The upstream closure_identity theorem extracts the sum equality directly from the structure field, while equipartitionExponents constructs the zero-prior canonical instance (1/3, 1/3, 1/3).
proof idea
The proof is a one-line term that constructs the conjunction by supplying the closure_identity lemma for the universal quantification over HydraulicExponents and the equipartitionExponents definition as the witness for nonemptiness.
why it matters
The declaration packages the core structural claim of the module, confirming that σ-conservation alone enforces the exponent sum without additional parameters. It supports the later HydraulicGeometryCert and supplies the two canonical partitions referenced in the module documentation. Within the Recognition Science hydrology extension it illustrates how conservation laws constrain observable exponents, consistent with the framework's emphasis on algebraic closure from ledger identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.