homoStageCount
plain-language theorem explainer
The declaration asserts that the inductive type enumerating human evolutionary stages has cardinality exactly five. Anthropologists aligning social structures with Recognition Science would cite this to confirm the match between evolutionary complexity and configDim D = 5. The proof is a one-line decision procedure that enumerates the five constructors of the stage type.
Claim. The finite type of human evolutionary stages has cardinality $5$, where the stages are Australopithecus, Homo habilis, Homo erectus, Homo heidelbergensis, and Homo sapiens.
background
The module AnthropologyFromRS derives social science from Recognition Science by mapping five canonical subfields and five evolutionary stages to configDim D = 5. Human evolution is treated as a phi-ladder of Z-complexity rungs, with Homo sapiens at the highest rung below artificial systems. HomoStage is the inductive type whose five constructors are exactly the listed stages, deriving Fintype, DecidableEq, and related instances to support cardinality statements.
proof idea
The proof is a one-line wrapper that applies the decide tactic. The tactic exhaustively checks the equality by enumerating the five constructors of HomoStage and confirming the resulting finite type has size 5.
why it matters
This theorem supplies the five_stages field in the anthropologyCert definition, which certifies that anthropological structures align with the five-dimensional configuration space. It directly realizes the module claim that five evolutionary stages equal configDim D = 5. The result closes the enumeration step for downstream certification without touching the forcing chain or physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.