equilibriumRatio_gt_one
plain-language theorem explainer
The theorem establishes that the equilibrium prey-to-predator population ratio exceeds one under the phi-ladder calibration of Lotka-Volterra dynamics. Ecologists working with stable ecosystems cite it to confirm the golden-ratio scaling of populations at recognition equilibrium. The proof is a one-line wrapper that unfolds the ratio definition and applies the known inequality for phi.
Claim. The equilibrium prey-to-predator population ratio satisfies $1 < phi$, where $phi$ denotes the golden ratio.
background
The module derives predator-prey dynamics from the phi-ladder in Recognition Science. At equilibrium the prey-to-predator ratio equals phi, matching the Lotka-Volterra fixed point N* = c/d, P* = a/b once growth rates are set to the canonical band. The five canonical interaction types equal configDim D = 5. Upstream, equilibriumRatio is the definition noncomputable def equilibriumRatio : ℝ := phi. The lemma one_lt_phi states 1 < phi and is proved from the quadratic definition of phi as (1 + sqrt(5))/2.
proof idea
The proof is a one-line wrapper. It unfolds the definition of equilibriumRatio to obtain phi, then applies the lemma one_lt_phi to discharge the inequality.
why it matters
This supplies the ratio_gt_one field inside the predatorPreyCert definition, which certifies both the count of five interaction types and the ratio property for the ecology tier. It rests on the foundational property phi > 1 that appears throughout the phi-ladder construction and the eight-tick octave. No open scaffolding remains at this leaf.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.