BiodiversityCert
plain-language theorem explainer
BiodiversityCert packages two invariants for an ecosystem at the Recognition Science optimum: exactly five ecological guilds and maximum Simpson diversity of 4/5. Ecologists working in the RS framework would cite it to certify that a given configuration matches the predicted healthy state. The definition is a direct structure declaration with no proof obligations.
Claim. A structure certifying that the set of five canonical ecological guilds has cardinality 5 and that the maximum Simpson diversity equals $4/5$.
background
The module derives biodiversity indices from the configuration dimension in Recognition Science. Shannon diversity reaches its maximum of log(5) when biomass is equally distributed across the five guilds. Simpson diversity is defined as 1 minus the sum of squared proportions and attains its peak value of 4/5 at this optimum.
proof idea
The declaration is a structure definition. Its first field asserts that the finite type cardinality of the five-guild inductive type equals 5. The second field equates the upstream constant maxSimpsonDiversity (defined as 1 - 1/5) to 4/5.
why it matters
This definition supplies the certificate type consumed by the biodiversityCert construction in the same module. It encodes the RS prediction that healthy ecosystems maximize diversity at configDim = 5, with Simpson index 4/5. The module states that degraded ecosystems have lower diversity, positioning this as a benchmark for ecological health.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.