prob_le_one
plain-language theorem explainer
Finite distinction events on a space of N+1 points have uniform counting probability at most one. Anyone assembling the delta-native probability axioms or the normalization certificate cites this bound. The argument is a short card comparison: the filtered set cannot exceed the universe, so the rational ratio is ≤ 1.
Claim. For every natural number $N$ and every predicate $E$ on the finite index set with $N+1$ points, the uniform counting probability $\mathrm{prob}(E) := |\{i : E(i)\}|/(N+1)$ (as a rational) satisfies $\mathrm{prob}(E) \le 1$.
background
In the primitive recognition calculus, a finite distinction event on parameter $N$ is a predicate on the nonempty discrete space $\mathrm{Fin}(N+1)$. Its count is the cardinality of the filtered universe of points where the predicate holds. Probability is the rational ratio of that count to $N+1$: uniform counting measure on a finite alternative set.
This sits at the native finite layer of Recognition Science, before continuum or cost-weighted constructions. The same module already records nonnegativity, empty-event zero, and certain-event one; the present bound closes the unit interval from above.
Upstream, count is exactly the filtered Finset card, and prob is that card cast to $\mathbb{Q}$ and divided by $N+1$. No continuum measure theory is involved.
proof idea
Classical mode, then unfold prob and count. Apply Finset.card_filter_le to get that the filtered universe has card at most the full universe card. Rewrite the universe card as $N+1$. Positivity gives $0 < (N+1:\mathbb{Q})$. Cast the natural inequality to rationals, rewrite the goal via div_le_iff₀ on the positive denominator, and finish by simp against the cast inequality.
why it matters
Feeds the delta-probability headline, which packages impossible-event zero, certain-event one, the unit interval $[0,1]$, monotonicity under inclusion, and additivity on disjoint events as the native finite-layer probability package. Also consumed by ProbabilityNormalizationCert in the verification layer, which certifies that recognition-weighted probabilities stay normalized.
In the Recognition framework this is bookkeeping, not a deep forcing step: it ensures the discrete counting measure on distinction alternatives is a genuine probability before one lifts to cost-weighted or continuum constructions. It does not touch T5–T8, the RCL, or the phi ladder; it only keeps the finite probability layer honest so later certificates can quote a clean $[0,1]$ bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.