PreTemporalOrderCert
plain-language theorem explainer
PreTemporalOrderCert packages six specific precedence assertions that fix the dependency order among recognition-light, physical light, time-tick, spacetime, light-cone, photon-EM, and the two observer stages. A foundation researcher tracing how time and observers emerge from recognition would cite the certificate to anchor the pre-temporal chain. The structure is assembled directly from the decidable rank comparisons supplied by the Stage inductive type and the Before definition.
Claim. Let $R$ be the recognition-light stage, $T$ the time-tick stage, $S$ spacetime, $L$ the physical-light stage, $C$ the light-cone stage, $P$ the photon-EM stage, $O_p$ the primitive-observer stage, and $O$ the physical-observer stage. PreTemporalOrderCert is the structure whose fields assert $R$ precedes $T$, $R$ precedes $S$, $S$ precedes $L$, $C$ precedes $P$, $O_p$ precedes $T$, and $L$ precedes $O$, where precedence means strictly lower rank in the Stage dependency ordering.
background
The module defines a pre-temporal forcing order that records logical dependencies rather than chronological succession. The central object is the inductive type Stage whose constructors run from distinction through recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick, lightCone, photonEM, and embodiedObserver. The Before predicate on two stages holds precisely when the first has smaller rank than the second; this predicate is decidable by the standard Nat.lt instance.
proof idea
PreTemporalOrderCert is a plain structure definition whose six fields are simply the six Before propositions. Each proposition is discharged in a separate theorem by the decide tactic, which reduces the rank comparison to a concrete Nat.lt goal that is solved automatically.
why it matters
The certificate is instantiated verbatim inside the cert definition and shown to be inhabited by the theorem cert_inhabited. It therefore supplies a concrete witness for the entire pre-temporal order that the module records. This order distinguishes the pre-temporal recognition-light (the primitive revealing act) from physical light (the null boundary that appears only after spacetime), a distinction required by the forcing chain that places timeTick after jCost and arithmeticObject.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.