InteractionType
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.