eventFinset
plain-language theorem explainer
Extracts the finite support of a distinction event on the discrete space {0,...,N} as an ordinary Finset. Counting lemmas and the uniform rational probability on finite recognition events cite it as the bridge from predicates to cardinalities. The body is a classical filter of the universe by the event predicate.
Claim. For $N\in\mathbb{N}$ and an event $E$ (a predicate on $\{0,\ldots,N\}$), write $\mathrm{supp}(E):=\{i\in\{0,\ldots,N\}:E(i)\}$ as a finite set.
background
In the primitive recognition calculus, a finite distinction event on the nonempty discrete space $\mathrm{Fin}(N+1)\cong{0,\ldots,N}$ is simply a predicate $E:\mathrm{Fin}(N+1)\to\mathrm{Prop}$. The module builds a uniform finite probability as a rational counting ratio on such events.
Working with counts and additivity requires a genuine Finset, not a bare predicate. This definition is the standard support extraction: keep those indices of the universe that satisfy $E$. Sibling notions count and prob then read off cardinality and the normalized ratio against $N+1$.
Related ledger and cosmology modules use other "Event" types (directed postings with ratios, lattice edge sets). Here the meaning is strictly the finite Boolean event on $\mathrm{Fin}(N+1)$.
proof idea
Definitional, not a proof. Under classical logic, return Finset.univ.filter applied to the predicate $E$. No lemmas are invoked; the term is the filtered universe.
why it matters
Local plumbing for the finite counting measure on distinction events. Downstream, count_eq_card identifies count E with the cardinality of this Finset (by rfl), and count_disjoint_or uses the Finset union identity for supports of disjoint events to get additivity of counts.
Those facts underwrite nonnegativity and normalization of the uniform rational probability (prob) in the same module. In the broader Recognition stack this is foundation-layer discrete measure structure, not yet the Born rule on quantum ledgers or continuum bridges; it supplies the finite-sample counting language those later layers can specialize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.