Lean formalizations for the paper "Parity of k-differentials in genus zero and one"