riverNetworkCert
plain-language theorem explainer
The declaration packages a certificate asserting that σ-conservation on a φ-self-similar drainage network forces Horton length ratio φ and bifurcation ratio φ², which in turn fixes Hack's exponent at exactly 1/2 inside the empirical band. Geomorphologists modeling river networks under Recognition Science would cite it to derive the scaling law from the underlying conservation principle. The construction is a direct record of pre-established positivity, ordering, and equality lemmas for the ratios and the exponent.
Claim. Let $R_l$ denote the Horton length ratio and $R_b$ the bifurcation ratio on a drainage network. The certificate states that $0 < R_l$, $0 < R_b$, $1 < R_l$, $1 < R_b$, $R_b = R_l^2$, $0 < log R_l$, $0 < log R_b$, $log R_b = 2 log R_l$, the Hack exponent $h = 1/2$, and $0.45 < h < 0.65$.
background
In the module on river networks from σ-conservation, a drainage network is modeled as a recognition tree obeying σ-conservation. This forces the upstream/downstream branching to satisfy the canonical Horton ratios $R_l = φ$ and $R_b = φ^2$, where φ is the golden ratio fixed point from the self-similar forcing chain. Hack's law then follows as $L ∝ A^h$ with $h = log R_l / log R_b = 1/2$ exactly. The RiverNetworkCert structure collects the required positivity and ordering statements together with the key identities. Upstream results include the theorem that bifurcation ratio equals length ratio squared, which encodes the two-step identity from σ-conservation, and the direct computation that the Hack exponent equals one half. The local setting is Track P2 of Plan v7, providing the structural identity while leaving fractal-basin-area corrections for later closure.
proof idea
The definition is a one-line wrapper that directly assigns the pre-proved lemmas horton_length_ratio_pos, horton_bifurcation_ratio_pos, horton_length_ratio_gt_one, horton_bifurcation_ratio_gt_one, bifurcation_eq_length_squared, log_length_ratio_pos, log_bifurcation_ratio_pos, log_bifurcation_eq_two_log_length, hack_exponent_eq_half, and hack_exponent_in_empirical_band to the corresponding fields of the RiverNetworkCert structure.
why it matters
This definition supplies the bundled certificate for the partial theorem on river networks, which demonstrates that σ-conservation plus φ-self-similarity recovers the observed Hack exponent at the lower end of the empirical range. It sits downstream of the Horton ratio theorems and the bifurcation identity, and feeds the broader claim that the eight-tick lattice structure appears in drainage networks as it does in volcanic recurrence and planetary orbits. The open question it touches is the attribution of the upper empirical band to fractal corrections not yet formalized.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.