@Burak Yeesh! No doubt that would be even worse, since it's now insiders who can get confused. Mathematicians are sometimes just really bad (irreflective) about choosing terminology and notation. I guess the same is true in every sphere of life (time for me to quit this thread, I think).

@AndrésE.Caicedo Never!! :-)

@Burak Okay, my apologies for attributing this to you, and I will remove that attribution. (But I am still of the strong opinion that the notation is terrible!) Dominic: merriam-webster.com/dictionary/egad

Egad, that is bad notation. I find it quite perverse to use the arrow notation both for a structure (a function: the usual notation) and for a property. I quite failed to understand at first that $\not \to$ meant failure of that property.

Does anyone know how to describe in formal terms how the "Francis function" is well-behaved over PSD matrices?

It's a worthwhile question, but I think you can take for granted that the experts who can answer will already be aware of the various subtleties.

Zolaterev's proof really is beautifully conceptual and explanatory, but as far as I know, it doesn't suggest similar conceptual proofs for other aspects of class field theory.

@PeterLeFanuLumsdaine That's a fair point.

@Z.M No, the adjoint functor theorems (whether SAFT or GAFT or some variant) don't use choice.

Thank you, @LSpice!

This works: (see 033 Why Math): fun.mawan.de/Comics/SpikedMath