RouteBCert
plain-language theorem explainer
Packages the two target properties of the Born-rule modulus: nonnegatively, f equals the square map and is multiplicative. Anyone citing Route B uniqueness (Proposition 3.7 of the Born-rule paper) uses this as the certified conclusion type. It is a Prop-valued structure, so there is no proof body; instances are assembled by filling the two fields.
Claim. A map $f:\mathbb{R}\to\mathbb{R}$ has a Route B Born-rule certificate when $f(r)=r^2$ for all $r\ge 0$ and $f(r_1 r_2)=f(r_1)f(r_2)$ whenever $r_1,r_2\ge 0$.
background
Module BornRuleRouteB formalizes Proposition 3.7 of the Born-rule paper (Simons, Washburn, Allahyarov): under the Route B premise bundle (SA)+(NC)+(CS)+(PA)+(P5)₂, the only admissible response function is the Born modulus $f(r)=r^2$. The module status is zero sorry.
The certificate is the conclusion shape of that uniqueness argument. Its first field is pointwise equality with the square on the nonnegative reals; the second is multiplicativity on the same cone. Multiplicativity is the algebraic shadow of independent composition of amplitudes (or of no-signaling product structure), while the quadratic identity is the Born rule itself.
Upstream, the module imports only Mathlib and RS Constants. The sibling hypothesis bundle (RouteBHyp and the hSub family) supplies the analytic and additive constraints from which both fields are later derived.
proof idea
Definitional packaging, not a proved theorem. The structure is a Prop with two fields: a universal quadratic identity on $\mathbb{R}_{\ge 0}$, and a two-argument multiplicativity identity on the same cone. No tactics or lemmas run here. Downstream, route_B_certified builds an instance by feeding born_rule_route_B into the quadratic field and modulus_multiplicativity into the mult field.
why it matters
This is the certified output type of Route B. The parent theorem route_B_certified states that every $f$ satisfying the Route B hypothesis bundle carries such a certificate, with quadratic filled by born_rule_route_B and mult by modulus_multiplicativity. That is the Lean rendering of Proposition 3.7: no-signaling uniqueness forces the Born rule.
In the broader Recognition framework the Born modulus is the bridge from the discrete recognition calculus to quantum measurement statistics. Pinning $f(r)=r^2$ with multiplicativity closes the Route B path to that bridge and keeps the verification layer free of sorry. It does not itself invoke the forcing chain T0–T8 or the J-cost, but it is the measurement-side counterpart those foundations must eventually match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.