prob_empty
plain-language theorem explainer
The impossible event on a finite distinction space of size N+1 has uniform counting probability zero. Anyone citing the delta-native probability axioms or the finite-layer headline package will use this fact. The argument is a one-line simplification through the counting definition and the empty-count lemma.
Claim. For every natural number $N$, the uniform counting probability of the empty (impossible) event on the finite set of $N+1$ distinction alternatives equals $0$.
background
In the Primitive Recognition Calculus, an event at parameter $N$ is a Boolean predicate on a finite index set of cardinality $N+1$ (the raw distinction alternatives). The count of an event is the number of indices that satisfy it. Probability is then the rational ratio of that count to $N+1$, so the construction is pure finite counting with no measure theory.
The empty-count lemma already records that the constantly-false predicate has count zero. This module is the delta-native finite layer: probability before continuum limits. Separate real-valued probability constructions elsewhere in the monolith (Born-rule amplitudes, Boltzmann factors, Gibbs weights on action sets) are not used here; they sit downstream or in parallel tracks.
proof idea
Classical logic is opened so the constantly-false predicate is decidable for counting. A single simp then unfolds the probability definition (count divided by $N+1$ as a rational) and rewrites via the empty-count lemma, which itself simplifies the count of the impossible event to zero. Zero over the positive denominator $N+1$ is zero in $\mathbb{Q}$.
why it matters
This lemma is one conjunct of the delta-probability headline theorem in the same module. That headline packages the native finite-layer axioms: impossible event has probability zero, certain event has probability one, every event lands in $[0,1]$, probability is monotone under implication of events, and disjoint events add. The headline is the citation point for grounding Recognition Science probability in finite distinction counting rather than continuum measure primitives. It supplies the discrete precursor layer beneath later continuum and quantum probability constructions in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.