prob_nonneg
plain-language theorem explainer
Uniform counting probabilities of finite distinction events on Fin(N+1) are nonnegative rationals. Anyone assembling the delta-native probability layer or a normalization certificate cites this bound. The proof unfolds the counting ratio and discharges nonnegativity by the positivity tactic.
Claim. For every natural number $N$ and every finite distinction event $E$ on the nonempty space $\mathrm{Fin}(N+1)$, the uniform counting probability $P(E)=|\{i:E(i)\}|/(N+1)$ (as a rational) satisfies $0\le P(E)$.
background
In the primitive recognition calculus, a finite distinction event on parameter $N$ is a predicate on the nonempty finite index set $\mathrm{Fin}(N+1)$. The associated probability is the uniform counting ratio: the number of indices satisfying the predicate, cast to $\mathbb{Q}$, divided by $N+1$.
This sits at the native finite layer before continuum or measure-theoretic probability. The same nonnegativity pattern appears for quantum-state Born weights and Boltzmann factors elsewhere in the monolith, but here the object is purely combinatorial: a rational card ratio on a finite alternative set.
Upstream, the probability definition is exactly that ratio; the count is the cardinality of the satisfying set. No cost functional or ledger weight enters at this stage.
proof idea
Tactic proof. After classical, unfold the probability definition to the ratio $(\mathrm{count},E:\mathbb{Q})/(N+1:\mathbb{Q})$. The positivity tactic closes the goal: the numerator is a natural cast (hence nonnegative) and the denominator $N+1$ is a positive natural cast, so the quotient is nonnegative in $\mathbb{Q}$.
why it matters
Feeds the delta-probability headline, which packages impossible-event zero, certain-event one, the closed interval $[0,1]$ for every event, and monotonicity under implication. That headline is the finite-layer statement that probability is rational counting over distinction alternatives.
Also referenced by the probability-normalization certificate path and by parallel nonnegativity lemmas in the quantum ledger and Boltzmann distribution modules, keeping the same axiomatic shape across layers. In Recognition Science terms this is bookkeeping at the discrete alternative layer, not yet the J-cost or eight-tick structure; it ensures the counting measure used before continuum limits is a genuine probability weight.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.