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

Stage

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  30inductive Stage where
  31  | distinction
  32  | recognitionInterface
  33  | singleValuedPredicate
  34  | symmetricComparison
  35  | compositionConsistency
  36  | rcl
  37  | jCost
  38  | arithmeticObject
  39  | timeTick
  40  | spacetime
  41  | lightCone
  42  | photonEM
  43  | embodiedObserver
  44  deriving DecidableEq, Repr
  45
  46/-- A numerical rank for the forcing order. Lower rank means prior structure. -/

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.