`EriksonStage`

definition

show as: view math explainer →

module: IndisputableMonolith.CrossDomain.DevelopmentReversal
domain: CrossDomain
line: 20 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.CrossDomain.DevelopmentReversal on GitHub at line 20.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

used by

formal source

  17
  18namespace IndisputableMonolith.CrossDomain.DevelopmentReversal
  19
  20inductive EriksonStage where
  21  | trustVsMistrust
  22  | autonomyVsShame
  23  | initiativeVsGuilt
  24  | industryVsInferiority
  25  | identityVsConfusion
  26  | intimacyVsIsolation
  27  | generativityVsStagnation
  28  | integrityVsDespair
  29  deriving DecidableEq, Repr, BEq, Fintype
  30
  31theorem eriksonCount : Fintype.card EriksonStage = 8 := by decide
  32theorem erikson_eq_2cube : Fintype.card EriksonStage = 2 ^ 3 := by decide
  33
  34/-- Reversal map on `Fin 8`. -/
  35def reverse : Fin 8 → Fin 8 := fun k => ⟨7 - k.val, by omega⟩
  36
  37/-- Reversal is an involution: reverse ∘ reverse = id. -/
  38theorem reverse_involution (k : Fin 8) : reverse (reverse k) = k := by
  39  apply Fin.ext
  40  simp only [reverse]
  41  omega
  42
  43/-- Reversal swaps first and last. -/
  44theorem reverse_swaps_endpoints :
  45    reverse ⟨0, by decide⟩ = ⟨7, by decide⟩ ∧
  46    reverse ⟨7, by decide⟩ = ⟨0, by decide⟩ := by
  47  refine ⟨?_, ?_⟩
  48  · apply Fin.ext; simp [reverse]
  49  · apply Fin.ext; simp [reverse]
  50

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.