expectation
plain-language theorem explainer
Uniform discrete expectation of a rational observable on a finite distinction space of cardinality N+1. Anyone working the primitive recognition calculus or classical-emergence bridges cites it as the mean under counting measure. The body is the plain average: total sum divided by N+1.
Claim. For $N \in \mathbb{N}$ and a rational-valued observable $X$ on the finite index set $\{0,\ldots,N\}$, the expectation is $\mathbb{E}[X] := \frac{1}{N+1}\sum_{i=0}^{N} X(i) \in \mathbb{Q}$.
background
The module builds a finite, fully rational probability calculus on distinction spaces. An event is a boolean predicate on Fin (N+1); count and prob are the corresponding cardinality and normalized frequency. Observables here are maps Fin (N+1) → ℚ, so every mean stays inside the rationals and needs no measure-theoretic completion.
Expectation is the companion mean: the same uniform weight $1/(N+1)$ that turns counts into probabilities, applied to a rational function instead of an indicator. The construction is noncomputable only because division in ℚ is marked that way in the library; the formula itself is elementary.
No external lemmas are required. Sibling facts (prob_empty, prob_univ, prob_nonneg, additivity on disjoint events) fix the probability side; this definition supplies the matching first-moment operator.
proof idea
Pure definition: cast the Finset sum of X over the universe to ℚ and divide by N+1. No tactics, no lemmas.
why it matters
Gives the first-moment primitive for the recognition calculus. Immediately yields expectation_const (constant observables return themselves). Downstream classical-emergence material cites the same mean when stating Ehrenfest-type claims (quantum expectations track classical equations) and the J-cost route to Newton’s law. Parallel uses appear in the Higgs-potential and hypersurface-deformation developments wherever a discrete average of a rational field is needed. Inside the forcing chain it stays foundational bookkeeping rather than a T5–T8 step, but every later mean-value identity in the monolith rests on this uniform average.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.