Event
plain-language theorem explainer
A finite distinction event is a predicate on the nonempty discrete space with N+1 points. It is the basic measurable set for the primitive recognition calculus probability layer (counts, finsets, and normalized probabilities on Fin(N+1)). Anyone building discrete recognition measures or delta-probability lemmas cites this type. The body is a one-line type abbreviation.
Claim. For each natural number $N$, a finite distinction event on the nonempty finite space with $N+1$ points is a predicate $E : \{0,\ldots,N\} \to \mathrm{Prop}$.
background
The module develops a discrete probability calculus for primitive recognition: events live on a nonempty finite carrier Fin (N+1), so there is always at least one point. An event is simply which of those points are distinguished (satisfy the predicate).
Sibling definitions turn events into combinatorial data: the count of satisfying points, the corresponding finset, and the normalized probability (count over N+1). Nonnegativity, the empty and universe cases, and monotonicity of counts sit next to this abbreviation.
The name collides with the cosmology Event structure (directed source/target postings with a positive ratio). Here the meaning is purely the finite-space predicate used by delta-probability, not a rung-coarsening posting.
proof idea
No proof. The declaration is a type abbreviation: Event N is definitionally equal to the function type from Fin (N+1) into Prop. Downstream lemmas unfold or treat it as an ordinary predicate on a finite index set.
why it matters
This is the carrier type for the Foundation primitive-recognition probability layer. Every count, finset extraction, and probability bound in the module is typed over it, so the discrete measure theory of distinction events has a single, parameterised event sort.
In the broader Recognition stack, finite distinction events feed the bookkeeping that later modules coarsen or trigger on (active blocks, demand, lossless descent). The local role is narrower: fix the nonempty finite sample space so that normalized probabilities and empty/universe identities are well-defined before any continuum or rung structure appears.
It does not itself invoke J-cost, the forcing chain, or the eight-tick octave; it only supplies the discrete event type those layers can instantiate when they need finite sample spaces.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.