log_phi_lt_one
plain-language theorem explainer
log φ < 1 supplies the upper bound on the natural log of the golden ratio needed for sub-square-root species growth. Ecologists working on Arrhenius exponents from J-cost on recognition graphs and gravity researchers distinguishing entropy coefficients cite this result. The tactic proof chains log monotonicity against phi_lt_two with the library fact log 2 < 1 and closes via linarith.
Claim. Let φ be the golden ratio. Then log φ < 1.
background
The module derives the structural species-area exponent z = log φ / (1 + log φ) for species count S(A) on a recognition graph under σ-conservation, placing z inside the empirical Arrhenius band (0.15, 0.45). This lemma supplies the concrete inequality log φ < 1 that forces z < 1/2, i.e., each area doubling adds fewer than √A new species. Upstream, phi_lt_two from PhiForcing states φ < 2 and Real.log_two_lt_d9 states log 2 < 1; the module doc notes that the complementary identity 1 - z = 1/(1 + log φ) records the missed-species fraction per area doubling.
proof idea
One-line wrapper that applies Real.log_lt_log to phi_pos and phi_lt_two to obtain log φ < log 2, invokes Real.log_two_lt_d9 inside a linarith block to get log 2 < 1, then finishes with a final linarith.
why it matters
The bound is required by BiodiversityScalingCert and species_area_exponent_lt_half to certify the species-area exponent band, and by c_RS_neq_LQG and c_RS_neq_string to show the RS leading-log coefficient differs from both -1/2 and -3/2. It anchors the ecology track of the forcing chain and supplies the numerical separation from LQG and string-theory entropy forms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.