interactionTypeCount
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 in Recognition Science
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.
scope and limits
- Does not derive the five interaction types from the forcing chain or J-uniqueness.
- Does not prove the equilibrium prey/predator ratio equals phi.
- Does not address time-dependent oscillation periods.
- Does not extend to interaction types outside the five enumerated constructors.
Lean usage
noncomputable def predatorPreyCert : PredatorPreyCert where five_types := interactionTypeCount ratio_gt_one := equilibriumRatio_gt_oneformal statement (Lean)
29theorem interactionTypeCount : Fintype.card InteractionType = 5 := by decide
proof body
Term-mode proof.
30
31/-- At equilibrium, prey/predator ratio = phi. -/