DevelopmentReversalCert
plain-language theorem explainer
DevelopmentReversalCert packages five properties asserting that the eight Erikson stages form a 2^3 cycle equipped with an involutive reversal on Fin 8. Developmental psychologists or neurodegeneration modelers would cite it to encode the predicted reversal pattern in dementia progression. The structure is populated by direct assembly of cardinality, involution, and endpoint lemmas with no additional proof steps.
Claim. A certificate whose fields assert: the set of Erikson stages has cardinality 8; this cardinality equals $2^3$; the reversal map $r$ on Fin 8 satisfies $r(r(k))=k$ for all $k$; $r(0)=7$; and the value of $r(6)$ is strictly less than the value of $r(0)$.
background
EriksonStage is the inductive type with eight constructors: trust versus mistrust, autonomy versus shame, initiative versus guilt, industry versus inferiority, identity versus confusion, intimacy versus isolation, generativity versus stagnation, and integrity versus despair. The reverse function is defined by reverse k := 7 - k.val on Fin 8 and satisfies the involution property reverse(reverse k) = k. The module formalizes the claim that these stages form a 2^3 tick cycle with neurodegeneration traversing them in reverse order.
proof idea
Structure definition whose fields are filled by direct references to sibling results: eriksonCount supplies the cardinality 8, erikson_eq_2cube supplies equality to 2^3, reverse_involution supplies the involution, reverse_swaps_endpoints supplies the endpoint swap, and midlife_inverts_first supplies the midlife inversion order.
why it matters
The certificate supplies the structural properties required by the downstream developmentReversalCert constructor. It encodes the eight-tick octave (T7) from the forcing chain as an involution on the Erikson stages, linking the Recognition Science 2^3 period to the reversal pattern in neurodegeneration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.