EcologicalGuild
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.