Non-real two-point fibres force $e^{\pi^2}$ transcendental

Source. This is Carlo Perassi's mathematics, from his unpublished note on Diaz's modulus conjecture, section Polar coordinates and the discreteness of the period, statement Theorem (Non-real two-point fibres force $e^{\pi^2}$ transcendental). Published on his mission with his permission. No novelty is claimed for it; the composition is elementary once its inputs are in place, and it is possibly known — it has not been checked against the literature.

Statement. Write $\overline{\mathbb Q}$ for the algebraic numbers, $\mathcal L=\{\ell\in\mathbb C:\exp\ell\in\overline{\mathbb Q}\}$, and

for the augmented logarithm space, the $\overline{\mathbb Q}$-vector space generated by $1$ and $\mathcal L$. For $\alpha\in\overline{\mathbb Q}^\times$ put

If $E_\alpha$ contains two distinct points and $\alpha\notin\mathbb R$, then

By the two-point algebraic-fibre bound (on this mission as Diaz.fibre_at_most_two) one always has $\#E_\alpha\le2$, so "contains two distinct points" is the manuscript's hypothesis $\#E_\alpha=2$.

What this does and does not assert. It does not assert that $e^{\pi^2}$ is transcendental. It is a conditional statement, on two counts, and both are visible inside the Lean statement.

1. The Diaz hypothesis. A point of $E_\alpha$ is a Diaz candidate: a counterexample to Diaz's conjecture $C(|u|)$, which the whole mission is about. No such point is known to exist. The theorem says that a non-real two-point fibre — the sharpest configuration a hypothetical failure of $C(|u|)$ could take — would settle $e^{\pi^2}$ outright.

2. The one carried citation. The hypothesis hSSE is D. Roy's strong six exponentials theorem, in the "Version 3" form stated by Diaz as Théorème 3, point 3, p. 379 of Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques, J. Théor. Nombres Bordeaux 19 (2007), 373–391 (original: D. Roy, Matrices whose coefficients are linear forms in logarithms, J. Number Theory 41 (1992), Corollary 2; also Waldschmidt, Diophantine Approximation on Linear Algebraic Groups, Corollary 11.16). Roy's theorem is proved mathematics, but it has no Mathlib formalisation at this revision, so it is carried as an explicit hypothesis rather than asserted. It is the only unformalised input: everything else the proof uses is already Proved on the platform.

Inputs used, all from the platform. The proof imports and uses three published nodes:

• Diaz.diaz_2007_cor2_P1 — Diaz's Corollaire 2 (P)(1) of 2007, itself stated over the carried hSSE;
• Diaz.indep_of_algebraic_product — the independence step of the manuscript's own proof;
• DiazModulus.pi_transcendental — Lindemann's theorem, from which the transcendence of $i\pi$ over $\overline{\mathbb Q}$ is obtained via Transcendental.algebraicClosure.

The argument. Two points of $E_\alpha$ differ by $2\pi i n$ with $n\in\mathbb Z\setminus\{0\}$. Writing $\theta=\operatorname{Im}u$, the identity

and the algebraicity of both moduli give $\pi(\theta+\pi n)\in\overline{\mathbb Q}$. Put $\nu:=i(\theta+\pi n)$, so that $\beta:=(i\pi)\nu=-\pi(\theta+\pi n)\in\overline{\mathbb Q}$. If $\nu=0$ then $\theta\in\pi\mathbb Z$ and $\alpha$ would be real, which is excluded; so $\beta\ne0$. Also $\nu\in\mathcal L$: $e^{i\theta}$ squares to $\alpha/\overline\alpha\in\overline{\mathbb Q}$, and $e^{i\pi n}=(-1)^n$. Since $i\pi$ is transcendental over $\overline{\mathbb Q}$ and $(i\pi)\nu\in\overline{\mathbb Q}^\times$, the triple $1,\nu,i\pi$ is $\overline{\mathbb Q}$-linearly independent. Diaz's Corollaire 2 (P)(1) applied to $(\lambda_1,\lambda_2,\lambda_3)=(i\pi,\nu,i\pi)$ gives $\{(i\pi)\nu,(i\pi)^2\}\not\subset\widetilde{\mathcal L}$; as $(i\pi)\nu\in\overline{\mathbb Q}\subset\widetilde{\mathcal L}$, one gets $(i\pi)^2=-\pi^2\notin\widetilde{\mathcal L}$, hence $\pi^2\notin\widetilde{\mathcal L}$ because $\widetilde{\mathcal L}$ is a $\overline{\mathbb Q}$-vector space. Finally $e^{\pi^2}$ algebraic would put $\pi^2$ in $\mathcal L\subset\widetilde{\mathcal L}$.

Formalization note. The algebraic numbers are the mission's Diaz.Qbar. As the mission carries no Definition node for $\widetilde{\mathcal L}$, the space is inlined: aLog is required to equal Submodule.span ↥Diaz.Qbar (insert 1 {l | Complex.exp l ∈ Diaz.Qbar}). The condition $|u|\in\overline{\mathbb Q}$ is written u * conj u ∈ Diaz.Qbar, the form used throughout the mission for the Diaz locus, and equivalent to it since $\overline{\mathbb Q}$ is closed under square roots. "$\alpha\notin\mathbb R$" is α.im ≠ 0. The conclusion Transcendental ℚ (Complex.exp ((Real.pi : ℂ) ^ 2)) is the transcendence of $e^{\pi^2}$, since $(\pi:\mathbb C)^2$ is the real number $\pi^2$ viewed in $\mathbb C$.