trophicLevelCount
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive J-cost balance equations at each level.
- Does not model continuous biomass dynamics or propagation.
- Does not connect to the spatial dimension D=3 from the forcing chain.
- Does not supply numerical values for phi or other constants.
formal statement (Lean)
31theorem trophicLevelCount : Fintype.card TrophicLevel = 5 := by decide
proof body
32