prob
plain-language theorem explainer
Uniform probability on a finite distinction space of size N+1 is the rational ratio of favorable points to total points. Anyone working at the delta-native probability layer of primitive recognition cites this definition as the base measure. The body is a one-line cast of the event count divided by N+1.
Claim. For $N \in \mathbb{N}$ and an event $E$ (a predicate on $\mathrm{Fin}(N+1)$), define $\mathrm{prob}(E) := \#\{i : E(i)\}/(N+1)$ as an element of $\mathbb{Q}$.
background
In the primitive recognition calculus, a finite distinction event on parameter $N$ is a predicate on the nonempty finite type $\mathrm{Fin}(N+1)$. The companion count returns the number of indices at which the predicate holds, obtained by filtering the universe finset and taking its cardinality.
The module builds a delta-native probability layer: probability is introduced before any continuum measure theory, as pure rational counting over finite alternatives. The denominator $N+1$ is exactly the cardinality of the underlying space, so the construction is the uniform measure on a finite set, valued in $\mathbb{Q}$ rather than $\mathbb{R}$.
Upstream, the local count is the only arithmetic input; other modules named Event or E (cosmology rung coarsening, lattice ball edges) are distinct notions and are not used in the body.
proof idea
Definition, not a proof. Cast the natural-number count of $E$ to $\mathbb{Q}$ and divide by the rational $N+1$. No lemmas are applied; noncomputable is inherited from classical finset filtering in count.
why it matters
This is the primitive probability measure for the Recognition Science finite layer. Downstream theorems establish the Kolmogorov-style headline on it: empty event has probability 0, universe has probability 1, every event lies in $[0,1]$, monotonicity under inclusion, and additivity for disjoint events (prob_empty, prob_univ, prob_nonneg, prob_le_one, prob_mono, prob_disjoint_or). Those facts are packaged as delta_probability_headline.
The definition also feeds ValidComparisonExamples.probabilityDisplayBridge, linking the counting ratio to display-level comparison. In the broader framework it supplies the finite, rational substrate on which later continuum or phi-ladder probability statements can be grounded, without assuming real analysis at the base.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.