primitive_observer_before_time
plain-language theorem explainer
The primitive recognizer precedes the time tick in the pre-temporal forcing order. This ordering is cited when assembling the full PreTemporalOrderCert that places recognition before time. The proof is a one-line wrapper that invokes the decidable rank comparison for the Before relation.
Claim. The recognition interface stage precedes the time tick stage: rank(recognitionInterface) < rank(timeTick).
background
The module defines a forcing order among pre-temporal stages rather than chronological time. Stage is the inductive type with constructors distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Before a b is the proposition rank a < rank b, equipped with a decidable instance via Nat.decLt. PrimitiveObserver is the alias for the recognitionInterface stage. Upstream, ObserverFromRecognition states that a primitive observer is exactly the primitive interface forced once recognition is active.
proof idea
The proof is a one-line wrapper that applies the decidable instance of Before, which reduces the claim to a direct Nat comparison of the ranks of recognitionInterface and timeTick.
why it matters
This theorem supplies the primitive_observer_pre_time entry in the PreTemporalOrderCert record. It completes one link in the documented pre-temporal chain that runs from distinction through recognitionInterface to timeTick, before any spacetime or physical light appears. The result is used to certify that recognition-light structure is forced prior to the emergence of time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.