prob_mono
plain-language theorem explainer
Pointwise inclusion of finite distinction events yields monotonicity of their rational probabilities. Anyone assembling the delta-native probability headline cites this. The proof unfolds the counting measure, lifts count monotonicity to rationals, and divides by the fixed positive denominator N+1.
Claim. Let $N\in\mathbb{N}$ and let $E,F:\mathrm{Fin}(N+1)\to\mathrm{Prop}$ be finite distinction events. If $E(i)$ implies $F(i)$ for every $i$, then $\mathrm{prob}(E)\le\mathrm{prob}(F)$, where probability is the rational ratio of the event count to $N+1$.
background
In this module, a finite distinction event on parameter $N$ is a predicate on the nonempty finite index set $\mathrm{Fin}(N+1)$. The count of an event is the cardinality of the filtered universe of indices where the predicate holds. Probability is that count divided by $N+1$, as a rational: pure finite counting measure on distinction alternatives.
The immediate upstream fact is count monotonicity: if $E$ implies $F$ pointwise, then $\mathrm{count}(E)\le\mathrm{count}(F)$, proved by Finset card comparison on the filtered universes. The present statement lifts that inequality through the common positive denominator.
Local setting is the primitive recognition calculus layer that treats probability as rational counting before any continuum or measure-theoretic extension.
proof idea
Unfold the definition of probability to a ratio of counts over $N+1$. Positivity gives $0<(N+1:\mathbb{Q})$. Apply count monotonicity under the inclusion hypothesis and cast the natural inequality to rationals. Finish with the standard lemma that divides both sides of a nonnegative inequality by a positive right-hand factor, preserving the order.
why it matters
Feeds the delta-native probability headline in the same module, which packages impossible event zero, certain event one, the unit interval bounds, monotonicity under inclusion, and additivity for disjoint events. That headline is the finite-layer claim that probability at the recognition base is rational counting over distinction alternatives, not an imported Kolmogorov axiom set.
In the Recognition framework this sits under Foundation: before mass ladders, eight-tick structure, or continuum limits, one needs a clean monotone counting probability on finite events. Monotonicity is the order-theoretic half of that package; without it the headline conjunction fails.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.