CoherentRecognition
plain-language theorem explainer
CoherentRecognition assembles a sequence of recognition events over the naturals, a reference event, and a witness that at least two events differ in state. It is invoked by the Observer structure and the master certificate observer_forcing_status. The declaration is a bare structure definition.
Claim. A coherent recognition structure consists of a map from natural numbers to recognition events (positive reals), a distinguished reference event, and a witness that at least two events have distinct states.
background
RecognitionEvent is a structure carrying a positive real state together with a positivity proof; its cost is defined as the J-cost. The module sets out a seven-step argument that any non-trivial coherent recognition forces an observer by attaching a persistent reference. Upstream, Jcost_eq_zero_iff states that the J-cost vanishes if and only if the argument equals 1 for positive reals. The local theoretical setting is the forcing chain from multiple distinguishable events to an observer-like substructure.
proof idea
The declaration is a structure definition. It introduces the three fields directly with no lemmas or computational content.
why it matters
This supplies the second step in the module's seven-step argument: a coherent recognition structure carries multiple distinguishable events. It is used to define the Observer structure, which adds the IsPersistent condition on the reference, and appears in the master certificate observer_forcing_status. The construction connects to the Recognition Science forcing chain by showing how non-trivial recognition forces an observer-like substructure without external posits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.