count_disjoint_or
plain-language theorem explainer
Disjoint events on a finite index set Fin(N+1) have additive point-counts: the count of their pointwise disjunction equals the sum of the counts. Anyone building finite probability on distinction events cites this before lifting to probabilities. The proof identifies counts with Finset cardinalities, shows the selected sets are disjoint, and applies the standard union-cardinality lemma.
Claim. Let $N\in\mathbb{N}$ and let $E,F:\mathrm{Fin}(N+1)\to\mathrm{Prop}$ be finite distinction events. If $E$ and $F$ are pointwise disjoint (for every index $i$, not both $E(i)$ and $F(i)$ hold), then $\mathrm{count}(E\lor F)=\mathrm{count}(E)+\mathrm{count}(F)$.
background
In the primitive recognition calculus, an Event on parameter $N$ is a predicate on the nonempty finite space $\mathrm{Fin}(N+1)$: a finite distinction pattern. The count of an event is the number of indices where the predicate holds, realized as the cardinality of the filtered universe Finset (eventFinset).
The module develops a finite probability calculus on these events: probability is count normalized by $N+1$. Additivity of count for disjoint events is the combinatorial step that makes probability additive. The local lemma count_eq_card records that count is definitionally the card of eventFinset, so Finset algebra applies directly.
Upstream, the same count/event vocabulary appears in cosmology coarsening (multiset event counts) and lattice edge sets, but here the objects are purely finite Boolean events on Fin(N+1), not geometric edges or ratio-carrying postings.
proof idea
Work classically. First prove that the eventFinset of the pointwise disjunction equals the union of the two eventFinsets (extensionality plus simp on the filter membership). Next show those two Finsets are Disjoint: from membership of both, unpack eventFinset and apply the hypothesis that no index satisfies both predicates. Rewrite all three counts via count_eq_card, substitute the union identity, and finish with Finset.card_union_of_disjoint.
why it matters
This is the counting engine under prob_disjoint_or, which states that disjoint finite events have additive probability (normalize by $N+1$ and cast the Nat sum). Without count additivity, the finite probability layer on distinction events cannot support mutually exclusive alternatives.
In Recognition Science, primitive recognition calculus sits under the foundation forcing chain: finite distinction events and their measures feed the ledger and delta-probability structure used when recognition content is coarse-grained. The result is elementary measure theory on a finite sample space, not a T5–T8 forcing step, but it is required scaffolding for any probabilistic reading of exclusive recognition outcomes (e.g. alternative postings that cannot co-occur on the same tick index).
Downstream only prob_disjoint_or is recorded as a direct user; that theorem is the citation surface for probability-level arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.