2.3 Summed carry-count identity
For prime \(p\), \(k \leq n\), and \(b {\gt} \texttt{trunc\_ log}(p, n)\),
\[ \sum _{i=1}^{b} \left\lfloor \frac{n}{p^i} \right\rfloor = \sum _{i=1}^{b} \left\lfloor \frac{k}{p^i} \right\rfloor + \sum _{i=1}^{b} \left\lfloor \frac{n-k}{p^i} \right\rfloor + \sum _{i=1}^{b} \mathrm{carry}(p, i, k, n-k). \]
Proof. Apply Lemma 2.7 pointwise for each \(i \in \{ 1, \ldots , b\} \) and use linearity of summation.