velocity_pos
plain-language theorem explainer
The velocity_pos theorem asserts that the velocity scaling exponent m remains strictly positive for any Leopold-Maddock triple obeying σ-conservation closure with positive components. Hydrologists and fluvial geomorphologists cite it when confirming physical consistency of at-a-station discharge partitioning into width, depth, and velocity. The proof is a direct one-line field projection from the HydraulicExponents structure.
Claim. Let $(b,f,m)$ be a triple of positive reals satisfying the Leopold-Maddock closure $b+f+m=1$. Then $m>0$.
background
The module extends Recognition Science to hydrology by deriving at-a-station hydraulic geometry from σ-conservation on the discharge ledger $Q=w·d·v$, which implies the additive identity $b+f+m=1$ after taking logarithms. HydraulicExponents packages exactly such a triple: three positive reals together with the closure identity and the three positivity fields. The upstream forces structure from MagnitudeOfMismatch supplies the symmetry axiom that makes comparisons single-valued, but the present result rests only on the structure definition itself.
proof idea
This is a one-line term-mode proof that directly returns the velocity_pos field of the supplied HydraulicExponents structure.
why it matters
velocity_pos is a required building block for HydraulicGeometryCert, equipartitionExponents, leopoldMaddockExponents, and the three each_lt_one_* lemmas. It guarantees that the velocity component stays positive under the σ-conservation closure that the module extracts from the discharge identity, thereby completing the positivity half of the Leopold-Maddock partition. The result sits inside the broader Recognition Science program that forces D=3 spatial dimensions and the eight-tick octave from the same functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.