predatorPreyCert
plain-language theorem explainer
This definition assembles the predator-prey certificate by fixing the count of interaction types at five and confirming the equilibrium ratio exceeds one. Theoretical ecologists working with Lotka-Volterra systems under Recognition Science constraints would cite it to anchor phi-based population ratios. The construction is a direct record instantiation that pulls the two properties from prior theorems on cardinality and the phi inequality.
Claim. Define the certificate $C$ by the two properties that the set of canonical predator-prey interaction types has cardinality five and that the equilibrium prey-to-predator population ratio $r$ satisfies $1 < r$.
background
In the Recognition Science ecology module the Lotka-Volterra predator-prey oscillation period is required to follow the phi-ladder, so that at equilibrium the prey/predator ratio equals phi. The five canonical interaction types (top-down control, bottom-up control, apparent competition, intraguild predation, indirect mutualism) are identified with configuration dimension D = 5. The upstream theorem equilibriumRatio_gt_one reduces the inequality 1 < equilibriumRatio directly to one_lt_phi, while interactionTypeCount establishes the cardinality by decision.
proof idea
The definition is a one-line record construction. It supplies the five_types field from the theorem interactionTypeCount and the ratio_gt_one field from the theorem equilibriumRatio_gt_one.
why it matters
The certificate supplies the two base facts needed for the predator-prey module and thereby closes the elementary properties in the ecology tier. It supports the RS prediction that the equilibrium ratio equals phi and links to the phi-ladder fixed point. No downstream theorems are recorded, leaving open its integration with higher ecological models.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.