I.e., it's not just the size difference, but also that they use
different font shapes.