`rcl_before_jCost`

proved

show as: view math explainer →

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

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

formal source

  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
 100
 101theorem time_before_spacetime :
 102    Before Stage.timeTick Stage.spacetime := by
 103  decide
 104
 105theorem spacetime_before_lightCone :
 106    Before Stage.spacetime Stage.lightCone := by
 107  decide
 108
 109theorem lightCone_before_photonEM :
 110    Before Stage.lightCone Stage.photonEM := by
 111  decide
 112
 113theorem photonEM_before_embodiedObserver :
 114    Before Stage.photonEM Stage.embodiedObserver := by
 115  decide
 116
 117/-! ## Light: two senses -/
 118
 119/-- Recognition-light: the revealing act of an interface making distinction

papers checked against this theorem

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