horton_length_ratio_pos
plain-language theorem explainer
The theorem establishes positivity of the Horton length ratio, defined as the golden ratio φ on a self-similar drainage network forced by σ-conservation. Researchers deriving structural Hack exponents from Recognition Science would cite it to confirm the length growth factor exceeds zero before assembling network certificates. The proof is a one-line wrapper that invokes the known positivity of φ.
Claim. $0 < R_l$ where $R_l = φ$ is the Horton length ratio (per-order length growth on a φ-self-similar drainage network).
background
The module treats a drainage network as a recognition tree on the topographic ledger under σ-conservation. This forces upstream/downstream branching to obey canonical Horton ratios with length ratio $R_l = φ$ and bifurcation ratio $R_b = φ^2$, the same eight-tick lattice structure that appears in volcanic recurrence and planetary gap rules. The upstream definition simply sets the length ratio equal to phi, the self-similar fixed point of the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the positivity lemma for phi.
why it matters
This supplies the positivity field inside the riverNetworkCert definition that aggregates all Horton ratio properties. It supports the structural identity $h = 1/2$ for Hack's exponent under the forced ratios, consistent with the T7 eight-tick octave and phi-ladder. The module leaves numerical band checks against empirical $h ∈ (0.5, 0.65)$ as an open empirical task.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.