Planar logarithm factorization (source code)

= Planar logarithm factorization
{title2=$C(K,\mathbb C^*)=\exp C(K)\times\langle z-a_U:U\text{ bounded complementary component}\rangle$}

Choose $a_U$ in each bounded component of $\mathbb C\setminus K$. Every nonvanishing <continuous function> on $K$ extends nonvanishingly to a neighborhood. Use <finite-hole neighborhoods of a planar compact set> within that neighborhood, and subtract its finite list of winding obstructions by multiplying by $\prod(z-a_U)^{-k_U}$. The <continuous logarithm lifting criterion> gives the remaining exponential. Uniqueness follows by extending a purported logarithm of such a finite product to a smaller neighborhood: a small multiplicative error has a local logarithm, whereas its winding around the $U$th hole is $k_U$. Thus all $k_U$ vanish. The quotient by exponentials is the <free abelian group> on the bounded complementary components; each element has finite support.