biological_hasConfigDim5
plain-language theorem explainer
BiologicalState satisfies the configDim=5 predicate, confirming that this five-state biological model has exactly five elements. Cross-domain researchers in Recognition Science cite this instance when assembling product theorems across sensory, emotional, and biological domains. The proof is a one-line wrapper that unfolds the cardinality definition and applies the decide tactic on the derived Fintype instance.
Claim. The finite type BiologicalState satisfies $Fintype.card(BiologicalState) = 5$.
background
HasConfigDim5 is the predicate that a finite type T has cardinality exactly 5, defined as Fintype.card T = 5. BiologicalState is the inductive type with five constructors enumerating embryonic, developmental, mature, aging, and senescent phases, deriving DecidableEq, Repr, BEq, and Fintype from its structure.
proof idea
One-line wrapper that unfolds HasConfigDim5 to Fintype.card BiologicalState = 5 and applies the decide tactic, which succeeds because the inductive type derives Fintype with exactly five constructors.
why it matters
This instance populates configDimUniversalityCert and supplies the biological cardinality for three_domain_product (sensory × emotion × biological = 125) and five_domain_product (full product = 3125). It supports the module's structural claim that configDim D = 5 holds uniformly across domains, complementing the spatial D = 3 from the forcing chain T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.