RiverNetworkCert
plain-language theorem explainer
RiverNetworkCert packages the structural properties of a self-similar drainage network under σ-conservation, asserting that the Horton length ratio equals φ, the bifurcation ratio equals φ², their logarithmic relation holds, and that Hack's exponent is exactly 1/2 within the empirical band (0.45, 0.65). A geomorphologist applying Recognition Science to river basins would cite this certificate to ground Hack's law in the φ-ladder without external parameters. The declaration is a structure definition that directly assembles the positivity, square
Claim. Let $R_l = φ$ be the Horton length ratio and $R_b = φ^2$ the Horton bifurcation ratio. The structure certifies $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$, and that the Hack exponent $h = log R_l / log R_b$ satisfies $h = 1/2$ with $0.45 < h < 0.65$.
background
In the Recognition Science treatment of river networks, a drainage basin is modeled as a recognition tree on the topographic ledger. σ-conservation imposes self-similar Horton scaling with length ratio $R_l = φ$ and bifurcation ratio $R_b = φ^2$, where φ is the golden ratio fixed point from the J-uniqueness theorem. Hack's law then follows as $L ∝ A^h$ with exponent $h = log R_l / log R_b$ (MODULE_DOC). Upstream lemmas establish the core identities: bifurcation_eq_length_squared shows $R_b = R_l^2$, log_bifurcation_eq_two_log_length shows the doubling of the logarithm, and hack_exponent defines $h$ as the ratio of logs. The module proves the structural identity $h = 1/2$ exactly under these ratios, together with the positivity and ordering conditions required for a valid network.
proof idea
The declaration is a structure definition whose fields are populated by direct references to sibling results. Each field pulls the corresponding positivity statement, the equality theorems bifurcation_eq_length_squared and log_bifurcation_eq_two_log_length, the definition of hack_exponent, and the band check from hack_exponent_in_empirical_band. No tactics are required beyond the assembly of these prior facts.
why it matters
RiverNetworkCert serves as the master certificate in §4 of the module, feeding directly into the construction of riverNetworkCert. It closes the structural derivation of Hack's exponent from the φ-ladder forced by σ-conservation. The result connects to the broader Recognition framework through the self-similar fixed point (T6) and the eight-tick lattice (T7), reproducing the same φ² ratio that appears in eruption recurrence and orbital gaps. An open question remains the empirical adjudication against HydroSHEDS or USGS data to confirm the band (0.45, 0.65) holds in real basins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.