Observer
plain-language theorem explainer
An observer packages a coherent recognition structure (events with at least two distinct states plus a reference) together with a zero J-cost witness on that reference. Researchers tracing the observer-forcing argument or building deterministic projections cite this structure. It is introduced by a direct structure definition that assembles the two fields from the module's prior definitions of CoherentRecognition and IsPersistent.
Claim. An observer consists of a coherent recognition structure $C$ (a map from naturals to recognition events, a reference event, and a witness that at least two events have distinct states) together with a proof that the J-cost of the reference event is zero.
background
The module establishes that non-trivial coherent recognition forces an observer-like substructure through seven explicit steps. CoherentRecognition is the structure carrying a sequence of recognition events, a reference event, and a nontriviality witness that at least two events differ in state. IsPersistent is the predicate asserting that a reference event has J-cost exactly zero, justified because any positive cost would shift under context change while zero is the unique global minimum. The cost of any recognition event is defined as its J-cost via Cost.Jcost. The local setting is the derivation of the observer directly from the Recognition Composition Law and the uniqueness of the zero-cost state.
proof idea
This is a structure definition with exactly two fields. The first field imports a CoherentRecognition instance; the second field applies the IsPersistent predicate to its reference component. No lemmas, tactics, or reductions are invoked.
why it matters
The structure realizes step 7 of the module's forcing argument and is the target of nontrivial_recognition_forces_observer. It is used directly by has_distinguishable_events, cooper_paired_reference_yields_observer, cooper_pairing_yields_persistent, and the projection constructions in Determinism. It supplies the fixed identity-tick reference required for the eight-tick octave and the transition from recognition to deterministic observation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.