additive_nat_zero
plain-language theorem explainer
If a real function is Cauchy-additive on the positive reals and vanishes at 0 and 1, then it vanishes at every natural number. Born-rule uniqueness arguments cite this to kill the additive defect on ℕ before extending by continuity. The proof is a one-line specialization of the companion natural-multiple lemma at x = 1.
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$ and $g(1)=0$. Then for every natural number $n$, $g(n)=0$.
background
Module BornRuleRouteB formalizes Proposition 3.7 of the Born-rule paper: premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force the Born weight $f(r)=r^2$. Status is zero sorry.
The local strategy isolates an additive defect $g$ of the candidate weight. Additivity is required only on strictly positive reals: $g(x+y)=g(x)+g(y)$ for $x,y>0$, together with the normalization $g(0)=0$. The companion lemma additive_nat_mul already gives $g(n\cdot x)=n\cdot g(x)$ for $n\in\mathbb{N}$ and $x>0$, by induction on $n$ from the zero case $g(0)=0$.
Here one only needs the integer points themselves. Setting the free positive argument to $1$ and using $g(1)=0$ collapses the multiple to zero, so $g$ vanishes on all of $\mathbb{N}\subset\mathbb{R}$.
proof idea
One-line specialization of additive_nat_mul. Instantiate that lemma at the positive real $x=1$ (via one_pos) to obtain $g(n\cdot 1)=n\cdot g(1)$. Simplify $n\cdot 1=n$ by mul_one, rewrite, then apply $g(1)=0$ and mul_zero to conclude $g(n)=0$.
why it matters
Feeds the two immediate parents additive_zero_on_unit and additive_zero_on_nonneg, which extend vanishing from $\mathbb{N}$ first to the unit interval and then to all nonnegative reals, using continuity of $g$. Those steps are the arithmetic core of Route B: once the additive defect is identically zero on $[0,\infty)$, the no-signaling identity forces the Born weight $f(r)=r^2$.
In the Recognition Science ledger this sits inside the verification layer that certifies the Born rule as a forced consequence of the listed axioms, rather than an independent postulate. It does not itself invoke the forcing chain T0–T8 or the J-cost; it is pure real-analysis scaffolding for Proposition 3.7.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.