physical_observer_after_physical_light
plain-language theorem explainer
The theorem places the embodied-observer stage after the light-cone stage in the pre-temporal forcing hierarchy. A researcher assembling the dependency chain from spacetime boundaries to physical subsystems would cite it when confirming that observers presuppose the null cone. The proof is a one-line decision procedure that evaluates the rank comparison directly via the decidable instance of Before.
Claim. The forcing priority satisfies $rank(PhysicalLight) < rank(PhysicalObserver)$, where PhysicalLight is the light-cone stage and PhysicalObserver is the embodied-observer stage.
background
The Pre-Temporal Forcing Order module defines Before a b to mean rank a < rank b, with an instance that makes the relation decidable by natural-number comparison. PhysicalLight is the Stage.lightCone, the null boundary and electromagnetic carrier of spacetime. PhysicalObserver is the Stage.embodiedObserver, a finite-resolution physical subsystem that appears only after spacetime has been assembled.
proof idea
The proof is a one-line wrapper that applies the decidable instance of Before, reducing the claim to a direct Nat.lt comparison of the ranks assigned to the two stages.
why it matters
The result supplies one field of the PreTemporalOrderCert certificate that collects the ordering facts needed by the larger forcing chain. It confirms that physical light precedes the embodied observer, aligning with the T0-to-T8 sequence in which spacetime and its null cone are prerequisites for observers. No open scaffolding remains for this link.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.