@gregeganSF This is the kind of thing the robots are good at finding nowadays and, lo, I asked a robot and it found a reference.

(If you are sufficiently allergic to robot-derived information, you may choose to stop reading here. It looks to me as if the robot got it right, though.)

Luis A. Santaló, “Convexidad en el plano hiperbólico”, Matemática y Física Teórica XIX (1969), pp. 174–184, equation (2.6). https://ciaem-iacme.org/wp-content/uploads/2019/05/Convexidad-en-el-plano-hiperbolico.pdf

It's in Spanish, which I don't read very well, so I haven't actually checked that what Santaló is calculating is the same thing as you are, but the robot thinks it is.

The formula isn't exactly the same as yours but is equivalent. Santaló's formula is 4 sinh d/2 - 4 atan sinh d/2, which will be the same as yours if atan sinh d/2 = 2 atan tanh d/4, i.e., if sinh d/2 = 2 tanh d/4 / (1 - tanh^2 d/4), which is true.

There's a paper from Santaló two years earlier (in English) that might but probably doesn't have the same or an equivalent formula in, but it isn't freely available online.

If there's an earlier appearance of the formula, the robot doesn't know of it and couldn't find it. (Neither do I or could I, but I didn't find the Santaló paper either.)