PrimitiveObserver
plain-language theorem explainer
PrimitiveObserver names the recognitionInterface stage in the pre-temporal forcing chain. Researchers tracing observer emergence from recognition cite this when establishing that nontrivial recognition forces an interface structure prior to time. The declaration is a direct alias to the recognitionInterface constructor of the Stage inductive type.
Claim. Let Stage be the inductive type of pre-temporal dependency stages with constructors distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. Define PrimitiveObserver as the stage recognitionInterface.
background
The module records the forcing order among structures that must precede physical time. Stage enumerates these dependency stages, beginning with distinction and recognitionInterface. The module doc-comment distinguishes recognition-light (the primitive revealing act of distinction) from physical light (the null-cone carrier downstream of J-cost and spacetime). Upstream, ObserverFromRecognition defines an abbrev PrimitiveObserver (K : Type*) := PrimitiveInterface K and states that the observer is the interface structure recognition forces, not an external entity.
proof idea
This is a one-line definition aliasing the recognitionInterface constructor of Stage. No lemmas or tactics are applied beyond the inductive definition itself.
why it matters
The definition supplies the stage referenced in PreTemporalOrderCert for the assertion primitive_observer_pre_time : Before PrimitiveObserver Stage.timeTick and in the theorems primitive_observer_before_time and primitive_observer_before_physical_light. It marks the point in the forcing chain where recognition (after bare distinction) forces an interface, feeding the later steps that place recognition-light before timeTick and spacetime while physical light follows spacetime. This aligns with the pre-temporal order described in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.