lightCone_before_photonEM
plain-language theorem explainer
The theorem asserts that the light-cone stage precedes the photon-electromagnetic stage in the pre-temporal forcing order of Recognition Science. Researchers tracing the emergence of spacetime from recognition primitives cite this ordering to separate primitive distinction from electromagnetic propagation. The proof succeeds by a single invocation of the decidable instance of the Before predicate, which compares the dependency ranks of the two stages.
Claim. In the pre-temporal forcing order, the light-cone stage precedes the photon-electromagnetic stage: $Before(lightCone, photonEM)$, where $Before(a,b)$ holds precisely when the dependency rank of stage $a$ is strictly smaller than the rank of stage $b$.
background
The module records the dependency order that exists before time in Recognition Science. Physical time is itself a forced object, so the ordering is a forcing order: stage A is before stage B when B requires A as prior structure. The central distinction drawn is between recognition-light (the primitive revealing act of distinction, prior to time and spacetime) and physical light (the null-cone, photon, and electromagnetic carrier, downstream of J-cost, ticks, and spacetime).
proof idea
The proof is a one-line wrapper that applies the decidable instance of Before. That instance reduces the claim to a numerical comparison via Nat.decLt on the ranks assigned to lightCone and photonEM inside the Stage inductive type.
why it matters
This result supplies the light_cone_pre_photon field of the PreTemporalOrderCert record. It thereby certifies that the light-cone structure is forced prior to photon electromagnetic propagation, reinforcing the module's separation of primitive recognition-light from physical light as the first boundary of spacetime. The ordering is consistent with the broader forcing chain in which recognition precedes the emergence of time and spacetime.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.