pith. machine review for the scientific record. sign in
def definition def or abbrev

cert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 181def cert : PreTemporalOrderCert where
 182  recognition_light_pre_time := recognition_light_before_time

proof body

Definition body.

 183  recognition_light_pre_spacetime := recognition_light_before_spacetime
 184  physical_light_post_spacetime := physical_light_after_spacetime
 185  light_cone_pre_photon := lightCone_before_photonEM
 186  primitive_observer_pre_time := primitive_observer_before_time
 187  physical_observer_post_light := physical_observer_after_physical_light
 188

depends on (7)

Lean names referenced from this declaration's body.