[mschuetz]

File formats for georeferenced data also regularly store coordinates as 32 bit ints, with a scaling argument that can be used to convert the integer into a double precision number with a specific unit. E.g. your scene unit is meters and you want to store with a precision of millimeters? Multiply double precision coordinates by 1000, convert the result to an int32, save it to file. When you load the coordinate afterwards, divide it by 1000 and you you get back your double precision coordinate.