reverse_involution
plain-language theorem explainer
The map sending each of the eight Erikson stages to its counterpart by subtracting the index from seven is its own inverse. Modelers of neurodegeneration as stage reversal cite this to confirm the 2^3 cycle closes after two steps. The proof reduces the claim to integer arithmetic on the underlying values of Fin 8 via extension, simplification of the reverse definition, and the omega tactic.
Claim. Let $r : Fin 8 → Fin 8$ be defined by $r(k) = 7 - k$. Then $r(r(k)) = k$ for every $k$.
background
The module treats Erikson's eight life stages as a 2³ tick cycle. The reversal map is defined by reverse k := ⟨7 - k.val, by omega⟩, an order-reversing function on Fin 8 that stays inside the finite set. This construction supports the prediction that neurodegeneration traverses the stages backward from the forward developmental order.
proof idea
The term proof applies Fin.ext to reduce to equality of the underlying natural numbers, simplifies the two nested applications of reverse using its definition, and discharges the arithmetic identity 7 - (7 - k.val) = k.val with the omega tactic.
why it matters
This result supplies the involution field required by developmentReversalCert, which packages the full certificate including eriksonCount, erikson_eq_2cube, and the endpoint-swap lemmas. It completes the structural claim of the C6 module that the eight-tick octave is closed under reversal, consistent with the T7 forcing-chain landmark of period 2³.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.