Can we express $\lfloor\frac{a+b}M\rfloor$ and $\lceil\frac{a+b}M\rceil$ in simpler terms? Eg in terms of $\lfloor\frac aM\rfloor, a\bmod M, \lfloor\frac bM\rfloor, b\bmod M$, and possibly other simpler terms?
I posted a solution, but I feel that my proof of my solution is long and tedious. Was wondering if someone might have a better/simpler solution/proof or suggestions on how to make my solution/proof simpler.
(If there's a simpler derivation, let me know.)
Let integer division $//$ be defined as floor division, i.e., $x//M := \big\lfloor x/M \big\rfloor$ where $/$ is regular division.
A summary of $^{1,2}$ for floor division says that for dividend $x \in \mathbb R$ and divisor $M \in \mathbb R_{\neq 0}$, if we define the quotient as $q(x) := x//M = \big\lfloor x/M \big\rfloor$, the remainder as $r(x) := x - q(x)M$, and the Modulo operation as $x \bmod M := r(x)$, then these values of $q(x)$ and $r(x)$ satisfy
$$x = q(x)M + r(x)$$
$$ \begin{cases} \text{if } M > 0 &\text{then } 0 \leq r(x) < M\\ \text{if } M < 0 &\text{then } M < r(x) \leq 0 \end{cases} \qquad \equiv \qquad \begin{aligned} &0 \leq \lvert r(x) \rvert < \lvert M \rvert\\ &\text{and } \big(r(x) {=} 0 \text{ xor } \operatorname{sgn}(r(x)) {=} \operatorname{sgn}(M)\big) \end{aligned} $$
That is, the remainder $r(x)$ is either $0$ or has the same sign as the divisor $M$ (both are positive or both are negative).
Derivations of $\big\lfloor \frac{a + b}{M} \big\rfloor = q + q' + \big[\!\!\big[\ \lvert r + r' \rvert \geq \lvert M \rvert\ \big]\!\!\big]$ and $\big\lceil \frac{a + b}{M} \big\rceil = q + q' + \big[\!\!\big[\ \lvert r + r' \rvert > 0 \big]\!\!\big] + \big[\!\!\big[\ \lvert r + r' \rvert > \lvert M \rvert\ \big]\!\!\big]$
Let $a, b, M \in \mathbb R$ be real numbers, with $M \neq 0$, and define
$$ \begin{aligned} q &:= q(a) = \big\lfloor a/M \big\rfloor &r &:= a \bmod M = r(a) = a - qM\\ q' &:= q(b) = \big\lfloor b/M \big\rfloor &r' &:= b \bmod M = r(b) = b - q'M \end{aligned} $$
By $^{1,2}$, these values satisfy
$$ \begin{cases} \text{if } M > 0 &\text{then } 0 \leq r, r' < M\\ \text{if } M < 0 &\text{then } M < r, r' \leq 0 \end{cases} \qquad \equiv \qquad \begin{aligned} &0 \leq \vert r^* \rvert < \lvert M \rvert\\ &\text{and } \big(r^* {=} 0 \text{ xor } \operatorname{sgn}(r^*) {=} \operatorname{sgn}(M)\big)\\ &\text{for } r^* \in \{r, r'\} \end{aligned} $$
Proof of $\big\lfloor \frac{a + b}{M} \big\rfloor = q + q' + \big[\!\!\big[\ \lvert r + r' \rvert \geq \lvert M \rvert\ \big]\!\!\big] \qquad \text{See}\ ^3$
We have
$$ \begin{aligned} \Big\lfloor \frac{a + b}{M} \Big\rfloor &=\Big\lfloor \frac{qM + r + b}{M} \Big\rfloor\\ &= \Big\lfloor q + \frac{r + b}{M} \Big\rfloor\\ &= q + \Big\lfloor \frac{r + b}{M} \Big\rfloor &&(*1)\\ &= \Big\lfloor \frac{a}{M} \Big\rfloor + \Big\lfloor \frac{(a \bmod M) + b}{M} \Big\rfloor &&(*2) \end{aligned} $$
Let $a^* := b$ and $b^* = r$. We have
$$ \begin{aligned} \Big\lfloor \frac{r + b}{M} \Big\rfloor &= \Big\lfloor \frac{a^* + b^*}{M} \Big\rfloor\\ &= \Big\lfloor \frac{a^*}{M} \Big\rfloor + \Big\lfloor \frac{(a^* \bmod M) + b^*}{M} \Big\rfloor &&(2)\\ &= \Big\lfloor \frac{b}{M} \Big\rfloor + \Big\lfloor \frac{(b \bmod M) + r}{M} \Big\rfloor\\ &= q' + \Big\lfloor \frac{r' + r}{M} \Big\rfloor &&(*3) \end{aligned} $$
Now
$$ \begin{aligned} &\begin{cases} \text{if } M > 0 &\text{ then } 0 \leq r, r' < M \iff 0 \leq r + r' < 2M\\ \text{if } M < 0 &\text{ then } M < r, r' \leq 0 \iff 2M < r + r' \leq 0 \end{cases}\\ \\ &\begin{aligned} &\equiv &&0 \leq \lvert r + r' \rvert < \lvert 2M \rvert\\ &&&\text{and } \big(r {+} r' {=} 0 \text{ xor } \operatorname{sgn}(r {+} r') {=} \operatorname{sgn}(S))\\ \\ &\equiv &&0 \leq \frac{r + r'}{M} < 2 \end{aligned} \end{aligned} $$
The ratio $\frac{r + r'}{M}$ is nonnegative because either $r {+} r' {=} 0$, in which case, the ratio is $0$, or $r {+} r'$ and $M$ have the same sign, in which case the ratio is positive.
We have
$$ \begin{aligned} \Big\lfloor \frac{r + r'}{M} \Big\rfloor &= \begin{cases} 0 &\text{if } \frac{r + r'}{M} < 1\\ 1 &\text{if } \frac{r + r'}{M} \geq 1 \end{cases}\\ &= \Big[\!\!\Big[ \frac{r + r'}{M} \geq 1 \Big]\!\!\Big]\\ &= \Bigg[\!\!\Bigg[ \begin{cases} r + r' \geq M &\text{if } M > 0\\ r + r' \leq M &\text{if } M < 0 \end{cases} \Bigg]\!\!\Bigg]\\ &= \Big[\!\!\Big[\ \lvert r + r' \rvert \geq \lvert M \rvert\ \Big]\!\!\Big] &&(*4) \end{aligned} $$
Back to $(1)$
$$ \begin{aligned} \Big\lfloor \frac{a + b}{M} \Big\rfloor &= q + \Big\lfloor \frac{r + b}{M} \Big\rfloor &&(1)\\ &= q + q' + \Big\lfloor \frac{r' + r}{M} \Big\rfloor &&(3)\\ &= q + q' + \Big[\!\!\Big[\ \lvert r + r' \rvert \geq \lvert M \rvert\ \Big]\!\!\Big] &&(4)(*5)\\ &= \Big\lfloor \frac{a}{M} \Big\rfloor + \Big\lfloor \frac{b}{M} \Big\rfloor + \Big[\!\!\Big[\ \big\lvert (a \bmod M) + (b \bmod M) \big\rvert \geq \lvert M \rvert\ \Big]\!\!\Big] &&(*6) \end{aligned} $$
Proof of $\big\lceil \frac{a + b}{M} \big\rceil = q + q' + \big[\!\!\big[\ \lvert r + r' \rvert > 0 \big]\!\!\big] + \big[\!\!\big[\ \lvert r + r' \rvert > \lvert M \rvert\ \big]\!\!\big] \qquad \text{See}\ ^3$
We use the same definitions of $a, b, M \neq 0, q, r, q', \text{ and } r'$ as before.
For $x \in \mathbb R$, we have
$$ \begin{aligned} \big\lceil x \big\rceil &= \begin{cases} \big\lfloor x \big\rfloor &x \in \mathbb Z\\ \big\lfloor x \big\rfloor + 1 &x \not \in \mathbb Z \end{cases}\\ &= \big\lfloor x \big\rfloor + \Big[\!\!\Big[ x \not \in \mathbb Z \Big]\!\!\Big]\\ &= \big\lfloor x \big\rfloor + \Big[\!\!\Big[ x \bmod 1 \neq 0 \Big]\!\!\Big] &&(*7) \end{aligned} $$
Note that
$$ \begin{aligned} (a + b) \bmod M &= (qM + r + q'M + r') \bmod M\\ &= (r + r') \bmod M &&(*8) \end{aligned} $$
which means
$$ \begin{aligned} \Big[\!\!\Big[ (a + b) \bmod M \neq 0 \Big]\!\!\Big] &= \Big[\!\!\Big[ (r + r') \bmod M \neq 0 \Big]\!\!\Big] &&(8)\\ &= \Big[\!\!\Big[ \big(r + r' \neq 0\big) \land \big(r + r' \neq M \big) \Big]\!\!\Big] &&\text{Since } &&0 \leq \lvert r + r' \rvert < \lvert 2M \rvert\\ &&&&&\text{and } \big(r {+} r' {=} 0 \text{ xor } \operatorname{sgn}(r {+} r') {=} \operatorname{sgn}(M) \big)\\ &= \Big[\!\!\Big[ r + r' \neq 0 \Big]\!\!\Big] \Big[\!\!\Big[ r + r' \neq M \Big]\!\!\Big] &&(*9) \end{aligned} $$
So
$$ \begin{aligned} \Big\lceil \frac{a + b}{M} \Big\rceil &= \Big\lfloor \frac{a + b}{M} \Big\rfloor + \Big[\!\!\Big[ \frac{a + b}{M} \not \in \mathbb Z \Big]\!\!\Big] &&(7)\\ &= \Big\lfloor \frac{a + b}{M} \Big\rfloor + \Big[\!\!\Big[ (a + b) \bmod M \neq 0 \Big]\!\!\Big]\\ &= q + q' + \Big[\!\!\Big[\ \lvert r + r' \rvert \geq \lvert M \rvert\ \Big]\!\!\Big] + \Big[\!\!\Big[ r + r' \neq 0 \Big]\!\!\Big] \Big[\!\!\Big[\ r + r' \neq M \ \Big]\!\!\Big] &&(5)(9)\\ &= \begin{cases} q + q' &\text{if } r + r' = 0\\ q + q' + 1 &\text{if } 0 < \lvert r + r' \rvert \leq \lvert M \rvert\\ q + q' + 2 &\text{if } \lvert M \rvert < \lvert r + r' \rvert < \lvert 2M \rvert\\ \end{cases}\\ &= q + q' + \Big[\!\!\Big[\ \lvert r + r' \rvert > 0\ \Big]\!\!\Big] + \Big[\!\!\Big[\ \lvert r + r' \rvert > \lvert M \rvert\ \Big]\!\!\Big] &&(*10) \end{aligned} $$
where, recall
$$ \begin{aligned} q &:= \big\lfloor \frac{a}{M} \big\rfloor &r &:= a \bmod M\\ q' &:= \big\lfloor \frac{b}{M} \big\rfloor &r' &:= b \bmod M \end{aligned} $$
Example
For example, with $a = 8, b = 12.5, M = 5$, we have $q = 1, r = 3, q' = 2, r' = 2.5$. Substituting these values into $(10)$, we have
$$ \begin{aligned} \bigg\lceil \frac{8 + 12.5}{5} \bigg\rceil &= 1 + 2 + \big[\!\!\big[ 3 + 2.5 > 0 \big]\!\!\big] + \big[\!\!\big[ 3 + 2.5 > 5 \big]\!\!\big] &&(10)\\ &= 3 + \big[\!\!\big[ 5.5 > 0 \big]\!\!\big] + \big[\!\!\big[ 5.5 > 5 \big]\!\!\big]\\ &= 3 + 1 + 1\\ &= 5 \end{aligned} $$
which is correct as $\big\lceil \frac{8 + 12.5}{5} \big\rceil = \lceil 4.1 \rceil = 5$.
$^1$: See floored division in Wikipedia's Modulo operation
$^2$: See floored division in Desmos's 5 types of integer division and their corresponding quotient, remainder, and Modulo operation
$^3$: Where $\big[\!\!\big[ condition \big]\!\!\big]$ denotes Iverson bracket notation and is defined as
$$ \Big[\!\!\Big[ condition \Big]\!\!\Big] := \begin{cases} 1 &\text{if } condition\\ 0 &\text{otherwise} \end{cases} $$