biodiversityCert
plain-language theorem explainer
The definition assembles a biodiversity certificate by populating the guild count field with the result of a decision procedure and the Simpson maximum with a numerical equality. Researchers extending Recognition Science to ecological modeling would cite this when instantiating the optimum diversity structure for five guilds. It proceeds by direct record construction from two supporting theorems.
Claim. Define the biodiversity certificate as the structure with guild count equal to five and maximum Simpson diversity equal to four fifths.
background
The module sets biodiversity indices against configDim equal to five, matching the five canonical guilds of producers, primary consumers, secondary consumers, decomposers, and detritivores. Shannon diversity reaches its maximum of log five under equal biomass, while Simpson diversity reaches four fifths. The upstream theorem guildCount proves the guild type has cardinality five by decision procedure. The companion theorem maxSimpsonDiversity_eq reduces the maximum Simpson value to four fifths by unfolding and normalization.
proof idea
The definition constructs the certificate record by assigning the guild count field directly from the guildCount theorem and the Simpson maximum from the maxSimpsonDiversity_eq theorem. No additional tactics are applied beyond the record syntax.
why it matters
This definition supplies the concrete instance of the BiodiversityCert structure that certifies the RS-predicted biodiversity optimum at configDim five. It completes the local setup in the ecology module, where degraded ecosystems are characterized by lower diversity indices. No parent theorems depend on it yet, but it aligns with the framework's extension of configDim concepts beyond the spatial forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.