hSub_split
plain-language theorem explainer
Under Route B hypotheses (continuity, f(0)=0, f(1)=1, no-signaling), the square-root reparametrization h(x)=f(√x) obeys the split law h(R p)+h(R(1-p))=h(R) for R>0 and p∈(0,1). Anyone deriving Born-rule uniqueness from no-signaling (Prop. 3.7) cites this. Proof is a change of variables that feeds the no-signaling clause directly.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be continuous with $f(0)=0$, $f(1)=1$, and no-signaling identity $f(r s)+f(r\sqrt{1-s^2})=f(r)$ for all $0<r$ and $0<s<1$. Writing $h(x)=f(\sqrt{x})$, one has $h(R p)+h(R(1-p))=h(R)$ whenever $R>0$ and $0<p<1$.
background
The module formalizes Born Rule Route B (Proposition 3.7 of Simons–Washburn–Allahyarov): the premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force $f(r)=r^2$. Status is zero sorry.
RouteBHyp f packages continuity of $f$, the boundary values $f(0)=0$ and $f(1)=1$, and the no-signaling clause
$f(r s)+f(r\sqrt{1-s^2})=f(r)$ for $0<r$ and $0<s<1$. The auxiliary $h(x):=f(\sqrt{x})$ (written hSub f) is the reparametrization used in Steps 1–2 of the module, which convert no-signaling into an additive Cauchy equation on the positive reals.
Physically, no-signaling says a binary amplitude split creates no signaling channel; algebraically it is the seed identity that this lemma rewrites in $h$-coordinates.
proof idea
Unfold $h(x)=f(\sqrt{x})$. Set $r:=\sqrt{R}$ and $s:=\sqrt{p}$. Positivity of $r,s$ is immediate from $R>0$ and $p>0$; $s<1$ follows from $p<1$ via $s^2=p$ and a short nlinarith. The product rule for square roots gives $\sqrt{R p}=r s$ and $\sqrt{R(1-p)}=r\sqrt{1-s^2}$. Substituting these into the claimed equality reduces it exactly to the no-signaling clause of RouteBHyp applied at $(r,s)$, which is discharged by H.no_sig.
why it matters
Immediate parent is hSub_additive, which upgrades the binary split to full additivity $h(x+y)=h(x)+h(y)$ on positives. Continuity then forces $h(x)=c x$, and the normalization $f(1)=1$ yields $f(r)=r^2$: the Born amplitude-to-probability map. That is the content of Steps 1–2 in the module header (“No-Signaling → Additive Cauchy Equation”) and of Proposition 3.7 in the Born-rule paper. The lemma therefore sits on the verification spine that the RS derivation of the Born rule is fully discharged in Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.