`photonEM_before_embodiedObserver`

proved

show as: view math explainer →

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

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

 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
 136  decide
 137
 138theorem physical_light_after_spacetime :
 139    Before Stage.spacetime PhysicalLight := by
 140  decide
 141
 142/-- Physical light is not first in the forcing order. It requires spacetime. -/
 143theorem physical_light_not_first :

papers checked against this theorem

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