hSub_one
plain-language theorem explainer
Under the Route B hypothesis bundle, the square-root reparametrization of f sends 1 to 1. Anyone tracing the no-signaling path from continuous f with f(0)=0, f(1)=1 to the additive Cauchy equation needs this normalization. The proof is a one-line simp unfolding the reparametrization and applying f(1)=1.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ satisfy the Route B hypotheses (continuity, $f(0)=0$, $f(1)=1$, and the no-signaling identity). Define $h(x):=f(\sqrt{x})$. Then $h(1)=1$.
background
Route B formalizes Proposition 3.7 of the Born-rule paper: the premises (SA)+(NC)+(CS)+(PA)+(P5)$_2$ force $f(r)=r^2$. The structure RouteBHyp packages the pre-processed hypotheses: continuity of $f$, the endpoint values $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(x):=f(\sqrt{x})$ converts that identity into an additive Cauchy equation on the nonnegative reals (Steps 1–2 of the module). The cost-algebra $H(x)=J(x)+1=\frac12(x+x^{-1})$ is imported only as ambient Recognition infrastructure; the present lemma uses only the endpoint $f(1)=1$.
proof idea
One-line wrapper. Unfold $h(x)=f(\sqrt{x})$, reduce $\sqrt{1}$ to $1$ by Real.sqrt_one, then apply the field $f,1=1$ from the hypothesis bundle. No further lemmas are required.
why it matters
Normalization at the unit is the first concrete evaluation of $h$ after its definition. Downstream, hSub_eq_id uses it (together with continuity, additivity, and vanishing of the deviation $g=h-\mathrm{id}$ on the nonnegatives) to conclude $h(x)=x$ for all $x\ge 0$, which is the bridge from no-signaling to $f(r)=r^2$.
In the Recognition framework this sits inside the Born-rule uniqueness route, not the T0–T8 forcing chain itself; it is verification that the probability map forced by no-signaling is the Born quadratic. The module is already zero-sorry, so the lemma closes a trivial but mandatory base case rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.