HydraulicGeometryCert
plain-language theorem explainer
HydraulicGeometryCert packages the universal positivity and closure properties of every HydraulicExponents triple together with inhabitedness witnesses for the equipartition and Leopold-Maddock cases. Channel hydrologists would cite the certificate when deriving at-a-station relations from discharge conservation alone. The declaration is a plain structure definition that records the six fields without invoking any lemmas or tactics.
Claim. A certificate asserting that every triple of positive reals $(b,f,m)$ with $b+f+m=1$ satisfies the strict inequalities $0<b$, $0<f$, $0<m$, together with the existence of such triples for the equipartition partition and for the empirical central values $(0.26,0.40,0.34)$.
background
The module develops an extension of Recognition Science to hydrology by showing that σ-conservation on the discharge ledger $Q=w·d·v$ forces the hydraulic geometry exponents to obey $b+f+m=1$. HydraulicExponents is the structure that collects positive real numbers $b,f,m$ satisfying this algebraic closure. The present declaration supplies the master certificate that asserts these properties hold universally for the structure and that both the zero-prior equipartition triple and the Leopold-Maddock empirical triple are inhabited.
proof idea
The declaration consists of a structure definition whose six fields are the quantified statements over HydraulicExponents for the three positivity conditions, the closure identity, and the two Nonempty assertions. No proof steps or external lemmas are required; the structure directly encodes the certificate.
why it matters
The structure completes the master certificate in §3 of the module, supplying the bundled properties that the downstream hydraulicGeometryCert instantiates explicitly. It demonstrates how the Recognition framework's conservation laws constrain empirical hydraulic relations without fitted parameters, linking the algebraic closure to both theoretical equipartition and field data from Leopold & Maddock 1953.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.