horton_length_ratio_gt_one
plain-language theorem explainer
The theorem asserts that the Horton length ratio exceeds one in the Recognition Science model of drainage networks. Researchers deriving self-similar basin scaling or assembling network certificates would cite this when confirming ordering properties under σ-conservation. The proof is a one-line wrapper that directly invokes the established inequality 1 < phi.
Claim. $1 < R_l$ where $R_l$ is the Horton length ratio, defined as the per-order length growth factor on a φ-self-similar drainage network and equal to the golden ratio φ.
background
River networks arise as recognition trees on the topographic ledger. σ-conservation forces the upstream/downstream branching to obey the canonical Horton ratios length ratio R_l = φ and bifurcation ratio R_b = φ². The Horton length ratio is defined as the per-order length growth on such a network and equals φ. The upstream lemma one_lt_phi establishes that the golden ratio satisfies 1 < φ, with proofs available in Constants, PhiSupport, and PhiSupport.Lemmas.
proof idea
The proof is a one-line wrapper that applies the lemma one_lt_phi establishing 1 < phi.
why it matters
This supplies one of the ordering properties collected by the riverNetworkCert definition, which also includes length_ratio_pos, bifurcation_ratio_pos, bifurcation_ratio_gt_one, and bifurcation_eq_length_squared. It supports the structural derivation of Hack's exponent h = log R_l / log R_b = 1/2. The construction aligns with the eight-tick octave and φ-ladder landmarks in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.