horton_bifurcation_ratio_gt_one
plain-language theorem explainer
The theorem establishes that the Horton bifurcation ratio exceeds one in the Recognition Science model of river networks. Geomorphologists deriving self-similar drainage scaling from sigma-conservation would cite it when confirming positive branching. The proof unfolds the definition to phi squared and closes the inequality with nonlinear arithmetic on the known fact that one is less than phi.
Claim. In the sigma-conservation model the Horton bifurcation ratio satisfies $1 < R_b$ where $R_b = phi^2$.
background
The module models a drainage network as a recognition tree on the topographic ledger. Sigma-conservation forces upstream-downstream branching to obey the canonical Horton ratios length ratio R_l = phi and bifurcation ratio R_b = phi squared, with the latter defined directly as phi^2 to encode two phi-steps in tributary count per order. This construction sits inside the Recognition Science forcing chain where phi is the self-similar fixed point (T6) and the eight-tick octave supplies the phi-squared structure also seen in volcanic recurrence and planetary gap rules.
proof idea
The term proof first unfolds the definition of horton_bifurcation_ratio to obtain phi^2. It then introduces the fact 1 < phi from the upstream lemma one_lt_phi. Nonlinear arithmetic with phi_pos and one_lt_phi immediately yields the target inequality.
why it matters
The result supplies the bifurcation-ratio positivity certificate required by the downstream riverNetworkCert definition that collects all structural Horton properties for the Hack-exponent derivation. It completes the positivity half of the module's claim that R_b = phi squared, which together with the length-ratio facts produces h = 1/2 under Tokunaga-Horton scaling. The step therefore anchors the structural identity asserted in the module doc for the canonical band of Hack's exponent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.