erikson_eq_2cube
plain-language theorem explainer
EriksonStage has cardinality eight, confirming the 2^3 structure for the developmental reversal model. Researchers modeling neurodegeneration as an involution on the developmental ladder cite this cardinality to anchor the discrete cycle. The proof is a one-line decision procedure that enumerates the eight constructors after the derived Fintype instance.
Claim. The finite type of Erikson stages satisfies $|EriksonStage| = 2^3$.
background
The module frames Erikson's eight life stages as a 2³ tick cycle, with reversal defined as the order-reversing involution reverse k = 7 - k on Fin 8. EriksonStage is the inductive type whose constructors are the eight stages trustVsMistrust through integrityVsDespair and which derives Fintype, DecidableEq, and related instances. The upstream inductive definition supplies the finite enumeration required for the cardinality claim.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the goal Fintype.card EriksonStage = 2 ^ 3. The tactic succeeds by computing the cardinality directly from the Fintype instance derived on the eight-constructor inductive type.
why it matters
This result supplies the two_cube field to DevelopmentReversalCert, which assembles the full certificate of involution properties including stage count, involution, endpoint swap, and midlife inversion. It aligns with the eight-tick octave (T7) in the forcing chain and closes the discrete counting step for the cross-domain reversal claim in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.