`RecognitionLight`

definition

show as: view math explainer →

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

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

 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 :
 144    ¬∀ s : Stage, s ≠ PhysicalLight → Before PhysicalLight s := by
 145  intro h
 146  have hbad := h Stage.distinction (by decide)
 147  norm_num [Before, PhysicalLight, rank] at hbad
 148
 149/-! ## Observer: two senses -/
 150
 151/-- Primitive observer-like structure: a recognizer/interface. This is forced

papers checked against this theorem

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