`Stage`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PreTemporalForcingOrder
domain: Foundation
line: 30 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.PreTemporalForcingOrder on GitHub at line 30.

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

depends on

used by

formal source

  27/-! ## Stages -/
  28
  29/-- The dependency stages in the pre-temporal forcing chain. -/
  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. -/
  47def rank : Stage → ℕ
  48  | .distinction => 0
  49  | .recognitionInterface => 1
  50  | .singleValuedPredicate => 2
  51  | .symmetricComparison => 3
  52  | .compositionConsistency => 4
  53  | .rcl => 5
  54  | .jCost => 6
  55  | .arithmeticObject => 7
  56  | .timeTick => 8
  57  | .spacetime => 9
  58  | .lightCone => 10
  59  | .photonEM => 11
  60  | .embodiedObserver => 12

papers checked against this theorem

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