`developmentReversalCert`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.CrossDomain.DevelopmentReversal on GitHub at line 67.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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

papers checked against this theorem

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