Indeed, and "summation" is not the same as "addition".

Unfortunately, the syntax chosen for representing the sequence is that of an additive series, where a binary + operator is interposed between terms.

The semantics being shown does not seem to follow from a redefinition of that operator per se as stand-alone binary operator.

You really want to show this as, say

  fun([1 2 3 4 ... ])  

a function applied to a vector. Why the algebraic rules seem to work is because fun is a linear operator; i.e.

  n fun([x0 x1 ... ]) = fun([nx0 nx1 ...])

and

  fun(v0 + v1) = fun(v0) + fun(v1)

We can ply these rules back to the original 1 + 2 + 3 ... notation and then they look like algebra.

Basically, none of this means that the natural numbers add to -1/12; only that the sequence of natural numbers can be fed into some decimating calculation which ends up with -1/12.

Well, no kidding; the sequence of natural numbers can be fed into a decimating calculation which converges on any value you want, if you can freely choose the decimating calculation, and that calculation can be chosen to be linear operator.

Note that we don't have:

   fun([x0 x1 x3 ... x42 ...]) = fun([x3 x42 x0 ... x1 ...])

which would be required to hold if this were addition. We can't change the positions of the terms. Why? Because they correspond to different powers in a power series.