log_bifurcation_ratio_pos
plain-language theorem explainer
The declaration proves that the natural logarithm of the Horton bifurcation ratio is strictly positive. Researchers modeling river networks under Recognition Science would cite it to confirm log R_b > 0 when R_b equals phi squared. The proof is a short term-mode reduction that unfolds the definition, applies the logarithm power rule, invokes the positivity of log phi, and closes with the positivity tactic.
Claim. $0 < log R_b$ where $R_b = phi^2$ is the Horton bifurcation ratio.
background
The module interprets drainage networks as recognition trees on the topographic ledger under sigma-conservation. This forces the canonical Horton ratios length ratio R_l = phi and bifurcation ratio R_b = phi squared, which in turn yields Hack's exponent h = log R_l / log R_b = 1/2. The upstream definition horton_bifurcation_ratio sets the ratio to phi squared, representing tributary count per order as two phi-steps. The lemma one_lt_phi establishes phi > 1 and is quoted in the proof to guarantee that log phi is positive.
proof idea
The proof unfolds horton_bifurcation_ratio to phi squared. It rewrites the logarithm via Real.log_pow to obtain two times log phi. The upstream lemma one_lt_phi supplies 0 < log phi, after which the positivity tactic closes the goal.
why it matters
The result feeds the riverNetworkCert definition that collects positivity and inequality facts for the Horton ratios. It supplies one of the log-positivity ingredients needed to derive the structural Hack exponent of exactly 1/2 inside the Recognition Science framework, consistent with the eight-tick octave and phi-ladder. The module flags that numerical comparison against observed exponents in (0.5, 0.65) from HydroSHEDS catalogs remains open for empirical adjudication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.