trophicLevelCount
plain-language theorem explainer
The theorem fixes the cardinality of the inductive type of trophic levels at exactly five in the Recognition Science ecology model. Cascade modelers cite it to anchor the discrete level count when computing amplitude decay of order 1/phi per transfer. The proof is a one-line decision procedure that enumerates the five constructors of the inductive definition.
Claim. Let $T$ be the finite type whose elements are the trophic levels producers, herbivores, omnivores, carnivores, and apex predators. Then the cardinality of $T$ equals 5.
background
The module models trophic cascades via J-cost balance, where a level at equilibrium ratio $r_k$ satisfies $J(r_k)=0$ and a cascade trigger at the apex shifts each subsequent level by a factor of order phi^{-1}. The local setting equates the five levels to configuration dimension D=5. The upstream inductive definition TrophicLevel supplies the five constructors producers, herbivores, omnivores, carnivores, apexPredators together with its Fintype instance.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute the cardinality directly from the five constructors of the inductive type.
why it matters
This supplies the level count to the downstream certificate trophicCascadeCert. It fills the ecology tier of the Recognition Science framework by fixing the number of levels at five, matching the module's identification of configDim D=5 and supporting the 1/phi decay per level transfer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.