IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Biodiversity Indices from ConfigDim — B-tier Ecology Depth
   6
   7Shannon diversity H = -sum p_i log(p_i) is maximised at H = log(configDim)
   8= log(5) ≈ 1.609 nats, when all 5 canonical ecological guilds
   9(producers, primary consumers, secondary consumers, decomposers, detritivores)
  10= configDim D = 5 have equal biomass.
  11
  12RS prediction: the healthy ecosystem optimum is H_max = log(configDim)
  13= log(5) in RS units. Degraded ecosystems have H < H_max.
  14
  15The Simpson diversity D_s = 1 - sum p_i^2 is maximised at 1 - 1/configDim = 4/5 = 0.8.
  16Each trophic level reduction from optimum is a Z-rung step down.
  17
  18Lean status: 0 sorry, 0 axiom.
  19-/
  20
  21namespace IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim
  22open Constants
  23
  24/-- The five canonical ecological guilds. -/
  25inductive EcologicalGuild where
  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
  46