2.4. Aggregation (R9)🔗

R9 — Extensive quantities aggregate additively over parts; intensive ones do not. For an extensive kind the value over a whole is the sum of the values over its disjoint parts — the mass of an assembly is the sum of its parts' masses. Where this fails it must not be assumed: volume on mixing is sub-additive (ethanol and water), and that negation is stated to keep the extensive predicate honest. Tracking which kinds are extensive is the precondition for soundly summing measurements.

Beside the sum and the shared constant sits a third mode that is neither: the weighted mean. It is the first aggregation that divides, so it is the first that carries a side condition — the total weight is not zero — and the first whose law does not survive the descent to an executable carrier. The mode is carried at any Carrier, its law is proved where cancellation is available, and its rung at genuine binary32 is a bound rather than an equation. Those three sentences are one structure read at three carriers, not three structures.