Update: The answer shows that some tweaking is necessary to get this to work. The problem are those $f$ where there exist an $N$ such that $f(n)$ is always odd for $n \ge N$. But this can be remedied in a simple way -condition $\text{(2)}$ below is dropped and we just handle these 'overloaded' functions by equating them to 'there equal'.
If $f$ is overloaded there is a least $k$ (that might be $0$ with $f(0)$ also odd) so that $f(m)$ is odd for all $m \gt k$. We define a function $g$ that agrees with $f$ for $n \lt k$, has $g(k)=f(k)+1$ and for $m \ge k$, we recursively define $g(m + 1) = 2 * g(m)$. This function $g(x)$ is not overloaded.
Then, considering these two functions as equivalent the problem goes away.
So, we can define a binary operation that is obviously commutative. Interestingly, when adding numbers, if one is overloaded we can't use that representation in the definition of the binary operation - you must use that other representation in the two element block of the (really fine-grained) partition. So the necessity of condition $\text{(2)}$ below 'melts away;.
But showing that the operation is associative is not immediate. I think we can do this by using the fact that the binary operation is 'continuous'; c.f.
Prove Addition is Continuous (without epsilon-delta!)
When I work out the details I will post them in a another proof-checking question.
Incidentally, the purpose of this is to create a model of the positive real numbers under addition. Intuitively, you can think of the function $f$ as representing a canonical Cauchy sequences; for every $x$ there is one and only one $f$ with
$\quad x = \lim\limits_{n \to +∞} f(n) \, 2^{-n}$
But note that this is quite different - the real numbers with $+$ are being directly constructed ab initio; it is not necessary to define or use the rational numbers as an intermediate step. A computer running an artificial intelligence program might be able to 'understand' this construction easier than the usual methods.
Here $0 \in \mathbb N$.
Definition: A function $f: \mathbb N \to \mathbb N$ is called a Eudoxus magnitude if it satisfies the following:
$\tag 1 \forall n \; f(n+1) = 2f(n) \text{ or } f(n+1) = 2f(n) + 1$
$\tag 2 \forall\, m \; \exists \, n \ge m \; \text{ such that } f(n+1) = 2f(n)$
One interesting thing about a Eudoxus magnitude $f$ is that if we know the value of $f$ at $n$, then the value at all smaller numbers is determined:
$\tag 3 f(n-1) = \text{the quotient (Euclidean division) of dividend } f(n) \text{ by divisor } 2$.
Also, given any number $k$, we can create a Eudoxus magnitude with $f(n) = k$ using $\text{(3)}$.
I've come up with a way of adding two Eudoxus magnitudes (not pointwise addition) $f$ and $g$ as follows.
For any integer $n \ge 0$ such that $f(n+1) = 2f(n)$ or $g(n+1) = 2g(n)$, set $k = f(n) + g(n)$ and create a (partial) Eudoxus magnitude $h$ with $h(n) = k$ and defined on $[0,n]$.
In words, we look for an even output of either function at $n + 1$, then working on the initial segment $[0,n]$ take point-wise addition on $n$ and then 'ripple back' with $\text{(3)}$.
Claim: The value of the partial functions obtained by using different integers $n$ where $f(n+1) = 2f(n)$ or $g(n+1) = 2g(n)$ always agree on their common initial integer intervals.
If this is true, we've defined a unique function $h: \mathbb N \to \mathbb N $ by just 'going out further towards' $+\infty$. A bonus is that we can then immediately assert that the 'Eudoxus sum' $\oplus$ of two Eudoxus magnitudes is a Eudoxus magnitude.
I would like to prove this using only elementary number theory and logic. But besides writing a Python program to check out the coherence of this endeavor, at this point I don't have any proof at all.
Question 1: Can the above claim be established using any mathematical theories?