prob_univ
plain-language theorem explainer
Under the uniform finite counting measure on N+1 distinction slots, the certain event has probability one. Anyone assembling the delta-native probability axioms cites this as the unit-normalization half of the headline. The proof rewrites through the counting definition and divides N+1 by itself after a rational cast.
Claim. For every natural number $N$, if $\mathrm{prob}_N$ is the uniform rational counting measure on the $N+1$ indices $\{0,\ldots,N\}$, then $\mathrm{prob}_N(\{i : \top\}) = 1$.
background
In the primitive recognition calculus, an event on parameter $N$ is a predicate on the finite index set ${0,\ldots,N}$. The count of an event is the number of indices that satisfy it; the certain event (the constantly-true predicate) therefore has count $N+1$, by count_univ.
Probability is the uniform rational ratio $\mathrm{prob}(E) = (\mathrm{count}, E)/(N+1)$. This is the native finite layer before any continuum or Gibbs construction: pure counting of distinction alternatives, not a measure-theoretic pushforward.
The module packages the elementary calculus of these ratios (empty event, certain event, nonnegativity, unit bound, monotonicity) so later recognition statements can quote a single headline rather than rebuild the arithmetic each time.
proof idea
Tactic proof. Mark the context classical, then record $N+1 \neq 0$ in $\mathbb{Q}$ by positivity. Rewrite the goal with the definition of prob and with count_univ, which supplies $\mathrm{count}(\top) = N+1$. Align the natural and rational casts of $N+1$ by norm_num, and finish with div_self on the nonzero denominator.
why it matters
This is the unit half of the delta-native probability headline. Downstream, delta_probability_headline conjoins it with the empty-event zero, the $[0,1]$ bounds, monotonicity, and additivity on disjoint events, stating that probability at the native finite layer is rational counting over finite distinction alternatives.
In the Recognition Science stack this sits below continuum or thermodynamic constructions: it certifies that the discrete distinction layer already carries a normalized probability calculus. It does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the $\varphi$-ladder; it only supplies the elementary normalization those later layers may quote when they specialize to finite alternative sets.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.