hack_exponent_pos
plain-language theorem explainer
The theorem establishes that the Hack exponent is strictly positive under self-similar Hortonian scaling. Geomorphologists and climate modelers working in Recognition Science cite it to confirm the scaling exponent lies in the admissible positive range required by drainage-network laws. The proof is a one-line wrapper that rewrites the claim via the equality to one half and applies norm_num.
Claim. $0 < h$ where $h = (log R_l) / (log R_b)$, $R_l = phi$ is the length ratio, and $R_b = phi^2$ is the bifurcation ratio.
background
In the Recognition Science treatment of river networks, drainage basins are modeled as recognition trees on the topographic ledger. Sigma-conservation enforces the canonical Horton ratios: length ratio $R_l = phi$ and bifurcation ratio $R_b = phi^2$. The Hack exponent is defined as $h = log R_l / log R_b$ under self-similar Tokunaga-Horton scaling. This module establishes the structural identity $h = 1/2$ exactly, with the empirical band (0.45, 0.65) left for numerical adjudication against HydroSHEDS data. The upstream result states: 'The headline identity: h = 1/2 exactly.'
proof idea
The proof is a one-line wrapper. It rewrites the target inequality using the theorem that reduces the Hack exponent to one half, then applies norm_num to verify that zero is strictly less than one half.
why it matters
This theorem closes the positivity requirement for the Hack exponent, ensuring the logarithm in the definition is well-defined and the scaling exponent is positive. It supports the claim that sigma-conservation forces Horton ratios leading to the structural value h = 1/2 at the lower end of the empirical band. The result ties into the eight-tick lattice structure that produces phi-squared ratios in volcanic recurrence and planetary orbits. The module remains partial pending empirical confirmation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.