additive_zero_on_nonneg
plain-language theorem explainer
Continuous real functions additive on the positive reals and vanishing at 0 and 1 must vanish on the whole nonnegative half-line. Born-rule uniqueness cites this when the deviation of the subadditive envelope from the identity is forced to zero. The proof splits at the unit interval and reduces the exterior case via floor-plus-fraction decomposition.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ be continuous and satisfy $g(x+y)=g(x)+g(y)$ whenever $x,y>0$, with $g(0)=g(1)=0$. Then $g(x)=0$ for every $x\ge 0$.
background
Module BornRuleRouteB formalizes Proposition 3.7 of the Born-rule paper: premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force the response function $f(r)=r^2$. Route B works by studying a continuous subadditive envelope $h$ of $f$ on the nonnegative reals and the deviation $g:=h-\mathrm{id}$.
Cauchy's functional equation on $(0,\infty)$ is the local algebraic engine. With continuity, additivity, and the two normalization values $g(0)=g(1)=0$, the only continuous solution is the zero function. Two sibling lemmas prepare the ground: vanishing on the unit interval $[0,1]$, and vanishing at every natural number (by induction from $g(1)=0$).
proof idea
Case-split on whether $x\le 1$ or $x>1$.
- If $x\le 1$, apply the sibling lemma that already gives $g\equiv 0$ on the unit interval (using continuity, additivity on positives, and the two normalizations).
- If $x>1$, write $x=n+f$ with $n=\lfloor x\rfloor\in\mathbb{N}$ and fractional part $f\in[0,1)$. The natural-number lemma yields $g(n)=0$. If $f=0$ we are done. If $f>0$, positivity of $n$ lets additivity split $g(x)=g(f)+g(n)=g(f)$; the unit-interval lemma then kills $g(f)$.
why it matters
Immediate parent is the identity theorem for the subadditive envelope: the deviation $g=h-\mathrm{id}$ satisfies the hypotheses of this lemma, so $g\equiv 0$ on $[0,\infty)$ and therefore $h(x)=x$. That identity is the algebraic core of Route B uniqueness, which forces $f(r)=r^2$ under the no-signaling package (SA)+(NC)+(CS)+(PA)+(P5)₂.
In the broader Recognition Science ledger this closes the continuous Cauchy step inside the Born-rule verification chain; the module is already zero-sorry. It does not itself invoke the forcing chain T0–T8 or the J-cost, but it is the analytic bottleneck that lets the probabilistic response sit on the identity before the quadratic conclusion is read off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.