PrimitiveObserver
plain-language theorem explainer
PrimitiveObserver names the recognitionInterface stage in the pre-temporal forcing chain. Researchers deriving observer emergence from nontrivial recognition would cite this when placing the interface prior to timeTick. The definition is a direct alias to the second constructor of the Stage inductive type.
Claim. Let the primitive observer be the recognition interface stage in the pre-temporal forcing order, i.e., the stage at which a recognizer/interface is forced once recognition (beyond bare distinction) is present.
background
The module records the forcing order among stages that must precede physical time. Recognition-light (the primitive revealing act of distinction) is prior to time and spacetime, while physical light is downstream of J-cost, ticks, and spacetime. Stage is the inductive type of dependency stages: distinction, recognitionInterface, singleValuedPredicate, symmetricComparison, compositionConsistency, rcl, jCost, arithmeticObject, timeTick. The supplied DOC_COMMENT states that the primitive observer is a recognizer/interface forced as soon as recognition is in play. Upstream, ObserverFromRecognition defines PrimitiveObserver K as an abbreviation for PrimitiveInterface K, with the kernel being reflexive.
proof idea
One-line definition that directly aliases Stage.recognitionInterface.
why it matters
This definition supplies the stage referenced by PreTemporalOrderCert (primitive_observer_pre_time : Before PrimitiveObserver Stage.timeTick) and by primitive_observer_before_time. It fills the forcing-chain step at which nontrivial recognition forces an interface structure, prior to timeTick. The placement aligns with the module's distinction between recognition-light (pre-temporal) and physical light (post-spacetime). It is used downstream in nontrivial_recognition_forces_observer and RecognizerInducesLogicCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.