developmentReversalCert
plain-language theorem explainer
DevelopmentReversalCert is instantiated by direct substitution of the cardinality, involution, and ordering lemmas for the eight Erikson stages. A researcher modeling neurodegeneration as stage reversal would cite this to anchor the 2^3 cycle and the map k to 7-k. The definition is a record construction that assembles the six supporting results from the same module.
Claim. Let $E$ be the type of Erikson stages. The certificate asserts $|E|=8$, $|E|=2^3$, the reversal $r(k)=7-k$ 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
The module states C6: Erikson's eight stages form a 2^3 tick cycle with neurodegeneration running the ladder in reverse via the order-reversing involution reverse k = 7 - k on Fin 8. Involution means reverse composed with itself is the identity. The predicted pattern is that dementia passes through stages in reverse order, with mid-life stages inverting before early ones.
proof idea
The definition constructs the DevelopmentReversalCert record by direct field assignment: stage_count from eriksonCount, two_cube from erikson_eq_2cube, involution from reverse_involution, endpoints_swap from the first conjunct of reverse_swaps_endpoints, and midlife_first from midlife_inverts_first. All six upstream results are theorems proved by decide, Fin.ext, simp, or omega.
why it matters
This supplies the concrete certificate for the C6 structural claim, linking the eight-tick octave (T7) to the Erikson model via the involution and reversal properties. No parent theorems appear in the used_by list. It closes the formalization of wave 62 with zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.