pith. sign in
module module moderate

IndisputableMonolith.Ecology.BiodiversityIndexFromConfigDim

show as:
view Lean formalization →

The module defines the five canonical ecological guilds and associated biodiversity measures such as guild counts and Simpson diversity maxima inside the Recognition Science framework. Ecologists modeling species diversity under RS constraints would cite these definitions. It is a definitions-only module with no theorems or proofs.

claimThe module introduces the set of five canonical ecological guilds, the function counting guilds, the maximum Simpson diversity, and the biodiversity certification predicate.

background

This module belongs to the Ecology domain of Recognition Science and imports the Constants module. The upstream Constants module defines the fundamental RS time quantum as $\tau_0 = 1$ tick. The module doc-comment identifies its content as the five canonical ecological guilds; sibling definitions cover EcologicalGuild, guildCount, maxSimpsonDiversity, maxSimpsonDiversity_eq, BiodiversityCert, and biodiversityCert.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies foundational definitions that connect Recognition Science constants to ecological biodiversity measures. It supports applications of the RS framework to biology, though the dependency graph lists no immediate downstream theorems. It aligns with the overall derivation of sciences from the single functional equation via the imported constants.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (6)