Tension between two independent measurements, $|x-y|/\sqrt{\sigma_x^2+\sigma_y^2}$

The tension between two independent measurements $x\pm\sigma_x$ and $y\pm\sigma_y$ of the same quantity, expressed in units of the combined standard deviation:

This is the conventional significance of a difference between two independent Gaussian measurements; it is the quantity behind statements such as "$H_0=73.50\pm0.81$ is $7.1\sigma$ from $67.24\pm0.35$" in the abstract of the paper.

Formalization Note The paper does not write the formula out; this is the standard convention, and it reproduces every "$n\sigma$ from" figure quoted in the abstract and in Sect. 5.2.4 (to the stated rounding). The function is total: if $\sigma_x=\sigma_y=0$ the denominator is $0$ and Lean's division returns $0$; all uses in the mission have positive uncertainties.