additive_nat_mul
plain-language theorem explainer
If a real map is additive on positive reals and vanishes at zero, it is homogeneous over the naturals: g(n x) = n g(x) for every natural n and every x > 0. Cited inside Born-rule Route B after no-signaling has been reduced to an additive Cauchy equation on a transformed amplitude. Proof is induction on n, with a positivity check and ring rewrite in the successor step.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ satisfy $g(x+y)=g(x)+g(y)$ whenever $x>0$ and $y>0$, and suppose $g(0)=0$. Then for every $n\in\mathbb{N}$ and every $x>0$, $g(n\cdot x)=n\cdot g(x)$.
background
The module formalizes Born-rule Route B (Proposition 3.7): under continuity, normalization, and a no-signaling identity, the amplitude map is forced to $f(r)=r^2$. The Route B hypothesis bundle packages those premises: continuous $f$ with $f(0)=0$, $f(1)=1$, and $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for $r>0$ and $0<s<1$.
A change of variables $h(x)=f(\sqrt{x})$ turns the no-signaling identity into a two-term split on positive reals, i.e. an additive Cauchy equation on a restricted domain. Once that additive equation is in hand, standard real-analysis lemmas recover homogeneity and, with continuity, full linearity. The present statement is the natural-number homogeneity step for any additive $g$ with $g(0)=0$.
proof idea
Induction on $n$. The zero case is immediate from $g(0)=0$ and $0\cdot x=0$. In the successor case the proof splits on the predecessor: $n=1$ is a one-line simplification; for $n=m+2$ with $m\ge 0$ one rewrites $(m+2)x=(m+1)x+x$, checks positivity of $(m+1)x$ (so additivity applies), substitutes the inductive hypothesis, and finishes by casting and ring arithmetic.
why it matters
Private scaffolding inside Steps 1–2 of Route B (no-signaling to additive Cauchy). Downstream it feeds the lemma that an additive $g$ with $g(1)=0$ vanishes on every natural, and then the continuity argument that such a $g$ vanishes on the whole unit interval. Those vanishing lemmas close the uniqueness path that forces the Born amplitude $f(r)=r^2$ under the Route B premises. The module is marked zero-sorry; this lemma is one of the pure analytic rungs that keep the chain fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.