Algebraic squared distance forces an algebraic ratio

Let $K \subseteq \mathbb{C}$ be a subfield and let $u, v \in \mathbb{C}$ with $v \neq 0$. If the three squared moduli

all lie in $K$, then $u/v$ is algebraic over $K$.

Where this sits. This is the first half of the proof of Theorem 2.1 (thm:distance-plane, Algebraic-distance and plane rigidity) of the manuscript, the implication

for $u,v$ in the Diaz candidate locus, stated over an arbitrary base field because that is all the argument uses.

Proof. Put $z = u\bar v$. The two identities

place both coefficients of $X^2 - (z+\bar z)X + z\bar z$ in $K$, so $z$ is a root of a monic quadratic over $K$. Dividing that quadratic by $(v\bar v)^2$ turns it into a monic quadratic satisfied by $u/v = z/(v\bar v)$. The Lean writes down that quadratic directly and checks it is non-zero by reading its coefficient in degree two.

What is deliberately not claimed. The manuscript's theorem concludes $v/u \in \mathbb{Q}^{\times}$, not merely algebraicity. That last step is the Gelfond–Schneider quotient dichotomy for two non-zero logarithms, which is not available in this Mathlib revision and is not asserted here. Specialising $K = \bar{\mathbb{Q}}$ recovers exactly the algebraic-ratio conclusion of the manuscript's first paragraph.

The converse direction of the manuscript's equivalence is the trivial computation $|u - au| = |1-a|\,|u|$ and is not published.

Possibly known; not checked against the literature.

Source. Carlo Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz (private manuscript, 15 August 2026). The mathematics is his; this node only records one step of it in Lean, and claims no novelty of its own.