one_plus_log_phi_pos
plain-language theorem explainer
one_plus_log_phi_pos establishes that 1 plus the natural log of the golden ratio is positive. Ecologists modeling species-area scaling under Recognition Science cite it to guarantee the Arrhenius exponent z remains positive. The proof is a one-line wrapper that applies the prior log_phi_pos result and closes via linear arithmetic.
Claim. $1 + {log} φ > 0$, where φ is the golden ratio greater than 1.
background
In the Biodiversity Scaling from J-Cost module the species-area exponent is defined as z = log φ / (1 + log φ). Upstream theorems in PhiLadderLattice, BlackHoleHorizonStates, and DiscreteGauge each prove log φ > 0 because φ > 1. This local result ensures the denominator of z stays positive so the exponent is well-defined and positive on the inventory graph.
proof idea
The proof is a one-line wrapper that applies log_phi_pos from the same module and uses linarith to obtain the strict inequality.
why it matters
It supplies the one_plus_log_phi_pos field to the BiodiversityScalingCert structure and is invoked directly in species_area_exponent_pos, species_area_exponent_lt_half, and species_area_exponent_in_band. These results place z inside the empirical Arrhenius band (0.15, 0.45) and tie the scaling to φ-self-similar bond density under σ-conservation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.