`Before`

definition

show as: view math explainer →

module: IndisputableMonolith.Foundation.PreTemporalForcingOrder
domain: Foundation
line: 63 · 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 63.

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

  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 :
  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 :

papers checked against this theorem

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