pith. machine review for the scientific record. sign in
def definition def or abbrev high

reverse

show as:
view Lean formalization →

The reversal map on the eight-element cycle sends each index k to 7 minus k. Researchers modeling Erikson stages or eight-tick periodic systems in Recognition Science cite this definition to establish the involution property required for stage-order reversal. The definition is given directly by arithmetic on Fin 8 with a single omega tactic discharging the bound.

claimThe reversal function $r : [0..7] → [0..7]$ is defined by $r(k) = 7 - k$.

background

The CrossDomain.DevelopmentReversal module treats Erikson's eight life stages as a 2³ tick cycle. The reversal map formalizes the claim that neurodegeneration traverses these stages in reverse order, with the explicit statement that reverse k = 7 − k and that the map is an involution. Upstream results supply identity maps on algebraic structures and basic arithmetic on Peano objects that underwrite the Fin 8 construction.

proof idea

This is a direct one-line definition that constructs the Fin 8 element with value 7 - k.val and uses the omega tactic to confirm the result lies inside the interval.

why it matters in Recognition Science

The definition supplies the core map for the DevelopmentReversalCert structure and the theorems reverse_involution, reverse_swaps_endpoints, and midlife_inverts_first. It realizes the eight-tick octave (T7) inside the developmental-stage setting and feeds the double-entry ledger algebra that requires paired reverse edges. It touches the open question of whether the predicted midlife inversion matches observed dementia progression patterns.

scope and limits

Lean usage

example (k : Fin 8) : reverse (reverse k) = k := by simp [reverse]; omega

formal statement (Lean)

  35def reverse : Fin 8 → Fin 8 := fun k => ⟨7 - k.val, by omega⟩

proof body

Definition body.

  36
  37/-- Reversal is an involution: reverse ∘ reverse = id. -/

used by (26)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.