hack_exponent_in_empirical_band
plain-language theorem explainer
The Hack exponent h under self-similar Hortonian scaling satisfies 0.45 < h < 0.65. Hydrologists citing basin scaling laws would use this to confirm the Recognition Science structural prediction against catalogs. The proof reduces the claim to the exact identity h = 1/2 via a prior lemma then discharges the numerical bounds by direct computation.
Claim. Let $h = h = (log R_l) / (log R_b)$ where $R_l = phi$ is the Horton length ratio and $R_b = phi^2$ the bifurcation ratio forced by sigma-conservation. Then $0.45 < h < 0.65$.
background
In the Recognition Science treatment of river networks, sigma-conservation on a phi-self-similar drainage network forces the Horton length ratio $R_l = phi$ and bifurcation ratio $R_b = phi^2$. Hack's exponent is defined as $h = log R_l / log R_b$ (upstream doc: 'Hack's exponent under self-similar Hortonian scaling'). The module proves the structural identity $h = 1/2$ exactly and checks its position inside the empirical band (0.45, 0.65) reported by Hack 1957 and Rigon et al. 1996. The lower end matches the strict self-similar value while the upper end accommodates fractal-basin-area corrections not formalized here (module doc). Upstream, hack_exponent_eq_half establishes the headline identity $h = 1/2$ using log_bifurcation_eq_two_log_length and positivity of the logarithms.
proof idea
The proof is a term-mode wrapper. It rewrites the target inequality by applying the lemma hack_exponent_eq_half, reducing the claim to 0.45 < 1/2 < 0.65. The two resulting inequalities are then discharged directly by norm_num.
why it matters
This theorem supplies the numerical band check required by the master certificate river_network_one_statement, which assembles the full claim that sigma-conservation forces $R_b = R_l^2$, $h = 1/2$, and $0.45 < h < 0.65$. It closes the structural part of Track P2 while leaving fractal corrections open. The result rests on the phi-forced Horton ratios that arise from the eight-tick octave (T7) and the self-similar fixed point (T6) in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.