two_log_phi_gt
plain-language theorem explainer
Recognition Science establishes the inequality 0.69 < 2 log phi for the golden ratio phi. Biodiversity modelers cite this bound when placing the structural Arrhenius exponent z = log phi / (1 + log phi) inside the empirical interval (0.15, 0.45). The tactic proof obtains phi squared greater than 2 from phi_squared_bounds, applies monotonicity of the logarithm, rewrites via log_pow, and closes with the known lower bound on log 2.
Claim. $0.69 < 2 log phi$, where $phi$ denotes the golden ratio.
background
The module BiodiversityScalingFromJCost develops the Recognition Science account of biodiversity scaling. A regional ecosystem is treated as a recognition graph on its species inventory; sigma-conservation forces phi-self-similar bond density, so that species count S grows with sampled area A according to S(A) proportional to A^z with structural exponent z = log phi / (1 + log phi). This theorem supplies the numerical lower bound on log phi required to verify that z lies inside the empirical interval (0.15, 0.45).
proof idea
The tactic proof first obtains 2 < phi^2 from phi_squared_bounds via linarith. It then applies Real.log_lt_log to deduce log 2 < log (phi^2), rewrites the right-hand side with Real.log_pow, and uses Real.log_two_gt_d9 to get 0.69 < log 2. A final linarith combines the inequalities.
why it matters
The bound is invoked by the downstream theorem log_phi_gt_threeTenths to produce the cleaner statement 0.30 < log phi. This numerical control confirms that the structural Arrhenius exponent z belongs to the band that matches observed species-area relations, thereby supporting the J-cost derivation of biodiversity scaling in the module. It closes the verification step for the claim that any catalog with z outside (0.15, 0.45) would falsify the sigma-conservation reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.