count_mono
plain-language theorem explainer
Pointwise inclusion of finite distinction events on Fin(N+1) implies the support count of the smaller event is at most that of the larger. Discrete-probability constructions in the primitive recognition calculus cite this for monotone counting before normalizing. The argument is a direct Finset cardinality comparison after unfolding the filter definition of count.
Claim. For any $N\in\mathbb{N}$ and events $E,F:\mathrm{Fin}(N+1)\to\mathrm{Prop}$, if $E(i)$ implies $F(i)$ for every index $i$, then the number of points at which $E$ holds is at most the number at which $F$ holds.
background
In PrimitiveRecognitionCalculus.DeltaProbability an event on parameter $N$ is a predicate on the nonempty finite index set $\mathrm{Fin}(N+1)$. Its count is the cardinality of the classical filter of the universe by that predicate: how many discrete points satisfy the distinction.
The module equips these events with the uniform discrete probability $\mathrm{prob}(E)=\mathrm{count}(E)/(N+1)$. Related modules (RungCoarsen, lattice edge sets) use analogous event/count language, but here the event is purely a Prop-valued function on a finite type, with no ratio or adjacency data attached.
Monotonicity of count under pointwise implication is the elementary lattice fact needed before any comparison of normalized probabilities.
proof idea
Unfold count to $(\mathrm{Finset.univ.filter},E).\mathrm{card}$. Apply $\mathrm{Finset.card_le_card}$, reducing the claim to subset inclusion of the two filtered finsets. Membership in a filter is equivalent (after simp) to the predicate holding at that index; the hypothesis $E\Rightarrow F$ therefore sends members of $E$'s filter into $F$'s filter. Classical is opened so that Prop is decidable inside the filter.
why it matters
The sole downstream consumer in-module is prob_mono: once counts are monotone, dividing by the strictly positive rational $N+1$ yields $\mathrm{prob},E\le\mathrm{prob},F$ under the same pointwise inclusion. That is the basic order property of the discrete recognition measure before any ledger, Born-rule, or amplitude comparison.
The result is foundational bookkeeping inside the probability layer, not a step of the T0–T8 forcing chain, the Recognition Composition Law, or the phi-ladder mass formula. It closes the count half of the empty/univ/mono suite that makes the finite event algebra usable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.