biological_hasConfigDim5
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of these five states among all possible biological models.
- Does not address infinite or non-finite biological types.
- Does not derive connections to physical constants or the phi-ladder.
- Does not establish bijections with other D=5 domains.
Lean usage
have hb : Fintype.card BiologicalState = 5 := biological_hasConfigDim5formal statement (Lean)
50theorem biological_hasConfigDim5 : HasConfigDim5 BiologicalState := by
proof body
One-line wrapper that applies unfold.
51 unfold HasConfigDim5; decide