On Ishiki's Conjecture: $\mathrm{M}\mathrm{e}\mathrm{t}(D)$ Is Not Completely Metrizable for $\mid D\mid ={\mathrm{\aleph }}_1$

For a discrete topological space $D$, let $\mathrm{M}\mathrm{e}\mathrm{t}(D)$ denote the set of metrics on $D$ that are compatible with the discrete topology, equipped with the topology induced by the supremum distance. Ishiki’s Conjecture 5.1 asserts that $\mathrm{M}\mathrm{e}\mathrm{t}(D)$ is not completely metrizable when $\mid D\mid ={\mathrm{\aleph }}_1$. We prove this in ZFC by constructing a set $A\subseteq [0,1]$ of cardinality ${\mathrm{\aleph }}_1$ that is not $F_{\sigma }$ and embedding its complement as a closed subspace of $\mathrm{M}\mathrm{e}\mathrm{t}(D)$. The proof has also been formalised in Lean 4.