DevelopmentReversalCert

formal source

  57    (reverse ⟨6, by decide⟩).val < (reverse ⟨0, by decide⟩).val := by
  58  simp [reverse]
  59
  60structure DevelopmentReversalCert where
  61  stage_count : Fintype.card EriksonStage = 8
  62  two_cube : Fintype.card EriksonStage = 2 ^ 3
  63  involution : ∀ k : Fin 8, reverse (reverse k) = k
  64  endpoints_swap : reverse ⟨0, by decide⟩ = ⟨7, by decide⟩
  65  midlife_first : (reverse ⟨6, by decide⟩).val < (reverse ⟨0, by decide⟩).val
  66
  67def developmentReversalCert : DevelopmentReversalCert where
  68  stage_count := eriksonCount
  69  two_cube := erikson_eq_2cube
  70  involution := reverse_involution
  71  endpoints_swap := reverse_swaps_endpoints.1
  72  midlife_first := midlife_inverts_first
  73
  74end IndisputableMonolith.CrossDomain.DevelopmentReversal