HasRecognitionEvents
plain-language theorem explainer
A predicate asserting that a discrete event system with a given evolution admits at least one recognition event. It is the non-vacuity interface used throughout the conservation-necessity argument: MP plus non-trivial structure yields recognition, and recognition yields non-trivial flow. The body is a pure existential over the local recognition-event type, witnessed by a trivial reflexivity on the source field.
Claim. For a discrete event system $E$ (countable carrier of events) and an event evolution $\mathrm{ev}$ on $E$ (a well-founded binary relation on events), $\mathrm{HasRecognitionEvents}(E,\mathrm{ev})$ holds if and only if there exists a recognition event on $(E,\mathrm{ev})$.
background
The module derives non-trivial conservation from the Meta-Principle (MP: "Nothing cannot recognize itself"), so that recognition_requires_distinguishability need not be an axiom. The chain is: MP makes recognition possible on non-empty types; recognition requires distinction; distinction in a discrete event system requires non-zero flow; hence MP forces non-trivial conservation.
A discrete event system is a countable type of events. An event evolution packages a binary relation on those events together with a well-foundedness witness (no infinite descending chains). A recognition event, in this module's local sense, pairs two distinct events linked by the evolution relation: the minimal data that "something recognized something else."
Upstream foundation material supplies related recognition-event structures (agent pairs with positive ratio; positive recognition states) and the empty type Nothing as the absolute encoding of emptiness. Those feed the MP side of the story; this definition only records that recognition events are present for a given $(E,\mathrm{ev})$.
proof idea
Definitional, not a proof. The predicate is the proposition $\exists, re : \mathrm{RecognitionEvent}, E, \mathrm{ev},; re.\mathrm{source}=re.\mathrm{source}$. The equality is a trivial inhabitation witness so the existential is a pure existence claim. Inhabitants are supplied later by constructing a recognition event from two distinct evolving events.
why it matters
This is the non-vacuity gate in the conservation-necessity chain. Downstream, nontrivial_system_has_recognition_events shows that any system with at least two distinct events related by evolution satisfies the predicate ("minimal structure for recognition"). The refined main theorem recognition_implies_nontrivial_flow_exists then takes MP plus this predicate and produces a finite-support flow that is non-trivial: "the recognition flow itself is non-trivial."
That pair replaces the old axiom of the same name in LedgerNecessity: the question shifts from "is every flow non-trivial?" to "does a non-trivial flow exist?" Closing this gap is step 1–2 of the module argument (MP implies recognition is meaningful; recognition events exist in non-trivial systems) and feeds the forcing of conservation structure used in the broader verification exclusivity framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.