Solution (source code)

= Solution

For an infinite <cardinal number> $\kappa$, its <cofinality> is
$$
\operatorname{cf}(\kappa)=\min\{|A|:A\subseteq\kappa,\ \sup A=\kappa\},
$$
viewing $\kappa$ as an <initial ordinal>. Equivalently it is the smallest <cardinal number> which is the domain size of a <cofinal map> into $\kappa$.

Put $\lambda=2^\kappa$ and $\mu=\operatorname{cf}(\lambda)$. Suppose $\mu\leq\kappa$, and choose cofinal <ordinals> $\alpha_i<\lambda$ for $i<\mu$. Put $a_i=|\alpha_i|<\lambda$. Their union is $\lambda$, so <infinite cardinal arithmetic> gives
$$
\lambda\leq\sum_{i<\mu}a_i\leq\lambda\mu=\lambda.
$$
Apply the <König theorem for cardinal numbers> to $a_i<a_i^+$. Each <successor cardinal> $a_i^+$ is at most $\lambda$, whence
$$
\lambda=\sum_{i<\mu}a_i<\prod_{i<\mu}a_i^+\leq\lambda^\mu\leq(2^\kappa)^\kappa=2^{\kappa\cdot\kappa}=2^\kappa=\lambda.
$$
Here the last equalities use the <currying law for cardinal exponentiation> and <square of an infinite cardinal>. This contradiction proves the <cofinality of a power-set cardinal> bound
$$
\boxed{\operatorname{cf}(2^\kappa)>\kappa.}
$$