`spacetime_before_lightCone`

proved

show as: view math explainer →

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

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

 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
 128  decide
 129
 130theorem recognition_light_before_spacetime :
 131    Before RecognitionLight Stage.spacetime := by
 132  decide
 133
 134theorem recognition_light_before_physical_light :
 135    Before RecognitionLight PhysicalLight := by

papers checked against this theorem

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