PredatorPreyCert
plain-language theorem explainer
PredatorPreyCert packages the two invariants for a phi-ladder predator-prey model: exactly five canonical interaction types and an equilibrium prey-to-predator ratio strictly greater than one. Recognition Science ecologists cite it to certify compliance with configDim = 5 and the phi-scaled ratio in Lotka-Volterra systems. The declaration is a bare structure definition with no computational content or proof obligations.
Claim. A structure consisting of the assertions that the cardinality of the set of interaction types equals 5 and that the equilibrium prey-to-predator ratio exceeds 1, where the ratio is defined to equal the golden ratio $phi$.
background
The module calibrates the Lotka-Volterra predator-prey model so that equilibrium populations oscillate with prey/predator ratio $phi$. The five interaction types are top-down control, bottom-up control, apparent competition, intraguild predation, and indirect mutualism, matching configuration dimension D = 5. Upstream, equilibriumRatio is defined as the constant $phi$, while InteractionType is the inductive enumeration of those five cases.
proof idea
This is a structure definition that declares two fields with no tactics, lemmas, or reduction steps applied. The first field requires Fintype.card of InteractionType to equal 5; the second requires 1 < equilibriumRatio.
why it matters
The structure supplies the certificate type instantiated by the downstream definition predatorPreyCert, which builds an explicit witness from interactionTypeCount and equilibriumRatio_gt_one. It packages the ecology predictions that link to the Recognition Science T6 phi fixed point and the assignment of five interaction types to configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.