[jacobolus]

In this particular case, they’re just using a standard double precision IEEE 754 floating point number. So I assume they do all of their arithmetic (“for JPL's highest accuracy calculations”) using double precision floats.