equipartitionExponents
plain-language theorem explainer
The equipartitionExponents definition supplies the zero-prior canonical triple (1/3, 1/3, 1/3) for Leopold-Maddock hydraulic geometry exponents under σ-conservation. Fluvial geomorphologists modeling single-thread alluvial channels cite it as the balanced partition when no axis is preferred. The definition constructs the HydraulicExponents record directly and verifies positivity plus closure via norm_num reductions.
Claim. The equipartition exponents are defined by $b = f = m = 1/3$, forming a HydraulicExponents triple with $b > 0$, $f > 0$, $m > 0$ and $b + f + m = 1$.
background
The module Hydraulic Geometry from σ-Conservation encodes the Leopold-Maddock at-a-station exponents via the structure HydraulicExponents, which requires positive b (width), f (depth), m (velocity) together with the algebraic closure b + f + m = 1. This closure follows from σ-conservation on the discharge ledger Q = w · d · v, which implies ln Q = ln w + ln d + ln v and therefore the exponent sum equals 1. The equipartition triple is presented as the canonical zero-prior partition when no axis is favored. Upstream results include the RS-native units U and the field-extraction theorems width_pos, depth_pos, velocity_pos that confirm the positivity conditions.
proof idea
This is a definition that constructs the HydraulicExponents record by setting b := 1/3, f := 1/3, m := 1/3 and discharges the three positivity fields plus the closure field via norm_num tactics.
why it matters
This definition supplies the zero-prior canonical partition required by hydraulicGeometryCert and the hydraulic_geometry_one_statement theorem. It completes the pair of inhabited witnesses (equipartition and the empirical Leopold-Maddock triple) that demonstrate σ-conservation forces every valid exponent triple to sum to 1. In the Recognition Science framework it illustrates how a conservation identity analogous to the Recognition Composition Law produces balanced partitions in the absence of priors, here yielding equal exponents that sum to unity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.