TrophicLevel
plain-language theorem explainer
The inductive type enumerates five discrete trophic levels in a J-cost food-web model: producers through apex predators. Ecologists modeling cascade propagation in Recognition Science cite it to fix configDim at five. The definition is a direct inductive enumeration that derives decidable equality, representation, and finiteness automatically.
Claim. Let $T$ be the inductive type whose constructors are producers, herbivores, omnivores, carnivores, and apex predators, equipped with decidable equality and finite cardinality.
background
In the Recognition Science ecology module, J-cost quantifies deviation from recognition balance at each trophic level. A balanced web satisfies biomass ratio $r_k$ approximately 1, hence $J(r_k)=0$. Cascade onset occurs when the apex ratio exceeds $1/φ$, yielding $J(r_{apex})>J(φ)$, with each subsequent level shifted by $φ^{-1}$. The module documentation states that five levels equal configDim $D=5$. This definition supplies the discrete domain on which the cascade certificate operates.
proof idea
Direct inductive definition that introduces the five constructors and derives the typeclasses DecidableEq, Repr, BEq, Fintype via the deriving clause.
why it matters
This definition supplies the finite set of five trophic levels required by the downstream TrophicCascadeCert structure, which asserts Fintype.card equal to 5 together with a CanonicalCert. It realizes the five-level cascade model in the module documentation, where amplitude decays as $1/φ$ per transfer. The construction closes the ecology depth for the J-cost framework by providing the discrete domain on which the recognition balance equations operate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.