eriksonCount
plain-language theorem explainer
EriksonStage has cardinality eight, aligning the eight psychosocial stages with the 2^3 tick cycle. Researchers modeling neurodegeneration as stage reversal in developmental psychology would cite this cardinality to anchor the involution formalization. The proof is a one-line decide tactic that evaluates the Fintype instance derived from the eight inductive constructors.
Claim. The finite set of Erikson stages has cardinality eight: $|E| = 8$, where $E$ enumerates the eight crises from trust vs. mistrust through integrity vs. despair.
background
The module formalizes development reversal on Erikson's stages as an order-reversing involution on a 2^3 cycle, with reverse(k) = 7 - k. EriksonStage is the inductive type whose eight constructors are trustVsMistrust, autonomyVsShame, initiativeVsGuilt, industryVsInferiority, identityVsConfusion, intimacyVsIsolation, generativityVsStagnation, and integrityVsDespair; it derives Fintype, DecidableEq, and Repr. The upstream inductive definition supplies the finite type whose cardinality is asserted here.
proof idea
One-line wrapper that applies the decide tactic to compute Fintype.card directly from the eight-constructor inductive definition and its derived Fintype instance.
why it matters
Supplies the stage_count field to developmentReversalCert, which bundles the full reversal properties including the involution, endpoint swap, and midlife inversion. This realizes the T7 eight-tick octave landmark by equating the stage count to 2^3 and closes the structural claim of wave 62.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.