I believe the reason why we get the visual impression that the monospace
font is larger than the proportional, even though they take up as many
vertical pixels, is because it takes up more horizontal space.

Such visual illusions are not entirely uncommon in typography, and the
normal solution is to forget about aligning things "mathematically" or
with a ruler.  (Doing that would be counter-productive when the key
thing is what it looks like to a human reader and not to a machine.)
Instead, you simply eye-ball it.  There's no way around it.

So my conclusion is that Emacs does things "right" here, in the sense
that it doesn't do any adjustments: it just presents the font at the
specified font size.

We probably should make some adjustments to be more appealing to a human
reader, but the tricky part is what exactly to do.  Making the variable
width font slightly larger would work on my machine, but it won't work
if the chosen fonts have different x-heights.  (Eli's report was
illuminating: he seems to have the exact opposite problem from what we
have both observed.)

What, if anything, does TeX do about this?

Does harfbuzz, or something else, provide us with a way to know the
x-height of a character?