`arithmetic_before_time`

proved

show as: view math explainer →

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

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

  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
 120available. This is pre-temporal. -/
 121def RecognitionLight : Stage := Stage.recognitionInterface
 122
 123/-- Physical light: the null boundary / electromagnetic carrier of spacetime. -/
 124def PhysicalLight : Stage := Stage.lightCone
 125
 126theorem recognition_light_before_time :
 127    Before RecognitionLight Stage.timeTick := by

papers checked against this theorem

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