count_univ
plain-language theorem explainer
On the discrete sample space Fin(N+1), the always-true event has cardinality N+1. Probability normalizations in the primitive recognition calculus cite this identity. The proof is a classical one-line simplification of the filter-card definition of the event count.
Claim. For every natural number $N$, the count of points $i \in \mathrm{Fin}(N+1)$ satisfying the always-true predicate equals $N+1$.
background
In the DeltaProbability module, an event on parameter $N$ is a predicate on the finite type $\mathrm{Fin}(N+1)$. The associated count is the cardinality of the Finset of indices that satisfy the predicate: filter the universe by the event and take card.
This is the discrete counting measure underlying the module's probability map (count divided by $N+1$). The certain event is the constantly-true predicate, so its support is the whole universe.
Upstream, the same counting idea appears as multiset cardinality in RungCoarsen; here it is specialized to filtered Finsets on $\mathrm{Fin}(N+1)$.
proof idea
Classical mode is opened so that decidability of the constantly-true predicate is available. Unfolding the local count definition reduces the goal to the cardinality of $\mathrm{Finset.univ.filter}(\lambda,i.,\mathrm{True})$ on $\mathrm{Fin}(N+1)$. Simp discharges that filter as the full universe and applies the standard card formula $\lvert\mathrm{Fin}(N+1)\rvert=N+1$.
why it matters
The immediate parent is prob_univ, which rewrites the certain-event probability through this identity and concludes it equals one by division by the nonzero rational $N+1$. That unit-mass fact anchors the finite probability space used in the primitive recognition calculus.
Within Recognition Science foundation work, discrete event measures on octave-sized or ladder-sized index sets feed later forcing and coarsening arguments. This lemma is the cardinality half of the normalization; without it, the certain-event probability is not closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.