EcologicalGuild
EcologicalGuild enumerates the five canonical guilds that realize maximum biodiversity when configDim equals 5 in the Recognition Science ecology model. Biodiversity calculations cite this finite set to bound Shannon entropy at log(5) and Simpson diversity at 4/5. The declaration is an inductive type that automatically derives a Fintype instance, enabling direct cardinality proofs.
claimLet $G$ be the finite set of ecological guilds $G = $ {producer, primary consumer, secondary consumer, decomposer, detritivore}.
background
The module Biodiversity Indices from ConfigDim treats Shannon diversity as maximized at log(configDim) when biomass is equipartitioned across five guilds, yielding H_max = log(5) in RS units. Simpson diversity then reaches its peak value of 4/5. The inductive definition supplies the discrete carrier set whose cardinality is fixed at 5, matching the configDim parameter that distinguishes healthy from degraded ecosystems.
proof idea
The declaration is an inductive type with five explicit constructors, deriving DecidableEq, Repr, BEq, and Fintype instances by standard Lean automation. No separate proof body or lemmas are invoked.
why it matters in Recognition Science
This definition supplies the concrete set required by the guild_count field of BiodiversityCert and by the theorem guildCount that asserts Fintype.card EcologicalGuild = 5. It anchors the RS ecology claim that healthy ecosystems achieve H_max = log(5) and Simpson diversity 0.8, corresponding to the five-guild structure at configDim = 5. The module closes with zero sorry statements.
scope and limits
- Does not model continuous biomass distributions or interaction rates.
- Does not admit additional guilds such as tertiary consumers.
- Does not compute numerical diversity values, only the underlying finite set.
formal statement (Lean)
25inductive EcologicalGuild where
26 | producer | primaryConsumer | secondaryConsumer | decomposer | detritivore
27 deriving DecidableEq, Repr, BEq, Fintype
28