pith. machine review for the scientific record. sign in
module module moderate

IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim

show as:
view Lean formalization →

The module defines the five canonical ecological guilds together with guildCount and maxSimpsonDiversity measures derived from configuration dimension. It supplies the basic objects needed to construct a biodiversity index inside the Recognition Science framework. Ecologists working with RS constants would cite these definitions when mapping configuration structure to diversity metrics. The module contains only definitions and no theorems.

claimLet $G$ be the set of five canonical ecological guilds. Define guildCount as the cardinality of $G$ and maxSimpsonDiversity as the supremum of the Simpson index over configurations of given dimension.

background

The module sits in the ecology domain of Recognition Science and imports the RS time quantum τ₀ = 1 tick from IndisputableMonolith.Constants. It introduces EcologicalGuild as the five canonical types, guildCount as their number, and maxSimpsonDiversity as the maximum attainable Simpson diversity for a given configuration dimension. The local setting applies RS configuration structure to ecological guild models without invoking the forcing chain or phi-ladder directly.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the definitional base for biodiversity indices computed from configuration dimension. It feeds future theorems that certify biodiversity measures inside ecological applications of Recognition Science. No parent theorems appear in the current used-by graph.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)