reverse_swaps_endpoints
plain-language theorem explainer
The theorem shows that the reversal map on the eight Erikson stages interchanges the initial and terminal stages. Researchers modeling neurodegeneration as a reversed developmental sequence cite it to fix the boundary conditions of the involution. The proof reduces each equality to the explicit definition of the map via Fin.ext and simplification.
Claim. Let $r : Fin 8 → Fin 8$ be the map $r(k) = 7 - k$. Then $r(0) = 7$ and $r(7) = 0$.
background
The module treats Erikson's eight life stages as a cycle of length 8 arising from the 2³ tick structure. Reversal is the order-reversing map defined by $r(k) = 7 - k$ on Fin 8, which the sibling reverse_involution theorem shows is an involution. This endpoint result verifies the swap of stage 0 with stage 7, a prerequisite for the claim that mid-life stages invert before early ones in the reversed sequence.
proof idea
The term-mode proof refines the conjunction into two goals. Each goal is discharged by apply Fin.ext followed by simp [reverse], which reduces the equality to the arithmetic definition of the map.
why it matters
The result supplies the endpoints_swap component to DevelopmentReversalCert, which assembles the full certification of the reversal structure. It completes the boundary data for the C6 structural claim that links the eight stages to the eight-tick octave forced at T7. The parent cert packages this with the involution and midlife inversion to support the predicted clinical pattern of dementia progression.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.