InteractionType
InteractionType enumerates the five canonical predator-prey interaction modes required by the Recognition Science ecology model. Researchers calibrating Lotka-Volterra systems to the phi-ladder would cite it to fix configDim D = 5. The declaration is a plain inductive type with five constructors and automatic Fintype derivation.
claimThe inductive type of predator-prey interaction types consists of the five constructors top-down control, bottom-up control, apparent competition, intraguild predation, and indirect mutualism.
background
The module derives predator-prey oscillations from the phi-ladder: in a stable ecosystem at recognition equilibrium, prey and predator populations oscillate at frequencies in ratio phi:1, with equilibrium ratio phi when growth rates are calibrated to the canonical band. Five canonical interaction types are introduced to match configDim D = 5. The local setting is the ecology tier of Recognition Science, where Lotka-Volterra parameters are fixed by the phi-ladder equilibria.
proof idea
This is an inductive definition that introduces five named constructors and derives DecidableEq, Repr, BEq, and Fintype in one declaration.
why it matters in Recognition Science
The definition supplies the five interaction types required by the downstream theorem interactionTypeCount (Fintype.card InteractionType = 5) and by the structure PredatorPreyCert (which also records ratio_gt_one). It realizes the module claim that the number of canonical predator-prey interaction types equals configDim D = 5.
scope and limits
- Does not assign numerical growth rates to any constructor.
- Does not prove stability or oscillation periods.
- Does not derive the phi equilibrium ratio from the constructors.
formal statement (Lean)
25inductive InteractionType where
26 | topDown | bottomUp | apparentCompetition | intraguildPredation | indirectMutualism
27 deriving DecidableEq, Repr, BEq, Fintype
28