hSub_cont
plain-language theorem explainer
Under the Route B hypothesis bundle (continuity, normalization, and no-signaling), the substituted map x ↦ f(√x) is continuous. Anyone reducing no-signaling uniqueness to an additive Cauchy equation on [0,∞) cites this. Proof is a one-line composition of continuous maps: continuity of f with continuity of square root.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be continuous with $f(0)=0$, $f(1)=1$, and satisfy the no-signaling identity $f(rs)+f(r\sqrt{1-s^2})=f(r)$ whenever $0<r$ and $0<s<1$. Then the map $x\mapsto f(\sqrt{x})$ is continuous on $\mathbb{R}$.
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.
The Route B hypothesis bundle packages four pre-processed axioms on $f$: continuity, $f(0)=0$, $f(1)=1$, and the no-signaling split $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for $0<r$ and $0<s<1$. The substituted map is defined by $h(x):=f(\sqrt{x})$; it converts the multiplicative no-signaling identity into an additive Cauchy equation on the nonnegative reals (Steps 1–2 of the module).
Continuity of $h$ is the first regularity fact needed before uniqueness theorems for continuous additive maps can be applied.
proof idea
One-line wrapper. The hypothesis bundle already supplies continuity of $f$. Compose with Mathlib's continuous_sqrt via the standard fact that the composition of continuous real functions is continuous: H.cont.comp continuous_sqrt. No further lemmas from CostAlgebra or the functional-equation layer are used.
why it matters
Feeds the uniqueness theorem hSub_eq_id, which proves $f(\sqrt{x})=x$ for all $x\ge 0$ and thereby $f(r)=r^2$ on the positive ray. That parent applies additive-zero lemmas to the continuous deviation $h-\mathrm{id}$, so continuity of $h$ is an indispensable hypothesis there.
In the broader Recognition framework this is a verification lemma for the Born-rule route, not a forcing-chain step (T0–T8). It closes the regularity gap between the no-signaling axiom and the additive Cauchy analysis that yields the quadratic Born weight. No open scaffolding remains in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.