interactionTypeCount
plain-language theorem explainer
Exactly five canonical predator-prey interaction types exist in the Recognition Science ecology model. Ecologists calibrating Lotka-Volterra systems to the phi-ladder would cite the result to confirm configDim D equals 5. The proof is a direct decision on the Fintype cardinality of the inductive type.
Claim. |{top-down control, bottom-up control, apparent competition, intraguild predation, indirect mutualism}| = 5
background
InteractionType is the inductive type with constructors topDown, bottomUp, apparentCompetition, intraguildPredation, and indirectMutualism, deriving Fintype, DecidableEq, and related instances. The module derives Lotka-Volterra predator-prey oscillations from the phi-ladder, with equilibrium prey/predator ratio equal to phi and the interaction count fixed at configDim D = 5. It depends on the upstream equilibrium theorem asserting Jcost 1 = 0, which encodes zero recognition cost at equilibrium.
proof idea
A one-line wrapper that applies the decide tactic to compute Fintype.card directly from the inductive definition of InteractionType.
why it matters
The theorem supplies the five_types field inside predatorPreyCert, completing the certification of the predator-prey model. It realizes the configDim D = 5 claim in the ecology tier and connects to the phi-ladder equilibrium structure. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.