Compact sets of positive area are not conformally removable

Let $E:=K\cap \mathbb{C}$. By [F1], $E$ is Borel in the finite chart, and [F2] makes it Lebesgue measurable. The Countable Choice assumption of the Borel/Lebesgue interface follows from AC by [F8].

Define the finite-chart function ${\mu }_0(z)=\frac{1}{2}$ for $z\in E$ and ${\mu }_0(z)=0$ for $z\mathrm{\notin }E$. By [F2] it is measurable. Since ${\lambda }_2(E)>0$, its essential supremum is exactly $\mathrm{\parallel }{\mu }_0{\mathrm{\parallel }}_{\mathrm{\infty }}=\frac{1}{2}$: the pointwise bound gives at most $\frac{1}{2}$, while for every $t<\frac{1}{2}$ the set $\{\mathrm{\mid }{\mu }_0\mathrm{\mid }>t\}$ contains $E$ and has positive measure. The sphere-chart rule [F3] therefore defines a Beltrami coefficient $\mu$ with $\mathrm{\parallel }\mu {\mathrm{\parallel }}_{\mathrm{\infty }}=\frac{1}{2}<1$.

Apply the existence clause of [F4] with $k=\frac{1}{2}$. It gives an orientation-preserving sphere homeomorphism $F$ that is a weak solution for $\mu$ and has Beltrami coefficient ${\mu }_F=\mu$ almost everywhere.

On every local chart in $\widehat{\mathbb{C}}\setminus K$, the coefficient $\mu$ is zero almost everywhere because its finite-chart support is $E\subseteq K$ and the transition rule preserves zero. Hence the weak Beltrami equation from [F4] gives $F_{\bar{z}}=0$ almost everywhere there. The local coordinate maps belong to $W_{\mathrm{l}\mathrm{o}\mathrm{c}}^{1,2}$ by [F4], so [F5] makes them conformal. The Countable Choice assumptions of these measurable and weak-solution interfaces follow from AC by [F8]. Thus $F$ is conformal on $\widehat{\mathbb{C}}\setminus K$.

If $F$ were Möbius, [F6] would give ${\mu }_F=0$ almost everywhere. This contradicts ${\mu }_F=\mu =\frac{1}{2}$ on the positive-area set $E$ by step 2.1. Therefore $F$ is not Möbius, and [F7] says $K$ is not globally conformally removable. The same argument for any compact $K$ of positive area proves that every globally conformally removable compact set has zero area. The normalized measurable-Riemann-mapping and measure interfaces use the choice assumptions recorded in [F8].