The independence upgrade at the Diaz-locus quadric

Source. The hypothesis hIU is the Lemma Independence upgrade, statement 37 of C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026, the predecessor manuscript of Carlo Perassi's note on Diaz's modulus conjecture. That manuscript states explicitly that the lemma is not its own: "it is stated explicitly in [Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, p. 593], immediately after Theorem 15.30", in the form that $\mathbb Q$-linearly independent elements of $\mathcal L$ generating a field of transcendence degree one satisfy $Q(\lambda_1,\dots,\lambda_n)\ne0$ for every non-zero homogeneous rational $Q$ of degree two. In the manuscript it is derived from Roy and Waldschmidt's Théorème 0.2.

The cited lemma, as carried. Let $\lambda_1,\dots,\lambda_n\in\mathcal L$ be linearly independent over $\mathbb Q$ and let $P\in\mathbb Q[X_1,\dots,X_n]$ be a non-zero homogeneous polynomial of degree at most two with $P(\lambda_1,\dots,\lambda_n)=0$. Then $\operatorname{trdeg}_{\mathbb Q}\mathbb Q(\lambda_1,\dots,\lambda_n)\ge2$.

This statement was transcribed from C. Perassi, Rigidity of logarithms with algebraic modulus — Around a conjecture of Diaz, unpublished manuscript, 15 August 2026 and has not been verified against its original (Waldschmidt's book, or the Roy–Waldschmidt paper); neither source is held on this mission. It is carried as the explicit hypothesis hIU rather than asserted. The node asserts only the consequence below.

The consequence. Let $K\subset\mathbb C$ be a subfield and let $u,v$ be such that $u,\overline u,v,\overline v$ are all logarithms of elements of $K$, with squared moduli rationally commensurable,

and with $u,\overline u,v,\overline v$ linearly independent over $\mathbb Q$. Then

This is the manuscript's own reading of the lemma on the Diaz locus: two Diaz candidates with rational squared-modulus ratio have a $\mathbb Q$-linearly independent conjugate quadruple (that independence is the mission's Diaz.indep_quadruple) lying on the rational quadric $mX_1X_2-X_3X_4=0$, so the lemma applies at full strength.

What is verified. The instantiation itself: that $P=mX_1X_2-X_3X_4$ is a non-zero homogeneous polynomial of degree two over $\mathbb Q$ (non-zero because its value at $(1,1,0,0)$ is $m\ne0$), that it vanishes at the quadruple exactly when $v\overline v=m\,u\overline u$, and that the $\mathbb Q$-linear independence hypothesis of the lemma is the one supplied. Everything deeper sits inside hIU.

Formalization note. The lemma is carried over Fin n with MvPolynomial (Fin n) ℚ, MvPolynomial.IsHomogeneous, and evaluation by MvPolynomial.aeval; transcendence degree is Algebra.trdeg ℚ of Algebra.adjoin ℚ of the relevant set. #print axioms on the submitted proof: [propext, Classical.choice, Quot.sound].