guildCount
The theorem fixes the cardinality of the canonical ecological guilds at five, aligning with the configuration dimension in Recognition Science models. Ecologists applying the framework to biodiversity indices would cite this to anchor Shannon and Simpson maxima at log(5) and 4/5. The proof is a direct decision on the Fintype instance of the five-constructor inductive type.
claimThe cardinality of the set of five canonical ecological guilds (producers, primary consumers, secondary consumers, decomposers, detritivores) equals five: $|G| = 5$.
background
The Biodiversity Indices from ConfigDim module treats configDim as five, matching the Recognition Science value that yields maximum Shannon diversity log(5) when the five guilds have equal biomass. EcologicalGuild is the inductive type enumerating exactly those guilds, equipped with Fintype, DecidableEq and related instances. Upstream, configDim is defined as 5 in the cosmology module (with comment on baryon rung) and as d + 2 in the integration gap module, where d denotes spatial degrees of freedom plus temporal and ledger terms.
proof idea
The proof is a one-line wrapper that applies the decide tactic to evaluate Fintype.card on the inductive EcologicalGuild type, whose five constructors directly determine the cardinality.
why it matters in Recognition Science
This result populates the guild_count field of BiodiversityCert, which certifies the optimum indices at configDim = 5. It implements the module's claim that healthy ecosystems reach H_max = log(configDim) with five guilds, linking to the forcing chain's D = 3 spatial dimensions and the eight-tick octave. The declaration closes the ecological application of the configuration dimension without introducing new hypotheses.
scope and limits
- Does not prove these five guilds are exhaustive in observed ecosystems.
- Does not derive guild structure from recognition events or the J-cost equation.
- Does not compute biodiversity for concrete habitats or biomass distributions.
- Does not generalize the count to other values of configDim.
Lean usage
example : Fintype.card EcologicalGuild = 5 := guildCountformal statement (Lean)
29theorem guildCount : Fintype.card EcologicalGuild = 5 := by decide
proof body
Term-mode proof.
30
31/-- Maximum Simpson diversity at configDim = 5. -/