`distinction_first`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PreTemporalForcingOrder on GitHub at line 69.

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

  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 :
  78    Before Stage.singleValuedPredicate Stage.symmetricComparison := by
  79  decide
  80
  81theorem symmetry_before_composition :
  82    Before Stage.symmetricComparison Stage.compositionConsistency := by
  83  decide
  84
  85theorem composition_before_rcl :
  86    Before Stage.compositionConsistency Stage.rcl := by
  87  decide
  88
  89theorem rcl_before_jCost :
  90    Before Stage.rcl Stage.jCost := by
  91  decide
  92
  93theorem jCost_before_arithmetic :
  94    Before Stage.jCost Stage.arithmeticObject := by
  95  decide
  96
  97theorem arithmetic_before_time :
  98    Before Stage.arithmeticObject Stage.timeTick := by
  99  decide

papers checked against this theorem

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