The variance of a sum of m identically-distributed uncorrelated trials is m*q(1-q), and it is at the rationals because the record has no mulComm

Recorded description

Let X be a family of rational-valued random variables on a finite index range [0, n) with a distribution p, let m be a natural number and q a rational. If the family is pairwise uncorrelated below m and every trial below m has variance q(1-q), then the pointwise sum of the first m trials has variance m*q(1-q). Both extra hypotheses are exactly the ones Rat.variance_sumVars carries and no more. The proof is the same two steps as the mean, over Rat.variance_sumVars instead of Rat.expectation_sumVars. The statement lives at the rationals rather than over AlgS.OrderedRing for a MEASURED reason: the generic variance is the centred form and the generic covariance the computational one, and relating them needs E[fun k => X k * c] ~ E[X]*c, which pulls a constant past the weight p k and therefore needs mulComm -- a field ADR-1592 deliberately withheld. So the generic shelf has no variance_eq, hence no variance_add_of_uncorrelated, hence no variance of a sum. That is a fact about the RECORD, not about the mathematics: the moment AlgS.CommOrderedRing exists this theorem moves up verbatim.