log_bifurcation_eq_two_log_length
plain-language theorem explainer
The identity states that the logarithm of the Horton bifurcation ratio equals twice the logarithm of the Horton length ratio under phi-based scaling. Geomorphologists deriving exact Hack exponents from Recognition Science would cite this step when reducing self-similar drainage networks to the canonical band. The proof is a direct algebraic reduction that unfolds the two ratio definitions, applies the logarithm power rule, and finishes with ring simplification.
Claim. $log R_b = 2 log R_l$ where $R_l = phi$ denotes the Horton length ratio and $R_b = phi^2$ denotes the Horton bifurcation ratio.
background
The module derives river networks from sigma-conservation on the topographic ledger, imposing self-similar Tokunaga-Horton scaling. Under this regime the length ratio per Horton order equals phi while the bifurcation ratio equals phi squared, the same two-phi-step structure that appears in the eight-tick octave of the unified forcing chain. The upstream definitions are horton_length_ratio := phi and horton_bifurcation_ratio := phi^2; the lemma self from RecogSpec.Core supplies the phi-closed property used to anchor these ratios.
proof idea
The term proof unfolds horton_bifurcation_ratio and horton_length_ratio, rewrites the resulting power via Real.log_pow, and closes with ring.
why it matters
This identity supplies the algebraic bridge to hack_exponent_eq_half, which concludes that Hack's exponent equals exactly 1/2. It therefore completes the structural half of the RiverNetworkCert record and the empirical-band theorem that follows. The result sits inside the phi-ladder and T7 eight-tick octave of the forcing chain, confirming that the same recurrence producing phi^2 in volcanic and orbital contexts also fixes the drainage scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.