additive_zero_on_unit
plain-language theorem explainer
A continuous real function additive on positive arguments and vanishing at 0 and 1 must vanish on the whole unit interval [0,1]. Born-rule uniqueness proofs cite it to kill residual additive defects before extending off the unit interval. The argument is a compactness bound on [0,2] plus integer scaling that forces |N g(x)| past the bound.
Claim. Let $g:\mathbb{R}\to\mathbb{R}$ be continuous and satisfy $g(x+y)=g(x)+g(y)$ for all $x,y>0$, with $g(0)=0$ and $g(1)=0$. Then $g(x)=0$ whenever $0\le x\le 1$.
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 objects are continuous real maps $g$ that obey Cauchy's equation only on the open positive orthant, together with the normalization $g(0)=g(1)=0$. Sibling lemmas supply the integer scaffolding: repeated addition gives $g(nx)=n,g(x)$ for $n\in\mathbb{N}$ and $x>0$, and $g$ vanishes on every natural number because it is a sum of ones.
Compactness of $[0,2]$ supplies a uniform bound on $|g|$ once continuity is assumed; that bound is the only analytic input beyond additivity.
proof idea
Split on the endpoints: $x=0$ or $x=1$ is immediate from the normalizations. For $0<x<1$, take a maximizer of $|g|$ on the compact interval $[0,2]$ and set $M:=|g(z)|+1$, so $|g|\le M$ on that interval.
Assume $g(x)\ne 0$. Choose $N\in\mathbb{N}$ larger than $M/|g(x)|$. The integer-scaling lemma yields $g(Nx)=N,g(x)$. Write $Nx=\lfloor Nx\rfloor+\mathrm{frac}$ with fractional part in $[0,1)$. The integer part has $g$-value zero (sum of ones), so additivity gives $g(Nx)=g(\mathrm{frac})$. But then $N|g(x)|=|g(\mathrm{frac})|\le M$, contradicting the choice of $N$.
why it matters
Immediate parent is additive_zero_on_nonneg, which extends the vanishing statement from the unit interval to every nonnegative real by the same additivity (split $x\le 1$ versus $x>1$). That lemma is part of the Route-B chain that forces any continuous defect compatible with the Born-rule hypotheses to be identically zero, hence $f(r)=r^2$.
In the broader Recognition framework this is verification infrastructure rather than a forcing-chain landmark (T5–T8). It closes the analytic half of the no-signaling uniqueness argument: once additive continuous defects are killed on $\mathbb{R}_{\ge 0}$, the remaining algebraic constraints pin the quadratic Born weight. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.