modulus_multiplicativity
plain-language theorem explainer
Multiplicativity of the Born modulus on nonnegative reals is a corollary of Route B uniqueness, not an independent axiom. Under the Route B hypotheses (continuity, normalization, no-signaling), any admissible f satisfies f(r₁ r₂) = f(r₁) f(r₂) for r₁, r₂ ≥ 0. Cite this for Remark 3.6 of the Born-rule paper. The proof is a one-line reduction through the already-proved identity f(r) = r².
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 $f(rs)+f(r\sqrt{1-s^2})=f(r)$ whenever $0<r$ and $0<s<1$. Then for all $r_1,r_2\ge 0$, $f(r_1 r_2)=f(r_1)\,f(r_2)$.
background
This module formalizes Proposition 3.7 of the Born rule paper (Simons, Washburn, Allahyarov): the listed premises force $f(r)=r^2$. The Route B hypothesis bundle packages continuity of $f$, the normalizations $f(0)=0$ and $f(1)=1$, and the no-signaling split $f(rs)+f(r\sqrt{1-s^2})=f(r)$ for positive $r$ and $s\in(0,1)$.
Upstream uniqueness already identifies every such $f$ with squaring on the nonnegative reals. Multiplicativity of the modulus (MA in the paper) is therefore not an extra axiom; once $f(r)=r^2$ is known, the product law is pure algebra. The downstream certificate records both the quadratic law and this multiplicative law as certified consequences of the same hypothesis bundle.
proof idea
One-line term proof. Invoke Route B uniqueness three times: on the product $r_1 r_2$ (nonnegative because both factors are), on $r_1$, and on $r_2$. The goal rewrites as $(r_1 r_2)^2 = r_1^2\cdot r_2^2$, which ring closes.
why it matters
Remark 3.6 of the paper insists that modulus multiplicativity is a corollary, not a primitive assumption. This lemma makes that claim machine-checkable inside the zero-sorry Route B development. It is consumed by the Route B certificate, which packages both $f(r)=r^2$ and the product law under the same hypothesis bundle; that certificate is the audited endpoint of the no-signaling uniqueness route to the Born rule.
In the broader Recognition Science stack, Route B sits in the verification layer: it shows that the Born modulus is forced by continuity, normalization, and no-signaling, rather than being postulated. It is complementary to the forcing chain (T0–T8) that fixes the cost functional $J$, the golden ratio fixed point, the eight-tick octave, and $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.