delta_probability_headline
plain-language theorem explainer
At the native finite layer, probability is rational counting over Fin(N+1): the empty event has mass 0, the full event has mass 1, every event lands in [0,1], inclusion is monotone, and disjoint events add. Anyone building Delta-native measure or strong-closure certificates cites this as the Kolmogorov-style headline. The proof is a five-field term packing the already-proved component lemmas.
Claim. For every $N\in\mathbb{N}$, writing $\mathrm{prob}_N(E)=|\{i\in\mathrm{Fin}(N+1):E(i)\}|/(N+1)$ on events $E:\mathrm{Fin}(N+1)\to\mathrm{Prop}$: $\mathrm{prob}_N(\bot)=0$, $\mathrm{prob}_N(\top)=1$, every event satisfies $0\le\mathrm{prob}_N(E)\le 1$, $E\subseteq F$ implies $\mathrm{prob}_N(E)\le\mathrm{prob}_N(F)$, and pairwise disjoint events satisfy $\mathrm{prob}_N(E\lor F)=\mathrm{prob}_N(E)+\mathrm{prob}_N(F)$.
background
In PrimitiveRecognitionCalculus.DeltaProbability, an event on the nonempty finite index set Fin(N+1) is a predicate Event N := Fin(N+1) → Prop. The counting measure count E is the number of points satisfying E, and the uniform finite probability is the rational ratio prob E = (count E : ℚ)/(N+1).
This is the Delta-native layer: probability before any continuum limit, built only from finite distinction alternatives. The module already proves the elementary facts: empty event has count zero (hence prob 0), the universe has count N+1 (hence prob 1), nonnegativity and the upper bound ≤1, monotonicity under pointwise implication, and additivity when two events are pointwise disjoint.
Those component theorems (prob_empty, prob_univ, prob_nonneg, prob_le_one, prob_mono, prob_disjoint_or) are the upstream surface this headline packages. The Cosmology Event/edge imports appear only as ambient graph vocabulary; the probability object itself is purely the Fin(N+1) counting ratio.
proof idea
Term-mode five-conjunct packing. The proof is the tuple ⟨prob_empty N, prob_univ N, fun E ↦ ⟨prob_nonneg E, prob_le_one E⟩, fun _ _ h ↦ prob_mono h, fun _ _ h ↦ prob_disjoint_or h⟩. Each conjunct is discharged by the corresponding already-proved lemma: empty and universe normalizations, the [0,1] bounds paired per event, monotonicity under implication, and disjoint-or additivity. No new arithmetic is done here.
why it matters
This is the Kolmogorov-style headline for Delta-native probability: impossible = 0, certain = 1, values in [0,1], monotone, finitely additive on disjoint events. Downstream, strongClosureCertificate in DeltaNativeStrongClosure assembles the closed Delta-native theorem surface and consumes this headline as part of that certificate.
In the Recognition framework it anchors the finite-layer measure before continuum or analytic protocols attach. It does not itself invoke the forcing chain (T5–T8), RCL, or the phi-ladder; it supplies the discrete probability substrate those later layers sit on. Closing this surface lets the strong-closure certificate claim a fully proved finite-probability core rather than a scattered lemma list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.