Minimal Hamming distance of SHA512 hashes at bit flip For $n\in\mathbb{N}$ let $\{0,1\}^n$ denote the set of $\{0,1\}$-vectors of length $n$. Let $\{0,1\}^* = \bigcup_{n\in\mathbb{N}}\{0,1\}^n$ denote the collection of all finite-length $\{0,1\}$-strings.
If $x,y\in \{0,1\}^n$ for some $n\in\mathbb{N}$, we let $$d_H(x,y) = \big|\big\{ i\in \{0,\ldots,n-1\}:x_i \neq y_i\big\}\big| \;\;\in \{0,\ldots,n\}$$
denote the Hamming distance between $x, y$.
Let $h:\{0,1\}^* \to \{0,1\}^{512}$ denote the cryptological hash function ${\sf SHA512}$.
Question. Is it known whether $$m_0 = \min\{d_H(h(x),h(y)): (\exists n\in\mathbb{N}(x,y\in \{0,1\}^n)) \land (d_H(x,y)=1)\}$$
is positive? Is a lower bound $\geq 2$ for $m_0$ known?
We strongly hope that $m_0=0$ as we wish for the SHA512 compression function to perform as a random oracle. Thus for example, if we were to pick a $2^{521}$ long string $s$ there are $2^{521}$ other strings whose Hamming distance from $s$ is 1. The coupon collecting estimate would return all possible outputs with high probability, including the value that matches $\mathrm{SHA512}(s)$. Thus for any fixed, really long string we hope that there is one bit that you can flip that doesn't change the final value.
We strongly hope not to be able to constructively demonstrate that $m_0=0$ as this would be an example of a hash collision. To demonstrate that $m_0=0$ non-constructively seems to require more mathematical structure than is provided in its design.
Interestingly, the related value
$$m_1=\mathrm{min}\{d_H(h(x),h(y)):(\exists n\in\mathbb N,(x,y\in \{0,1\}^n))\wedge (d_H(x,y)=2)\}$$
can be shown to be zero by the pigeon hole principle. We pick a string of length $2^{512}+1$ and compute the hashes of its one-bit flips. Two of these must match and are a pair of strings with Hamming distance 2.

ETA: @poncho points out that SHA512 is limited to inputs of length at most $2^{128}-1$(!) and so these long string arguments do not apply to the standard version of SHA512, only the abstraction of the question. For the probabilistic argument with the standardised version, then instead we consider all strings of length 522 and fix some bit position these provide $2^{521}$ pairs that differ in that bit position and whose differences should be statistically independent. We should anticipate a full set of differences including 0.
Although the pigeonhole principle no longer delivers $m_1$ it does deliver an upper bound of 10 flips of input to produce matching output. We consider a string of length $2^{127}$ and the set of inputs produced by 5 flips. There are more than $2^{512}+1$ of these and so again by pigeonhole there must be two with the same value. The Hamming distance between this pair is at most 10 by the triangle inequality applied to the Hamming metric.