Imprecise font scaling

Hello,

I'm running the following code

\version "2.25.12"
\markup { LOL }
\markup { \magnify #2.0 LOL }

and the results are not really precise. When producing --eps, the relevant output lines are

/C059-Roman 3.86523438 output-scale div selectfont
/C059-Roman 7.73242188 output-scale div selectfont

However, 2 * 3.86523438 = 7.73046876 != 7.73242188. Basically the same behaviour can be
observed when using Cairo (both for EPS and SVG). (Producing SVG without Cairo is pretty
disastrous in this regard, but that doesn't bother me too much at the moment.)

You might say that the differences are negligible; and perhaps you're right. On the other
hand, I'd be alarmed if my code produced such a "big" difference when a simple multiplication
by two is expected.

By the way, my initial motivation was to find out what the output font sizes *really* are
(especially with respect to the lyrics) so that I can include LilyPond examples in TeX
with *exactly* the same font (size). I couldn't locate any documentation for these
mechanisms so far…

Best,
AS