hSub_zero
plain-language theorem explainer
Under the Route B hypothesis bundle, the substituted map h(x)=f(√x) vanishes at zero. Anyone proving Born-rule uniqueness f(r)=r² via the additive Cauchy route cites this as the base case for the deviation argument. The proof is a one-line simp that unfolds the substitution and applies f(0)=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)$ for $r>0$ and $0<s<1$. Define $h(x):=f(\sqrt{x})$. Then $h(0)=0$.
background
Module BornRuleRouteB formalizes Proposition 3.7 of the Born-rule paper: premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force $f(r)=r^2$. Status is zero sorry.
RouteBHyp packages the pre-processed hypotheses: 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)$ for $r>0$, $0<s<1$.
The auxiliary substitution is $h(x):=f(\sqrt{x})$. Steps 1–2 of the module convert no-signaling into an additive Cauchy equation for $h$ on the nonnegative reals; the zero value of $h$ is the first normalization needed for that reduction.
proof idea
One-line wrapper. Unfold $h(x)=f(\sqrt{x})$, reduce $\sqrt{0}$ to $0$ by Real.sqrt_zero, then apply the bundled fact $f(0)=0$ from RouteBHyp. No further lemmas are required.
why it matters
Feeds hSub_eq_id, which proves $h(x)=x$ for all $x\ge 0$ by showing the deviation $g(x)=h(x)-x$ is additive and continuous, hence zero on the nonnegatives once it vanishes at zero. That identity is the algebraic core of Route B: once $f(\sqrt{x})=x$, the Born rule $f(r)=r^2$ follows on the positive ray. The module is the formalization of the paper's uniqueness theorem under no-signaling; this lemma is the base case of the additive-deviation argument that closes the proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.