pith. sign in
module module high

IndisputableMonolith.Hydrology.HydraulicGeometryFromSigma

show as:
view Lean formalization →

The module defines the Leopold-Maddock at-a-station triple (b, f, m) for single-thread stream reaches under sigma conservation. It requires all exponents positive and enforces the closure b + f + m = 1. Hydrologists and geomorphologists cite it when applying Recognition Science to channel geometry. The structure consists of exponent definitions, positivity results, and a certification theorem.

claimThe Leopold-Maddock triple $(b, f, m)$ on a single-thread reach satisfies $b + f + m = 1$ with $b, f, m > 0$.

background

Recognition Science applies its conservation laws to hydrology through the sigma parameter. This module imports the base time quantum from Constants and focuses on channel geometry. The Leopold-Maddock triple (b, f, m) captures at-a-station hydraulic relations for single-thread reaches. The module enforces positivity of each exponent and the closure condition b + f + m = 1.

proof idea

This is a definition module, no proofs. It assembles the HydraulicExponents definition, positivity lemmas for each component, the closure identity, and the HydraulicGeometryCert.

why it matters in Recognition Science

The module supplies the hydraulic geometry foundation that supports downstream applications in Recognition Science modeling of physical systems. It realizes the Leopold-Maddock relations as a direct consequence of sigma conservation in the framework.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)