`rank`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PreTemporalForcingOrder on GitHub at line 47.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  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
  61
  62/-- Forcing priority: `a` is before `b` iff its dependency rank is smaller. -/
  63def Before (a b : Stage) : Prop := rank a < rank b
  64
  65instance (a b : Stage) : Decidable (Before a b) := Nat.decLt _ _
  66
  67/-! ## Main order theorems -/
  68
  69theorem distinction_first (s : Stage) (h : s ≠ Stage.distinction) :
  70    Before Stage.distinction s := by
  71  cases s <;> simp [Before, rank] at h ⊢
  72
  73theorem recognition_before_predicate :
  74    Before Stage.recognitionInterface Stage.singleValuedPredicate := by
  75  decide
  76
  77theorem predicate_before_symmetry :

papers checked against this theorem

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