photonEM_before_embodiedObserver
plain-language theorem explainer
The pre-temporal forcing order places the electromagnetic photon stage before the embodied observer stage. Researchers mapping the emergence of spacetime and observers from recognition primitives would cite this link. The proof reduces to an automatic decision on the rank comparison via the built-in decidable instance for the Before relation.
Claim. $rank( photonEM ) < rank( embodiedObserver )$, where $Before(a,b)$ holds precisely when the dependency rank of stage $a$ is strictly smaller than that of stage $b$.
background
The module establishes a forcing order among dependency stages that precedes the emergence of physical time. Recognition-light (the primitive act of making distinction available) is pre-temporal, while physical light (null-cone photons) appears only after J-cost, ticks, and spacetime. The central definition is $Before(a,b) := rank(a) < rank(b)$, equipped with a decidable instance via Nat.decLt. The Stage inductive type enumerates the ordered dependency stages in this chain, beginning with distinction and recognitionInterface and continuing through later stages including photonEM and embodiedObserver.
proof idea
The proof is a one-line wrapper that invokes the decidable instance for Before, which reduces the rank comparison to a concrete Nat inequality that Lean resolves by decide.
why it matters
This theorem supplies one concrete link in the pre-temporal forcing chain documented in the module, separating the photon electromagnetic stage from the embodied observer stage. It directly supports the module's distinction between recognition-light (pre-temporal) and physical light (downstream of J-cost and spacetime). No downstream theorems are recorded in the used-by graph, leaving its integration with later results such as time_before_spacetime open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.