pith. machine review for the scientific record. sign in
def definition def or abbrev high

hack_exponent

show as:
view Lean formalization →

Hack's exponent is the ratio of the logarithm of the Horton length ratio to the logarithm of the Horton bifurcation ratio under self-similar scaling. Geomorphologists working on basin area-length relations cite this definition when connecting φ-forced Horton ratios to Hack's law. It is supplied as a direct abbreviation that substitutes the module's φ-based constants into the logarithmic expression.

claim$h = (log R_l) / (log R_b)$, where $R_l = φ$ is the Horton length ratio and $R_b = φ^2$ is the Horton bifurcation ratio.

background

In this module a drainage network is treated as a recognition tree on the topographic ledger. σ-conservation forces upstream-downstream branching to obey the canonical Horton ratios with length ratio equal to φ and bifurcation ratio equal to φ squared. These ratios are supplied by the upstream definitions: the Horton length ratio encodes per-order length growth on a φ-self-similar network, while the Horton bifurcation ratio encodes tributary count per order as two φ-steps. The local setting is the partial theorem on the structural Hack exponent in the canonical band, with empirical adjudication against world catalogs left open.

proof idea

One-line definition that substitutes the φ-based Horton ratios into the ratio of real logarithms.

why it matters in Recognition Science

This definition supplies the structural Hack exponent shown equal to 1/2 in the downstream theorem hack_exponent_eq_half and assembled into the river network one-statement. It realizes the self-similar Tokunaga-Horton scaling forced by σ-conservation on the eight-tick lattice, placing h exactly at the lower edge of the empirical band (0.45, 0.65). The upper edge remains open for fractal-basin-area corrections not formalized here.

scope and limits

formal statement (Lean)

 125def hack_exponent : ℝ :=

proof body

Definition body.

 126  Real.log horton_length_ratio / Real.log horton_bifurcation_ratio
 127
 128/-- The headline identity: `h = 1/2` exactly. -/

used by (5)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.