count_eq_card
plain-language theorem explainer
For a finite distinction event on Fin(N+1), the event count equals the cardinality of the selected finset. Probability and measure lemmas in the primitive recognition calculus cite this to move between the count API and Finset.card. The equality is definitional; the proof is a one-line reflexivity.
Claim. For every $N \in \mathbb{N}$ and every finite distinction event $E$ on $\mathrm{Fin}(N+1)$ (a predicate $E : \mathrm{Fin}(N+1) \to \mathrm{Prop}$), the number of points satisfying $E$ equals the cardinality of the finite set of those points.
background
In this module a finite distinction event on the nonempty discrete space $\mathrm{Fin}(N+1)$ is simply a predicate $E : \mathrm{Fin}(N+1) \to \mathrm{Prop}$. The count of an event is the number of indices where the predicate holds; the selected finset is the corresponding subset of $\mathrm{Fin}(N+1)$ obtained by filtering the universe.
Both constructions are classical and noncomputable only insofar as Prop-valued filters require classical choice of decidability. The local setting is a discrete probability calculus for primitive recognition: counts feed normalized probabilities on finite distinction spaces, before continuum or measure-theoretic structure is introduced.
Upstream, the same counting pattern appears in cosmology rung-coarsening (multiset card of recognition events) and lattice edge sets, but here the ambient space is the elementary finite type $\mathrm{Fin}(N+1)$.
proof idea
One-line definitional reflexivity. By construction the count is exactly the cardinality of the filtered universe finset that defines the selected set of the event, so rfl closes the goal with no lemmas or rewriting.
why it matters
This identity is the bridge used by the disjoint-additivity theorem for counts: disjoint finite events have additive counts, proved by identifying the count of a disjunction with the card of a union and applying Finset card-union under a disjointness hypothesis. Without the definitional link, every later probability identity (empty event, universe, monotonicity, nonnegativity, bound by one) would have to re-expand the filter each time.
In the Recognition Science stack this sits in the foundation layer that turns raw distinction events into a discrete probability calculus. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder; it supplies the elementary counting hygiene those later layers assume when they talk about finite recognition samples.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.