reverse_involution
The reversal map on the eight-element set of Erikson stages satisfies r(r(k)) = k for every k. Researchers modeling neurodegeneration as backward traversal of the 2^3 stage ladder would cite this to anchor the involution property. The proof is a one-line wrapper that applies Fin.ext, simplifies the definition of reverse, and closes with omega.
claimLet $r$ be the map on the set of eight stages given by $r(k) = 7 - k$. Then $r(r(k)) = k$ for every stage index $k$.
background
The module formalizes C6: Erikson's eight life stages are treated as a 2^3 tick cycle, with reversal defined by the order-reversing map $r(k) = 7 - k$ on Fin 8. This supplies the structural claim that neurodegeneration runs the ladder backward, so that mid-life stages invert before early ones. The upstream definition of reverse is the function fun k => ⟨7 - k.val, by omega⟩, which is used directly in the statement.
proof idea
The term proof applies Fin.ext to reduce the equality on Fin 8 to an equality on the underlying natural numbers. It then simplifies the nested applications of reverse using the definition, after which omega discharges the resulting arithmetic identity 7 - (7 - k) = k.
why it matters in Recognition Science
This theorem supplies the involution component of developmentReversalCert, which assembles the full certificate that the eight stages form a closed reversal cycle. It realizes the eight-tick octave (T7) inside the Recognition framework by exhibiting an explicit involution on the 2^3 stages. The result closes the formal part of the predicted clinical pattern without addressing empirical validation.
scope and limits
- Does not derive the reversal map from the forcing chain T0-T8.
- Does not prove any clinical observation about dementia progression.
- Does not extend the involution property to other stage models.
- Does not address the Berry creation threshold or phi-ladder mass formulas.
Lean usage
example (k : Fin 8) : reverse (reverse k) = k := reverse_involution kformal statement (Lean)
38theorem reverse_involution (k : Fin 8) : reverse (reverse k) = k := by
proof body
Term-mode proof.
39 apply Fin.ext
40 simp only [reverse]
41 omega
42
43/-- Reversal swaps first and last. -/