route_B_certified
plain-language theorem explainer
Packages Route B uniqueness into a single certificate: under continuity, normalization, and the no-signaling identity, any real map f equals the Born modulus r ↦ r² on the nonnegative reals and is multiplicative there. Cite when a downstream verifier needs both quadratic form and multiplicativity as one Prop. Proof is a structure constructor that wires the two established lemmas.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ be continuous with $f(0)=0$, $f(1)=1$, and satisfying the no-signaling identity $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for all $r>0$ and $0<s<1$. Then $f$ is certified as the Born rule: $f(r)=r^2$ for every $r\ge 0$, and $f(r_1 r_2)=f(r_1)f(r_2)$ whenever $r_1,r_2\ge 0$.
background
Module formalizes Proposition 3.7 of the Born-rule paper (Simons–Washburn–Allahyarov): premises that encode no-signaling uniqueness force the Born modulus. Status is zero sorry.
The hypothesis bundle collects four conditions 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 $r>0$ and $0<s<1$. From these the module derives an additive Cauchy equation on a substituted map, then recovers $f(r)=r^2$.
The certificate is a two-field Prop: quadratic form on $\mathbb{R}_{\ge 0}$, and multiplicativity on the same cone. Multiplicativity is recorded as a corollary (Remark 3.6), not an independent axiom. Upstream cost algebra defines the shifted cost $H(x)=J(x)+1=\tfrac12(x+x^{-1})$, under which the Recognition Composition Law becomes d'Alembert's equation; that background motivates the functional-equation route but is not invoked in this packaging step.
proof idea
Term-mode structure construction, not a new argument. The quadratic field is filled by applying born_rule_route_B (Proposition 3.7) at each $r\ge 0$. The multiplicativity field is filled by applying modulus_multiplicativity, which itself is a one-line ring rewrite from the quadratic identity at $r_1$, $r_2$, and $r_1 r_2$. No additional tactics or Cauchy analysis occur here.
why it matters
Terminal packaging theorem for Route B inside the verification layer. It turns the proved uniqueness $f(r)=r^2$ and its multiplicative corollary into a single named certificate that external checkers can demand as one hypothesis. The module doc ties it to Proposition 3.7 of the Born-rule paper: premises (SA)+(NC)+(CS)+(PA)+(P5)₂ force the Born modulus. In the broader Recognition framework this is the no-signaling route to the probability law that sits on top of the forcing chain (T5 J-uniqueness and the RCL), rather than a new derivation of $J$ or $\varphi$. No downstream consumers are wired yet in the graph; the declaration is the export surface for the route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.