Scaling this back to the loud volume of step 1 (RTX6001 at 10 V output range), that's 3.8 mA. This is quite a bit lower that the 20 mA target, due to lower power of high/treble frequencies of real music (opposed to typical audio test signals).
Conclusion 2: the output swing target of 20 mA-peak is (much) more than enough for typical music signals!
Ok, the next step is to actually design the ouput stage...
If survival of the listener when the headphone's insulation fails is of importance, and it could very well be for DIY electrostatic headphones, it would be nice to have an accurate current limit at some non-lethal value.
Residual-current devices here are usually designed to trip at 30 mA RMS, so 20 mA peak is still below that. However, if the gyrator circuit mimics an ideal inductor accurately, the current through it will just increase without bound when there is a short. An ordinary current source would be safer in that sense, or a gyrator circuit with a built-in current limiter.