BiologicalState
plain-language theorem explainer
BiologicalState enumerates five stages of biological development as an inductive type. Cross-domain universality arguments cite it to confirm the biological domain meets the D=5 cardinality requirement. The declaration is a direct inductive definition that derives Fintype, DecidableEq, and related instances for immediate use in product cardinality proofs.
Claim. The set of biological states is the five-element set with distinct elements embryonic, developmental, mature, aging, and senescent, equipped with decidable equality and finite-type structure.
background
The module establishes that configDim D=5 appears across domains by defining a predicate HasConfigDim5(T) that holds exactly when the cardinality of T is 5. Five domain-specific types are introduced, each proved to have cardinality 5 by direct decision, and their products are shown to equal 125 or 3125. BiologicalState supplies the biological-domain instance in this collection.
proof idea
The declaration is an inductive definition with five constructors. The deriving clause automatically installs DecidableEq, Repr, BEq, and Fintype instances, enabling the cardinality equalities used in the three-domain and five-domain product theorems.
why it matters
BiologicalState is referenced by ConfigDimUniversalityCert to certify the biological D=5 instance alongside the sensory, emotion, economic, and linguistic domains. It directly supports the three_domain_product theorem (cardinality 125) and five_domain_product theorem (cardinality 3125). This contributes to the module's structural claim that D=5 configurations recur with high frequency across the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.