midlife_inverts_first
plain-language theorem explainer
The theorem shows that the reversal map on Fin 8 sends stage 6 to index 1 and stage 0 to index 7, so the former precedes the latter numerically. Modelers of neurodegeneration as an involution on the eight-stage Erikson cycle cite it to confirm that mid-life stages invert before early ones in the reversed sequence. The proof is a one-line simp wrapper on the reverse definition.
Claim. Let $r(k) = 7 - k$ for $k$ in Fin 8. Then $r(6) < r(0)$.
background
The module formalizes Erikson's eight life stages as a 2³ tick cycle under Recognition Science, with neurodegeneration running the ladder in reverse. The reversal map is the order-reversing involution reverse k = 7 - k on Fin 8. This local setting draws from the eight-tick octave landmark where the period equals 2³.
proof idea
The proof is a one-line wrapper that applies simp [reverse] to unfold the map and reduce the claim to the numerical inequality 1 < 7.
why it matters
This result supplies the midlife inversion field in developmentReversalCert, which aggregates stage count, the 2³ equality, the involution property, endpoint swap, and this inequality. It fills the C6 structural claim on the involution for the 2³ Erikson cycle and connects directly to the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.