prob_disjoint_or
plain-language theorem explainer
Disjoint events on a finite distinction space have additive uniform probability: P(E ∨ F) = P(E) + P(F) when E and F never hold together. Anyone building the delta-native probability layer cites this for finite additivity. The proof unfolds the counting ratio, applies the corresponding count identity, and cancels the common denominator.
Claim. Let $N\in\mathbb{N}$ and let $E,F:\mathrm{Fin}(N+1)\to\mathrm{Prop}$ be finite distinction events. If for every index $i$ one has $\neg(E(i)\land F(i))$, then the uniform rational probability satisfies $P(E\lor F)=P(E)+P(F)$, where $P(G)=\#\{i:G(i)\}/(N+1)$.
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 count of an event is the number of indices where the predicate holds; the uniform probability is that count divided by $N+1$, valued in $\mathbb{Q}$.
This module develops the elementary measure facts needed before any continuum limit: empty event has probability zero, the universe has probability one, monotonicity, and nonnegativity in $[0,1]$. The companion lemma states that disjoint events have additive counts: if $E$ and $F$ never hold jointly, then $\mathrm{count}(E\lor F)=\mathrm{count}(E)+\mathrm{count}(F)$.
The present statement lifts that integer identity to the rational counting measure by dividing by the fixed denominator $N+1$.
proof idea
Term-mode proof in four steps. Unfold prob to expose the ratio of counts over $N+1$. Rewrite the numerator via count_disjoint_or applied to the disjointness hypothesis, obtaining $\mathrm{count}(E\lor F)=\mathrm{count}(E)+\mathrm{count}(F)$. Cast the natural-number sum to rationals with Nat.cast_add, then finish by ring on the common denominator.
why it matters
Finite additivity is the last structural clause in the delta-probability headline theorem of this module, which packages the native finite layer: impossible event zero, certain event one, probabilities in $[0,1]$, monotonicity, and disjoint additivity. That headline is the Recognition-native stand-in for Kolmogorov axioms before any continuum or measure-theoretic extension.
In the broader foundation, probability is not postulated as a real-valued measure on an abstract $\sigma$-algebra; it is rational counting over finite distinction alternatives. This lemma closes the additive half of that story at the discrete layer that feeds later continuum and physics constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.