theorem
proved
recognition_light_before_spacetime
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.PreTemporalForcingOrder on GitHub at line 130.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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
152as soon as recognition, not merely bare abstract distinction, is in play. -/
153def PrimitiveObserver : Stage := Stage.recognitionInterface
154
155/-- Embodied observer: a physical subsystem with finite resolution, downstream
156of spacetime and physical light. -/
157def PhysicalObserver : Stage := Stage.embodiedObserver
158
159theorem primitive_observer_before_time :
160 Before PrimitiveObserver Stage.timeTick := by