PhysicalObserver
plain-language theorem explainer
PhysicalObserver names the embodied observer stage in the pre-temporal forcing chain. Researchers establishing ordering constraints between spacetime and observers cite this when proving that physical light precedes any embodied subsystem. The definition is a direct one-line assignment to the embodiedObserver constructor of the Stage inductive.
Claim. Define the physical observer as the embodied observer stage: $PhysicalObserver := Stage.embodiedObserver$, where this stage lies downstream of spacetime and physical light in the forcing order.
background
The module records a forcing order that exists before time, with each stage required as prior structure for the next. Stage is the inductive type listing these stages, beginning with distinction and recognitionInterface and continuing through symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick, and embodiedObserver. The module distinguishes primitive recognition-light, which precedes time and spacetime, from physical light, which is the null-cone carrier downstream of J-cost, ticks, and spacetime.
proof idea
The definition is a one-line wrapper that directly assigns PhysicalObserver to the embodiedObserver constructor of the Stage inductive.
why it matters
This supplies the embodied observer stage required by physical_observer_after_physical_light, which proves Before PhysicalLight PhysicalObserver, and by the PreTemporalOrderCert structure that records the full pre-temporal ordering. It fills the segment of the chain after spacetime formation, consistent with the module's separation of recognition-light from physical light. The placement supports the transition to finite-resolution subsystems before timeTick emerges in the forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.