hSub_additive
plain-language theorem explainer
Under the Route B hypothesis bundle (continuity, endpoint values, no-signaling), the substituted map attached to f is additive on positive reals. Anyone closing the Cauchy step of Born-rule uniqueness (toward f(r)=r²) cites this. The proof reduces additivity to the split identity by barycentric weights x/(x+y) and y/(x+y), then finishes by linear arithmetic.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy the Route B hypotheses: continuity, $f(0)=0$, $f(1)=1$, and the no-signaling identity $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for $r>0$ and $0<s<1$. Write $h_f$ for the associated substituted map. Then $h_f(x+y)=h_f(x)+h_f(y)$ whenever $x>0$ and $y>0$.
background
The module formalizes Proposition 3.7 of the Born-rule paper (Simons–Washburn–Allahyarov): the premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force $f(r)=r^2$. Status is zero sorry.
RouteBHyp f packages the pre-processed hypotheses: $f$ continuous, $f(0)=0$, $f(1)=1$, and the no-signaling identity
$f(r s)+f(r\sqrt{1-s^2})=f(r)$ for $r>0$ and $0<s<1$. The section heading marks Steps 1–2: convert no-signaling into an additive Cauchy equation for a transformed map $h_f$ (written hSub f in the development).
Upstream support is elementary positivity and cancellation on $\mathbb{R}_{>0}$ (sum of positives is positive; $S\cdot(x/S)=x$), together with the in-module split lemma that decomposes $h_f$ along a convex weight in $(0,1)$.
proof idea
Fix $x,y>0$. Let $S:=x+y>0$ and $p:=x/S$. Then $0<p<1$, $S\cdot p=x$, and $S\cdot(1-p)=y$ (the last by field simplification and linear arithmetic). Apply the split lemma hSub_split at $S$ and $p$, which expresses $h_f(S)$ as the sum of $h_f$ on the two scaled pieces. Rewrite those pieces to $x$ and $y$, then close by linarith. The argument is local to positives and does not yet use continuity of $h_f$.
why it matters
Sole downstream consumer is hSub_eq_id, which proves $h_f(x)=x$ for all $x\ge 0$. That proof builds the continuous additive deviation $g=h_f-\mathrm{id}$, invokes the present additivity to get $g(a+b)=g(a)+g(b)$ on positives, and concludes $g\equiv 0$ by the bounded-deviation Cauchy argument in the same module.
Identifying $h_f$ with the identity is the bridge from no-signaling to the quadratic Born rule $f(r)=r^2$ along Route B (Proposition 3.7). It sits in the verification layer that certifies the measurement postulate rather than in the T0–T8 forcing chain, but it is required for the RS claim that Born weights are forced rather than postulated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.