reverse
plain-language theorem explainer
The reversal map on the eight-element cycle is the arithmetic function sending each index k to 7 minus k. Researchers formalizing the predicted reversal of Erikson stages during neurodegeneration would cite this map to encode the order-reversing involution on the 2^3 cycle. The definition is a direct construction on Fin 8 whose bound is discharged by the omega tactic.
Claim. The map $r : [0,7] → [0,7]$ is defined by $r(k) = 7 - k$.
background
The module treats Erikson's eight life stages as the cycle Fin 8, identified with the 2^3 tick structure of the eight-tick octave. Reversal is the order-reversing involution on this cycle, so that neurodegeneration is predicted to traverse the stages backward. Upstream identity maps from CostAlgebra and ArithmeticOf supply the algebraic identity operation that appears in the related involution theorems; the module doc-comment states the structural claim that dementia progression passes through stages in reverse order.
proof idea
The definition is a direct one-line construction: the function on Fin 8 is written explicitly as subtraction from 7, with the omega tactic discharging the single proof obligation that the result lies in the correct range.
why it matters
This definition supplies the reversal operation required by DevelopmentReversalCert, reverse_involution, reverse_swaps_endpoints and midlife_inverts_first. It realizes the C6 structural claim inside the cross-domain reversal module and connects the 2^3 stage count to the eight-tick octave (T7) of the forcing chain. The map enables the explicit clinical prediction that mid-life stages invert before early stages.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.