hSub_eq_id
plain-language theorem explainer
Under the Route B hypotheses (continuity, f(0)=0, f(1)=1, and the no-signaling split), the substituted map h(x)=f(√x) equals the identity on every nonnegative real. Born-rule uniqueness proofs cite this to reduce f(r)=r² to an identity check after the square-root change of variables. The argument shows the deviation h−id is a continuous additive Cauchy function vanishing at 0 and 1, hence zero on [0,∞).
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be continuous with $f(0)=0$, $f(1)=1$, and satisfying the no-signaling identity $f(rs)+f(r\sqrt{1-s^2})=f(r)$ whenever $r>0$ and $0<s<1$. Define $h(x):=f(\sqrt{x})$ for $x\ge 0$. Then $h(x)=x$ for every $x\ge 0$.
background
Route B is the no-signaling uniqueness path to the Born rule in the Simons–Washburn–Allahyarov paper. The module packages the paper’s hypotheses (SA)+(NC)+(CS)+(PA)+(P5)₂ into a single structure: continuity of $f$, the normalizations $f(0)=0$ and $f(1)=1$, and the no-signaling split $f(rs)+f(r\sqrt{1-s^2})=f(r)$ on the positive quadrant with $s\in(0,1)$.
Earlier steps in the same file convert that split into an additive Cauchy equation for the substituted map $h(x)=f(\sqrt{x})$ (nonnegative domain). Sibling lemmas record $h(0)=0$, $h(1)=1$, continuity of $h$, and additivity $h(a+b)=h(a)+h(b)$ for $a,b\ge 0$. The deviation $g(x):=h(x)-x$ is then itself continuous and additive, and vanishes at the unit points.
The key upstream tool inside the module is the lemma that any continuous additive real function on $[0,\infty)$ that vanishes at $0$ and $1$ is identically zero. That is the bridge from the Cauchy data to pointwise identity.
proof idea
Form the deviation $g:=h-\mathrm{id}$. Continuity of $g$ is immediate from continuity of $h$ (sibling cont lemma) minus continuous_id. Additivity of $g$ on nonnegative summands is the sibling additivity of $h$, rewritten by ring. The values $g(0)=0$ and $g(1)=0$ are the sibling normalizations of $h$ at $0$ and $1$. Feed these four facts, together with $x\ge 0$, into the module lemma that continuous additive maps vanishing at $0$ and $1$ are zero on $[0,\infty)$. Unfold the deviation definition and finish by linear arithmetic to obtain $h(x)=x$.
why it matters
This is the last intermediate before Proposition 3.7 (Route B): $f(r)=r^2$ for all $r\ge 0$. The parent theorem applies the present identity at $x=r^2$, unfolds the square-root substitution, and simplifies by $\sqrt{r^2}=r$ on $r\ge 0$. Without the identity $h=\mathrm{id}$, the Cauchy analysis would stop short of the quadratic Born weight.
In the broader Recognition framework the result closes the analytic half of the Born-rule forcing: once no-signaling has produced an additive continuous $h$, the only remaining freedom is killed by the unit normalizations. The module status is zero-sorry, so this step is fully discharged rather than scaffolding. It does not itself invoke the J-cost, the eight-tick octave, or the $\varphi$-ladder; those enter other routes and mass formulae.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.