IndisputableMonolith.Hydrology.HydraulicGeometryFromSigma
This module formalizes the Leopold-Maddock at-a-station triple (b, f, m) for single-thread stream reaches under σ-conservation with b + f + m = 1 and all terms positive. Hydrologists and geomorphologists modeling hydraulic geometry would cite the resulting certified exponents. The module supplies the core definitions and supporting lemmas that structure the hydrology application of Recognition Science.
claimThe Leopold-Maddock at-a-station triple $(b, f, m)$ on a single-thread reach satisfies $b, f, m > 0$ and the σ-conservation closure $b + f + m = 1$.
background
The module belongs to the Hydrology domain and imports Constants, where τ₀ is defined as the fundamental RS time quantum equal to 1 tick. It introduces the σ-conservation closure that enforces equipartition among the hydraulic exponents for width, depth, and velocity. The setting applies the Recognition Composition Law and phi-ladder structures to empirical at-a-station relations, with sibling declarations supplying the individual positivity lemmas and the final HydraulicGeometryCert.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the foundational definition of the Leopold-Maddock triple that feeds HydraulicGeometryCert and the equipartitionExponents lemmas within the same module. It fills the step that translates σ-conservation into the positive exponents b, f, m summing to 1, connecting the Recognition Science forcing chain to observed hydraulic geometry.
scope and limits
- Does not derive numerical values for b, f, m.
- Does not treat multi-thread or braided reaches.
- Does not incorporate time-dependent channel evolution.
- Does not address sediment transport or bedload equations.
depends on (1)
declarations in this module (13)
-
structure
HydraulicExponents -
theorem
width_pos -
theorem
depth_pos -
theorem
velocity_pos -
theorem
closure_identity -
theorem
each_lt_one_b -
theorem
each_lt_one_f -
theorem
each_lt_one_m -
def
equipartitionExponents -
def
leopoldMaddockExponents -
structure
HydraulicGeometryCert -
def
hydraulicGeometryCert -
theorem
hydraulic_geometry_one_statement