pith. machine review for the scientific record. sign in
theorem proved term proof high

river_network_one_statement

show as:
view Lean formalization →

Sigma-conservation on a phi-self-similar drainage network forces the Horton bifurcation ratio to equal the square of the length ratio. Hack's exponent is then exactly one half under self-similar scaling. This value sits at the lower end of the empirical Hack band (0.45, 0.65). The proof is a direct term that assembles the ratio identity, the exponent equality, and the numerical band check.

claimUnder sigma-conservation on a phi-self-similar drainage network, the Horton bifurcation ratio satisfies $R_b = R_l^2$, Hack's exponent is $h = 1/2$, and $0.45 < h < 0.65$, where $R_l = phi$ and $R_b = phi^2$.

background

In the Recognition Science treatment of river networks, a drainage basin is modeled as a recognition tree on the topographic ledger. Sigma-conservation enforces self-similar branching with Horton length ratio $R_l = phi$ and bifurcation ratio $R_b = phi^2$. Hack's law states that mainstream length scales with basin area as $L propto A^h$, and under Hortonian scaling the exponent is $h = log R_l / log R_b$ (from the hack_exponent definition). The module proves the structural identity $h = 1/2$ exactly, which lies in the empirical range (0.45, 0.65) reported by Hack (1957) and subsequent catalogs. Upstream results establish the ratio equality $R_b = R_l^2$ from sigma-conservation and the logarithm identity that reduces the exponent to one half.

proof idea

The proof is a term-mode wrapper that directly pairs the bifurcation-equals-length-squared identity, the theorem establishing the exponent equals one half, and the two sides of the empirical band membership.

why it matters in Recognition Science

This statement consolidates the core results of the river-network module, linking sigma-conservation to observed Horton ratios and placing the derived Hack exponent in the empirical band. It parallels the phi-squared ratios arising in the eight-tick octave structure seen in volcanic recurrence and planetary formation. The partial closure notes that fractal-basin corrections, which would raise the exponent toward the upper band, remain outside the present formalization.

scope and limits

formal statement (Lean)

 184theorem river_network_one_statement :
 185    horton_bifurcation_ratio = horton_length_ratio ^ 2 ∧
 186    hack_exponent = 1 / 2 ∧
 187    (0.45 : ℝ) < hack_exponent ∧ hack_exponent < 0.65 :=

proof body

Term-mode proof.

 188  ⟨bifurcation_eq_length_squared, hack_exponent_eq_half,
 189   hack_exponent_in_empirical_band.1, hack_exponent_in_empirical_band.2⟩
 190
 191end
 192
 193end RiverNetworkFromSigmaConservation
 194end Climate
 195end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.