The square-root composition isnt the hard part here, the proof still leans on probability-one correctness and a deterministic Dec, so it sidesteps the exact CKKS case where the annoying bad events actually live. So calling this a verified noise-flooding result feels a bit too broad, its really a verified reduction for a cleaned-up model with the messy deployment bits left out.