RouteBHyp
plain-language theorem explainer
Route B packages the four analytic hypotheses that force the Born-rule map f to equal the square on the nonnegative reals. Continuity, the normalizations f(0)=0 and f(1)=1, and the no-signaling split identity are collected as a single Prop on f. Anyone citing Proposition 3.7 of the Born-rule paper takes this bundle as the standing assumption. The declaration is a structure, not a proved statement; downstream lemmas discharge uniqueness from these fields alone.
Claim. A real function $f$ satisfies the Route B hypotheses when it is continuous, $f(0)=0$, $f(1)=1$, and the no-signaling identity holds: for all $r>0$ and $0<s<1$, $f(r s)+f\bigl(r\sqrt{1-s^2}\bigr)=f(r)$.
background
The module formalizes Proposition 3.7 of the Born-rule paper (Simons, Washburn, Allahyarov): under a short list of structural premises, the only admissible response map is $f(r)=r^2$. Route B is the no-signaling uniqueness path. The structure here is the pre-processed hypothesis bundle for parts (a)–(d) of that proposition.
The four fields are continuity of $f$, the two normalizations $f(0)=0$ and $f(1)=1$, and the geometric split identity that encodes no-signaling on positive radii. The split uses the complementary factor $\sqrt{1-s^2}$, so the two arguments of $f$ behave like adjacent legs of a right triangle scaled by $r$.
Downstream work rewrites the split in squared coordinates via the auxiliary map $hSub,f,x:=f(\sqrt{x})$. That change of variables turns the no-signaling identity into an additive Cauchy equation on the positive reals, which continuity then forces to be linear.
proof idea
No proof body: the declaration is a Prop-valued structure. It simply records four named fields (continuity, value at 0, value at 1, no-signaling split) that later lemmas project out. Typical use is to pass a term of type RouteBHyp f into hSub_cont, hSub_one, hSub_split, hSub_additive, and finally hSub_eq_id and born_rule_route_B.
why it matters
This bundle is the single hypothesis of the main uniqueness theorem born_rule_route_B, which states $f(r)=r^2$ for all $r\ge 0$. Every intermediate lemma in the module (hSub_cont, hSub_one, hSub_split, hSub_additive, hSub_eq_id, modulus_multiplicativity, and the additive-zero lemmas) takes a RouteBHyp assumption and peels off one field or a derived Cauchy identity.
In the paper numbering this is Proposition 3.7(a)–(d) pre-processed. The module status is zero sorry, so the structure is the clean interface between the physical premises (no-signaling plus mild regularity) and the forced Born square. Measure additivity (MA) is recovered later as a corollary, not assumed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.