Alright, some more simulation results, then.
I made a completely new set with a slightly enhanced oscillator model that now also incorporates flicker noise, which I think is more prominent in crystal oscillators than pure white noise. The effect of it is visible in the cyan curve, it is less steep because flicker noise doesn't average out like white noise.
Looking back at the my previous results, I'm pretty sure I made a mistake with the tc=2000 plot, it is considerably worse than you'd expect.
The colors are the same as before, I just added the ADEV of the TIC measurements in "green", it shows the effect of filtering most prominently.
First graph is without qerr correction, no filtering and tc=1000, which should be fairly optimal for this oscillator.
Second graph is identical but includes a 60 second EMA filter on the TIC measurements. See how the green curve gets flatter. Also notice that the effect for tau < 100s is almost negligible, there's a slight improvement between 100s and 1000s but the stability around 1000s is slightly worse.
Third graph is with qerr correction, no filter, tc=1000. There's a visible advantage for tau > 100s, but one can also see that the performance for tau > 1000 is worse than it could be. The time constant is too long already for this combination of GPS and oscillator.
Fourth graph is again no qerr correction, no filter but tc=2000, which gives a better result which almost matches the result from the sawtooth corrected GPS, but not quite. Of course such long time constants comes at a cost: you better have a really well controlled environment because the control loop will basically do nothing to counter any such effects.
I think this shows that there is definitely an advantage in using quantization correction, not particularly for short tau but for medium to long term stability starting with tau = 100s. Why UR8US didn't see any advantage, well, his requirements were for very short tau, well below 100s. This area is completely dominated by the oscillator.