theorem
proved
guildCount
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim on GitHub at line 29.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
26 | producer | primaryConsumer | secondaryConsumer | decomposer | detritivore
27 deriving DecidableEq, Repr, BEq, Fintype
28
29theorem guildCount : Fintype.card EcologicalGuild = 5 := by decide
30
31/-- Maximum Simpson diversity at configDim = 5. -/
32noncomputable def maxSimpsonDiversity : ℝ := 1 - 1 / 5
33
34theorem maxSimpsonDiversity_eq : maxSimpsonDiversity = 4 / 5 := by
35 unfold maxSimpsonDiversity; norm_num
36
37structure BiodiversityCert where
38 guild_count : Fintype.card EcologicalGuild = 5
39 simpson_max : maxSimpsonDiversity = 4 / 5
40
41noncomputable def biodiversityCert : BiodiversityCert where
42 guild_count := guildCount
43 simpson_max := maxSimpsonDiversity_eq
44
45end IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim