A clean proof of the cleaning lemma

The Cleaning Lemma is an important property of stabilizer quantum codes. It states that for any region $R$ where no logical operator is supported, any logical operator passing through $R$ can be “cleaned” (or moved) outside the region. Conventional proofs of this lemma rely on dimension counting. In this note, we present a stronger lemma that reveals a more fundamental algebraic structure underlying the Cleaning Lemma. See the PDF version for the full note.