maxSimpsonDiversity
plain-language theorem explainer
The definition assigns the maximum Simpson diversity index the value 1 - 1/5 when five ecological guilds are present at configDim = 5. Biodiversity researchers in the Recognition Science program cite this constant when constructing certificates for ecosystem health. It is introduced by a direct constant definition with no further computation.
Claim. The maximum Simpson diversity index for five equally abundant ecological guilds is $1 - 1/5$.
background
The module defines biodiversity indices using configDim, the number of canonical ecological guilds fixed at 5. Shannon diversity is maximized at log(configDim) when all guilds have equal biomass, while Simpson diversity $D_s = 1 - sum p_i^2$ is maximized at 1 - 1/configDim. The supplied module doc states that each trophic level reduction from optimum is a Z-rung step down, and Lean status is zero sorry or axiom.
proof idea
The declaration is a noncomputable definition that directly sets maxSimpsonDiversity to the constant 1 - 1/5. The companion theorem maxSimpsonDiversity_eq unfolds this definition and applies norm_num to establish equality with 4/5.
why it matters
This supplies the simpson_max field in the BiodiversityCert structure, which certifies guild_count = 5 and the maximum Simpson value. It fills the RS prediction for healthy ecosystem optimum at configDim = 5, consistent with the framework's use of phi-ladder and D = 3 spatial dimensions in broader contexts. No open questions are indicated in the downstream results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.