expectation_const
plain-language theorem explainer
The finite rational expectation of a constant observable equals that constant on any finite distinction space. Anyone building delta-native averages or checking that the counting measure is a probability would cite this. The proof is a short tactic reduction: sum of constants, divide by cardinality, cancel the nonzero denominator.
Claim. For every natural number $N$ and every rational $c$, if $X$ is the constant function with value $c$ on the finite distinction space of cardinality $N+1$, then the finite rational expectation of $X$ equals $c$.
background
In the delta-native probability layer, an event space is the finite type $\mathrm{Fin}(N+1)$ of distinction alternatives. Probability is rational counting: the measure of a set is its cardinality over $N+1$. The companion observable average is the finite rational expectation
$$\mathbb{E}[X] := \frac{1}{N+1}\sum_{i\in\mathrm{Fin}(N+1)} X(i)\in\mathbb{Q}.$$
The module headline is that this counting measure is a genuine probability on the native finite layer: empty event has measure zero, the universe has measure one, and every event lands in $[0,1]$. Expectation is the linear dual of that counting measure. The constant-function identity is the first algebraic sanity check that the average is normalized and translation-invariant under constant shifts.
proof idea
Unfold the definition of expectation. The sum of the constant function $c$ over $\mathrm{Finset.univ}$ is $(N+1)\cdot c$ by the standard constant-sum lemma. The denominator $N+1$ is nonzero as a rational (positivity). Cancel via field simplification to obtain $c$. No induction and no case split on $N$ are required.
why it matters
This is a foundation lemma inside Primitive Recognition Calculus: it certifies that the delta-native expectation is a normalized mean, not an unscaled sum. Downstream probability and ledger constructions that treat observables as rational functions on finite distinction spaces rely on this identity when they pull constants out of averages. In the broader Recognition framework it sits under the finite-layer probability story that precedes continuous or Born-rule measures; it does not itself invoke the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder, but it keeps the discrete counting layer algebraically clean so those later bridges can attach without renormalization hacks. No downstream theorems currently list it as a direct dependency in the graph, so its role is infrastructural rather than headline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.