gDev
plain-language theorem explainer
Defines the pointwise deviation of the square-root substitution of f from the identity: g(x) = f(√x) − x. Born-rule uniqueness proofs cite it to convert the additive Cauchy equation for hSub into a zero-deviation statement. The body is a one-line abbreviation of that difference.
Claim. For $f:\mathbb{R}\to\mathbb{R}$ and $x\in\mathbb{R}$, set $g_{\mathrm{dev}}(f,x) := f(\sqrt{x}) - x$.
background
Module BornRuleRouteB formalizes Proposition 3.7 of the Born-rule paper: the premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force $f(r)=r^2$. The Route B hypothesis bundle packages continuity of $f$, the normalizations $f(0)=0$ and $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$.
The auxiliary map $h_{\mathrm{sub}}(f,x):=f(\sqrt{x})$ rewrites no-signaling as an additive split on nonnegative reals. Continuity, $h_{\mathrm{sub}}(0)=0$, and $h_{\mathrm{sub}}(1)=1$ pass from $f$ to $h_{\mathrm{sub}}$. The deviation $g_{\mathrm{dev}}$ measures how far $h_{\mathrm{sub}}$ sits from the identity, so that vanishing of $g_{\mathrm{dev}}$ is exactly $h_{\mathrm{sub}}(x)=x$.
proof idea
Pure definitional abbreviation: unfold to $h_{\mathrm{sub}}(f,x)-x$, i.e. $f(\sqrt{x})-x$. No tactics or lemmas.
why it matters
Feeds the uniqueness theorem $h_{\mathrm{sub}}(f,x)=x$ on $[0,\infty)$. That theorem applies the additive-zero-on-nonnegatives lemma to $g_{\mathrm{dev}}$, using continuity of $h_{\mathrm{sub}}-\mathrm{id}$ and the additive Cauchy identity inherited from no-signaling. Establishing $h_{\mathrm{sub}}=\mathrm{id}$ is the bridge from the no-signaling split to $f(r)=r^2$, the central claim of Route B (Proposition 3.7). Status of the module is zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.