count
plain-language theorem explainer
Counts how many points of the finite index set Fin(N+1) satisfy a given distinction event. Anyone building discrete probabilities or measure-one statements on finite recognition events cites it as the raw cardinality. The body is a classical Finset filter of the universe followed by card.
Claim. Fix $N \in \mathbb{N}$ and a finite distinction event $E$ on the nonempty space $\mathrm{Fin}(N+1)$ (i.e., a predicate $E : \mathrm{Fin}(N+1) \to \mathrm{Prop}$). The count of $E$ is the number of indices $i$ for which $E(i)$ holds: $\#\{ i \in \mathrm{Fin}(N+1) : E(i) \}$.
background
In this module a finite distinction event on parameter $N$ is a predicate on the nonempty finite type $\mathrm{Fin}(N+1)$. That type is the discrete sample space for the primitive recognition calculus: each index is a distinguishable slot, and the event marks which slots fire.
The count is the unnormalized measure of an event. Sibling definitions turn it into a probability by dividing by the universe size $N+1$, and prove elementary facts (empty event has count zero, the universal event has count $N+1$, monotonicity, nonnegativity of probabilities).
Related counting idioms appear elsewhere in the monolith (multiset event counts in rung coarsening, edge Finsets on lattice balls), but here the object is strictly the cardinality of a predicate on $\mathrm{Fin}(N+1)$.
proof idea
Definition, not a proof. Under classical logic it builds the Finset of all $i : \mathrm{Fin}(N+1)$ with $E,i$ true by filtering Finset.univ, then returns that Finset's card. Noncomputable only because Prop-valued filters need classical choice of decidability.
why it matters
This is the numerator for discrete recognition probabilities in the primitive calculus: once count and the universe cardinality are in hand, prob and the standard bounds (prob_nonneg, prob_le_one, empty/univ cases) follow immediately. Downstream the same counting pattern supports algebraic weight and nonzero-vector counts (e.g. Hamming weights and $2^D-1$ nonzero vectors in $\mathbb{F}_2^D$), shell-capacity bookkeeping in the periodic table, and other finite ledger tallies across chemistry and constants modules.
In the Recognition Science stack, finite distinction events are the atomic yes/no postings before continuum limits and the forcing chain (T5 J-cost, T7 eight-tick octave). A clean event count keeps those discrete layers honest and feeds any later claim that a recognition event has positive or full measure on a finite window.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.