hSub
plain-language theorem explainer
Defines the square-root reparametrization $h_f(x)=f(\sqrt{x})$ used in Born-rule Route B. Anyone citing Proposition 3.7 Steps 1–2 (no-signaling to additive Cauchy) needs this change of variables. The body is a one-line abbreviation, not a theorem.
Claim. For $f:\mathbb{R}\to\mathbb{R}$ and $x\in\mathbb{R}$, set $h_f(x):=f(\sqrt{x})$.
background
Module BornRuleRouteB formalizes Proposition 3.7 of the Born-rule paper (Simons–Washburn–Allahyarov): premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force $f(r)=r^2$, with zero sorry.
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$.
Steps 1–2 convert that multiplicative split into an additive Cauchy equation. The standard device is to pass to the composed map $x\mapsto f(\sqrt{x})$, so products under the square root become sums of the new argument.
proof idea
Pure definitional abbreviation: evaluate $f$ at $\mathrm{Real.sqrt},x$. No lemmas, no tactics.
why it matters
Local scaffolding for the no-signaling $\to$ additive Cauchy reduction inside Route B. Sibling facts (vanishing at 0, value 1 at 1, continuity, split identity, additivity) are stated for this reparametrized map and feed the uniqueness argument that $f(r)=r^2$.
That uniqueness is the central verification claim of the Born-rule paper in this monolith. Downstream name collisions with hypothesis binders and typeclass subtraction are unrelated; the real consumers are the in-module additive-Cauchy lemmas built on this change of variables.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.