Finite probability pushforward ($p_f(y)={\sum }_{x:f(x)=y}p(x)$)

Map a finite probability distribution through a function by summing the masses of source atoms with the same image. The image of the finite support is finite, and fibres partition the original support, so summing the output masses gives the original total one. Non-injective images require addition, not overwriting. A computational snapshot can evaluate each source image once and answer later mass queries by summing matching entries.