Diaz's conjecture on the real and imaginary axes, given Hermite--Lindemann

The declaration has four explicit hypotheses and no typeclass assumptions. The first, $h_{HL}$, is an assumption of the bundle proposition HermiteLindemann, which unfolds to the full statement

so the result is conditional on that entire universally quantified proposition being available, and the declaration's name does disclose this dependence. The remaining data are a complex number $u$ together with:

• $h_u$: $u \neq 0$;
• $h_{ax}$: $\Im(u) = 0$ or $\Re(u) = 0$ — that is, $u$ lies on the real axis or on the imaginary axis (the two cases overlap only at $u = 0$, which $h_u$ excludes);
• $h_{mod}$: the number $\lVert u \rVert = \sqrt{(\Re u)^2 + (\Im u)^2}$, a nonnegative real, coerced into $\mathbb{C}$, is algebraic over $\mathbb{Q}$ — equivalently, $|u|$ is an algebraic real number. (The coercion is the only $\mathbb{R} \to \mathbb{C}$ cast in the statement; algebraicity of the coerced value over $\mathbb{Q}$ is the same condition as algebraicity of the real $|u|$.)

The conclusion is that $e^{u}$ is transcendental over $\mathbb{Q}$, i.e. a root of no nonzero rational polynomial.

Two structural points about the hypothesis set. First, $h_u$ is load-bearing: at $u = 0$ one has $\lVert u\rVert = 0$ algebraic and $e^0 = 1$ algebraic, so the statement would be false without it. Second, $h_{ax}$ and $h_{mod}$ combine: if $\Im u = 0$ then $\lVert u\rVert = |\Re u|$, so $h_{mod}$ makes $\Re u$ algebraic and hence $u = \Re u$ is an algebraic complex number; if $\Re u = 0$ then $\lVert u \rVert = |\Im u|$, so $\Im u$ is algebraic and $u = i\,\Im u$ is again algebraic, $i$ being algebraic. The two hypotheses therefore jointly say exactly: $u$ is a nonzero algebraic number lying on one of the two coordinate axes, and the conclusion is then the instance of $h_{HL}$ at $a := u$.

The statement contains no reference to DiazModulusConjecture, IsCandidate, $\mathcal{L}$, $\tilde{\mathcal{L}}$, $\overline{\mathbb{Q}}$, or any other bundle definition apart from HermiteLindemann; it makes no claim about any $u$ off the axes, and no claim about complex $u$ whose modulus is algebraic while $u$ itself is not.

Discrepancies:

1. The name presents the result as the restriction of Diaz's modulus conjecture to the coordinate axes, obtained from Hermite–Lindemann. The code's hypotheses, however, do not merely restrict the conjecture's domain — on either axis "$\lVert u \rVert$ algebraic" is equivalent to "$u$ algebraic", so the region covered is precisely the set of nonzero algebraic points of the two axes. Every such $u$ is already a direct instance of the assumed $h_{HL}$; the modulus hypothesis contributes nothing beyond establishing algebraicity of $u$ itself, and the statement covers no $u$ to which $h_{HL}$ does not already apply verbatim. The distinguishing content of the modulus conjecture as stated in the bundle — quantification over all nonzero $u$ with algebraic modulus, including transcendental $u$ — is absent from this restricted form.
2. The conditional hypothesis $h_{HL}$ is an assumption on HermiteLindemann, which the bundle's own doc-comment describes as a classical theorem (Hermite 1873, Lindemann 1882) that is merely absent from the platform's Mathlib rather than an open proposition; the sibling declaration DiazModulus.hermite_lindemann_holds asserts it unconditionally. So the "_of_hermite_lindemann" qualifier signals a dependency on a classically established statement, not on an unproved conjecture.