born_rule_route_B
plain-language theorem explainer
Under continuity, f(0)=0, f(1)=1, and the no-signaling split identity, any real map f equals the square on the nonnegative reals. Born-rule uniqueness arguments cite this as Proposition 3.7 (Route B). The proof applies the prior identity for the square-root reparametrization of f, then unwinds that reparametrization at r².
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be continuous with $f(0)=0$, $f(1)=1$, and $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for all $r>0$ and $0<s<1$. Then $f(r)=r^2$ for every $r\ge 0$.
background
The module formalizes Route B of the Born rule paper (Simons, Washburn, Allahyarov): premises force the Born modulus map to be quadratic, with status zero sorry. The hypothesis bundle on $f$ is continuity, normalization $f(0)=0$ and $f(1)=1$, and the no-signaling split $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for $r>0$ and $0<s<1$. That identity is the functional residue of no-signaling under a two-outcome radial decomposition.
The auxiliary reparametrization $h_{\mathrm{sub}}(f)(x):=f(\sqrt{x})$ converts the radial problem into an additive Cauchy equation on the nonnegative line (module Steps 1–2). Upstream lemmas already show that, under the full bundle, this reparametrization is the identity on $[0,\infty)$.
proof idea
Invoke the prior lemma that the square-root reparametrization of $f$ equals the identity on nonnegative arguments, evaluated at $r^2$ (nonnegative by construction). Unfold $h_{\mathrm{sub}}(f)(r^2)=f(\sqrt{r^2})$ and simplify $\sqrt{r^2}=r$ for $r\ge 0$ to obtain $f(r)=r^2$. Two-line term proof: one application of the identity lemma, then a targeted simp rewriting the square root.
why it matters
This is the main uniqueness claim of Proposition 3.7 (Route B): the Born weight is forced to be $r^2$, not postulated. Downstream, modulus multiplicativity follows as a one-line corollary (Remark 3.6: multiplicativity is not an axiom), and the route certificate packages both the quadratic law and multiplicativity. In the Recognition verification layer this closes the no-signaling route to the Born rule, complementary to cost-functional uniqueness (J-cost and the Recognition Composition Law) elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.