IndisputableMonolith.Ecology.PredatorPreyFromPhiLadder

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Predator-Prey Dynamics from Phi-Ladder — Tier F Ecology
   6
   7The Lotka-Volterra predator-prey oscillation period follows the phi-ladder:
   8in a stable ecosystem at recognition equilibrium, prey and predator
   9populations oscillate at frequencies in ratio phi:1.
  10
  11RS prediction: prey/predator population ratio at equilibrium = phi
  12(Lotka-Volterra equilibrium N* = c/d, P* = a/b gives ratio phi when
  13the growth rates are calibrated to the canonical band).
  14
  15The 5 canonical predator-prey interaction types (top-down control,
  16bottom-up control, apparent competition, intraguild predation, indirect
  17mutualism) = configDim D = 5.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith.Ecology.PredatorPreyFromPhiLadder
  23open Constants
  24
  25inductive InteractionType where
  26  | topDown | bottomUp | apparentCompetition | intraguildPredation | indirectMutualism
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem interactionTypeCount : Fintype.card InteractionType = 5 := by decide
  30
  31/-- At equilibrium, prey/predator ratio = phi. -/
  32noncomputable def equilibriumRatio : ℝ := phi
  33
  34theorem equilibriumRatio_gt_one : 1 < equilibriumRatio := by
  35  unfold equilibriumRatio; exact one_lt_phi
  36
  37structure PredatorPreyCert where
  38  five_types : Fintype.card InteractionType = 5
  39  ratio_gt_one : 1 < equilibriumRatio
  40
  41noncomputable def predatorPreyCert : PredatorPreyCert where
  42  five_types := interactionTypeCount
  43  ratio_gt_one := equilibriumRatio_gt_one
  44
  45end IndisputableMonolith.Ecology.PredatorPreyFromPhiLadder
  46