theorem
proved
interactionTypeCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Ecology.PredatorPreyFromPhiLadder on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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