DiscreteEventSystem
plain-language theorem explainer
A discrete event system is a countable type of events: the minimal carrier on which recognition, evolution, and conserved flow are later defined. Anyone proving conservation necessity from the Meta-Principle cites this as the ambient discrete setting. It is a bare structure declaration (carrier plus countability), not a proved claim.
Claim. A discrete event system is a pair $(E,\kappa)$ where $E$ is a type of events and $\kappa$ witnesses that $E$ is countable.
background
The module Conservation Necessity aims to derive non-trivial conservation from the Meta-Principle (MP), rather than postulating distinguishability as an axiom. The chain is: MP makes recognition possible on non-empty types; recognition needs distinction; distinction in a discrete setting needs structural difference, read as non-zero flow; hence MP forces non-trivial conserved flow.
This structure supplies the ambient discrete world for that argument: only a countable event carrier. Related but distinct "Event" notions appear upstream (directed postings with positive ratio in rung coarsening; finite distinction predicates on Fin (N+1) in the primitive recognition calculus). Here the carrier is abstract and untyped beyond countability.
Immediately downstream, event evolution packages a relation on this carrier with a well-foundedness witness, and finite-support integer flows live on pairs of events. Distinguishability is then identified with non-triviality of such a flow.
proof idea
No proof: this is a structure definition. It declares a type field Event and a countability witness. Downstream constructions (evolution, finite-support flow, edge flows, distinguishability) take an instance of this structure as their first parameter.
why it matters
This is the base typeclass-like carrier for the whole conservation-necessity development. Parent results that quantify over it include the key lemma that distinct evolved events force non-zero flow on that edge, the identification of distinguishability with non-trivial flow, edge-supported unit flows, and the headline theorem that MP plus a non-trivial evolution yields some non-trivial conserved flow.
That headline result replaces the former axiom that recognition requires distinguishability in the ledger-necessity layer. In Recognition Science terms, "flow" is information transfer during recognition; proving existence of non-trivial flow from MP closes a gap between the Meta-Principle and conservation structure, rather than assuming conservation or distinguishability outright. Countability keeps the discrete, ledger-style setting aligned with the framework's discrete recognition events (as opposed to a continuous field ontology).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.