Assuming choice, normality is not productive: the normal lower-limit line has a nonnormal square

Given: The Axiom of Choice and the lower-limit line $L$.

The Axiom of Choice supplies a choice function for every family of nonempty sets, hence for every countably indexed family, which is the Axiom of Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ($\mathrm{AC}_\omega$)).

Under the Axiom of Countable Choice, the lower-limit line is normal (Assuming countable choice, the lower-limit line is normal).

Jones's lemma injects $\mathcal P(D)$ into $\mathcal P(E)$ when a normal space has closed discrete $D$ and dense $E$ (Jones's bound: under choice, a closed discrete subspace of a normal space cannot have more subsets than a dense set has subsets).

The plane $L^2$ has $E=\mathbb Q^2$ at most countable and $D=\{(x,-x):x\in\mathbb R\}$ closed discrete with $D\approx\mathbb R$ (The lower-limit plane has a countable dense set and a closed discrete antidiagonal of size $|\mathbb{R}|$).

Cantor's theorem gives no injection $\mathcal P(\mathcal P(\mathbb N))\to\mathcal P(\mathbb N)$, and Schröder-Bernstein turns injections both ways into a bijection (Assuming the Axiom of Choice, $2^{\kappa} = \lvert \mathcal{P}(\kappa) \rvert$, and Cantor's theorem in cardinal form: $\kappa < 2^{\kappa}$, The Schröder-Bernstein theorem).

The ternary Cantor-set coding injects $\mathcal P(\mathbb N)$ into $\mathbb R$, while $x\mapsto\{q\in\mathbb Q:q<x\}$ injects $\mathbb R$ into $\mathcal P(\mathbb Q)$; a rational between distinct reals makes the latter map injective, and $\mathbb Q\approx\mathbb N$ (The Cantor set is exactly the set of $\sum_{k \ge 1} a_k 3^{-k}$ with every $a_k \in \{0,2\}$, and this gives a bijection with $\{0,1\}^{\mathbb{N}}$, ℚ is dense in every Archimedean ordered field, $\mathbb{Q}$ is countably infinite).