cert
plain-language theorem explainer
This definition assembles a certificate structure that bundles six forcing-order relations among pre-temporal primitives in Recognition Science. It records recognition light as prior to time ticks and spacetime, spacetime as prior to physical light, the light cone as prior to photon emission, and the primitive observer as prior to time. Workers on the T0-T8 forcing chain cite it to fix the dependency order before time emerges. The construction is a direct structure instantiation that assigns the six individual ordering theorems to the fields of
Claim. Let $cert$ be the structure of type $PreTemporalOrderCert$ whose fields witness the relations $Before(RecognitionLight, Stage.timeTick)$, $Before(RecognitionLight, Stage.spacetime)$, $Before(Stage.spacetime, PhysicalLight)$, $Before(Stage.lightCone, Stage.photonEM)$, $Before(PrimitiveObserver, Stage.timeTick)$, and $Before(PhysicalLight, PhysicalObserver)$.
background
The module records forcing orders that exist before physical time is itself forced. Recognition light is the primitive act of distinction; physical light is the null-cone carrier that appears only after spacetime. The certificate structure $PreTemporalOrderCert$ packages exactly these six relations so that downstream arguments can invoke the entire pre-temporal order by a single name. The six component theorems are proved by direct decision on the Stage ordering.
proof idea
One-line structure construction. The definition supplies the six fields of $PreTemporalOrderCert$ by direct assignment of the already-proved theorems lightCone_before_photonEM, physical_light_after_spacetime, physical_observer_after_physical_light, primitive_observer_before_time, recognition_light_before_spacetime, and recognition_light_before_time.
why it matters
The certificate closes the pre-temporal segment of the forcing chain (T0-T8) by collecting the relations that place recognition light before time and spacetime while placing physical light after spacetime. It supplies the concrete witness required by any later argument that treats time as a derived object. No downstream uses are recorded yet; the definition therefore functions as a stable interface for the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.