log_phi_pos
plain-language theorem explainer
The inequality 0 < log φ holds because φ > 1 and the natural logarithm is strictly increasing on (1, ∞). Ecologists deriving species-area relations from J-cost conservation on recognition graphs cite this to guarantee that the structural exponent z = log φ / (1 + log φ) is positive. The proof is a one-line wrapper applying the Mathlib primitive Real.log_pos directly to the upstream bound one_lt_phi.
Claim. $0 < log φ$, where $φ$ is the golden ratio fixed point of the Recognition Composition Law.
background
This theorem sits inside the Biodiversity Scaling from J-Cost module, which treats a regional ecosystem as a recognition graph whose σ-conservation forces φ-self-similar bond density. The module derives the Arrhenius form S(A) ∝ A^z with z = log φ / (1 + log φ) and checks that z lies in the empirical band (0.15, 0.45). The upstream lemma one_lt_phi states 1 < φ via the quadratic definition φ = (1 + √5)/2, quoted as 'φ > 1: The golden ratio is strictly greater than 1.' Parallel copies of the same positivity fact appear in BlackHoleHorizonStates and PhiLadderLattice to support the same inequality in gravity and number-theory contexts.
proof idea
The proof is a one-line wrapper that applies Real.log_pos to the hypothesis one_lt_phi. No additional tactics are required; the positivity of the logarithm on (1, ∞) is supplied directly by Mathlib.
why it matters
The result supplies the log_phi_pos field inside the BiodiversityScalingCert structure, which is then used by species_area_exponent_pos to prove z > 0 and by species_area_exponent_in_band to place z inside (0.15, 0.45). It therefore closes the basic positivity step required for the module's claim that σ-conservation on inventory graphs reproduces the observed Arrhenius dispersion. The fact traces back to the T6 forcing of φ as self-similar fixed point and is reused across gravity and lattice modules.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.