count_empty
plain-language theorem explainer
The constantly false event on the discrete space Fin(N+1) has count zero. Anyone building normalized event probabilities from finite filter-card counts cites this base case. The proof is a one-line classical simplification that unfolds the definition of count.
Claim. For every natural number $N$, the number of points of $\mathrm{Fin}(N+1)$ that satisfy the constantly false predicate is $0$.
background
In Primitive Recognition Calculus, an event on a finite discrete space of size $N+1$ is a predicate $E:\mathrm{Fin}(N+1)\to\mathrm{Prop}$. The count of $E$ is the cardinality of the filtered universe:
$\lvert{i\in\mathrm{Fin}(N+1):E(i)}\rvert$, implemented as Finset.univ.filter followed by card.
This module equips those finite events with an elementary probability calculus, taking probability as count divided by the size of the universe. The impossible event is the constantly false predicate.
The local count is the filter-card definition above. The Cosmology.RungCoarsen count (multiset card of log-ratio events) is a separate name and is not used in the argument.
proof idea
Enable classical logic, then simp on the definition of count. Filtering Finset.univ by the constantly false predicate yields the empty finset, whose cardinality is zero, so the equality holds in one simplification step.
why it matters
This is the zero base case for the discrete probability layer in Foundation.PrimitiveRecognitionCalculus. Downstream, prob_empty cites it directly: the impossible event has probability zero via simp [prob, count_empty]. That normalization is required before nonnegativity, monotonicity, and certainty lemmas can be stated cleanly. It is bookkeeping rather than a forcing-chain landmark (T0–T8), but the delta-probability constructions that sit above this module rely on a well-behaved empty-event count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.