hack_exponent_eq_half
plain-language theorem explainer
hack_exponent_eq_half establishes that the Hack exponent equals exactly one half under self-similar Hortonian scaling forced by sigma-conservation. Researchers modeling river-basin geometry with recognition trees cite the identity to anchor the lower edge of the empirical Hack range. The term-mode proof unfolds the ratio definition, substitutes the double-log relation, invokes positivity of the length-ratio logarithm, and cancels via field simplification.
Claim. $ h = 1/2 $ where $ h := (log R_l) / (log R_b) $, $ R_l = phi $ is the Horton length ratio, and $ R_b = phi^2 $ is the Horton bifurcation ratio.
background
The module treats a drainage network as a recognition tree on the topographic ledger under sigma-conservation. This forces phi-self-similar Horton scaling with length ratio per order equal to phi and bifurcation ratio equal to phi squared, the same two-phi-step structure that appears in the eight-tick lattice elsewhere in the framework. Hack's law then reads L proportional to A to the power h, and self-similar scaling converts the exponent into the ratio of logarithms of the two ratios.
proof idea
Unfold the definition of hack_exponent to expose the ratio of logs. Rewrite the denominator via log_bifurcation_eq_two_log_length, which supplies log R_b equals two times log R_l. Invoke log_length_ratio_pos to confirm the denominator is positive. Apply field_simp to reduce the ratio directly to one half.
why it matters
The identity is invoked in river_network_one_statement, the headline certified claim that bundles the Horton ratios, the exact Hack exponent, and membership in the empirical band. It realizes the Recognition Science prediction that sigma-conservation on the phi-ladder produces the eight-tick octave, here visible as two phi-steps in bifurcation per single step in length, fixing h at the strict lower bound of observed values. The result closes the structural half of the partial theorem; fractal corrections that could raise the exponent remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.