log_phi_gt_threeTenths
plain-language theorem explainer
The theorem establishes that log φ exceeds 0.30. Researchers deriving the species-area exponent from J-cost conservation in Recognition Science cite this bound to confirm the exponent lies inside the empirical Arrhenius range. The proof halves the lower bound supplied by the companion result 0.69 < 2 log φ and closes via linear arithmetic.
Claim. $0.30 < log φ$ where φ denotes the golden ratio.
background
In the Recognition Science treatment of biodiversity a regional ecosystem is modeled as a recognition graph whose σ-conservation forces φ-self-similar bond density. The species count S over area A then obeys the Arrhenius form S ∝ A^z with structural exponent z = log φ / (1 + log φ). The upstream theorem two_log_phi_gt states 0.69 < 2 log φ because phi^2 > 2.5, which supplies the concrete numerical anchor used here. This local setting forms part of Track Q3 of Plan v7, where the structural exponent is shown to lie in the empirical Arrhenius band (0.15, 0.45) without free parameters.
proof idea
The proof is a one-line wrapper. It invokes the upstream theorem two_log_phi_gt establishing 0.69 < 2 log φ, then applies linarith to deduce the halved lower bound 0.30 < log φ.
why it matters
The bound is assembled into the BiodiversityScalingCert structure that certifies the species-area exponent lies inside the empirical Arrhenius band (0.15, 0.45). It thereby completes one numerical check required for the partial theorem on biodiversity scaling from J-cost. The result supports the claim that φ-self-similarity reproduces observed ecological scaling laws.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.