Removable singularity for bounded harmonic functions under Countable Choice

Translate $p=0$ and choose $0<R<1$ so that ${\bar{B}}_R\subset \mathrm{\Omega }$. Under the given Countable Choice premise, ball mean values and the smoothness theorem make $u$ smooth on the punctured domain; its trace on $\mathrm{\partial }{B}_R$ is smooth. Let $h$ be its harmonic replacement on $B_R$, and $w=u-h$. Then $w$ is harmonic off zero and vanishes on the outer sphere. The replacement is bounded on the closed ball.

For $0<\delta <R$, put $A_{\delta }={\max }_{\mathrm{\mid }x\mathrm{\mid }=\delta }\mathrm{\mid }w(x)\mathrm{\mid }$, a finite nonnegative number. On $\delta <r=\mathrm{\mid }x\mathrm{\mid }<R$ take ${\varphi }_{\delta }(x)=A_{\delta }(\delta \mathrm{/}r{)}^{n-2}$ if $n\ge 3$, and ${\varphi }_{\delta }(x)=A_{\delta }\log (R\mathrm{/}r)\mathrm{/}\log (R\mathrm{/}\delta )$ if $n=2$. For radial $f$, differentiation of ${\mathrm{\partial }}_{i}f(r)=f\mathrm{\prime }(r)x_i\mathrm{/}r$ gives $\mathrm{\Delta }f=f\mathrm{\prime }\mathrm{\prime }+(n-1)f\mathrm{\prime }\mathrm{/}r$. Substitution proves $\mathrm{\Delta }{\varphi }_{\delta }=0$ in both dimensions. Each barrier equals $A_{\delta }$ on the inner sphere and is nonnegative on the outer sphere.

Comparison on the bounded annulus applied separately to $w$ and $-w$ against ${\varphi }_{\delta }$ yields $\mathrm{\mid }w(x)\mathrm{\mid }\le {\varphi }_{\delta }(x)$. In the bounded case $A_{\delta }$ remains uniformly bounded for small $\delta$. At fixed $x\mathrm{\ne }0$, the factor ${\delta }^{n-2}$ tends to zero for $n\ge 3$, and the denominator $\log (R\mathrm{/}\delta )$ tends to infinity for $n=2$. Thus $w(x)=0$.

Under the stated little-o hypotheses, $A_{\delta }=o({\delta }^{2-n})$ or $A_{\delta }=o(\log (1\mathrm{/}\delta ))$, because $h$ is bounded. The same barrier bound again tends to zero at each fixed nonzero $x$. Hence $u=h$ on the punctured ball in either case. Define $u(0)=h(0)$ and retain the original $u$ outside the ball; equality on their overlap proves harmonicity locally everywhere. Any continuous extension must have this value at zero, proving uniqueness.