Amazing summary, Jeremy!
One nitpick is regarding the double-CRT: you are referring to the RNS encoding, when the original paper[0] uses the term to talk about how polynomials are stored for fast computation. It's a nice philosophical view of decomposing the polynomial Φm(X) into products X − ζi the same way that the integer modulus Q is decomposed into primes. So it's more like one CRT on the coefficients, and another implemented as a DFT.