Strong four exponentials implies Diaz's modulus conjecture

The strong four exponentials conjecture settles Diaz's modulus conjecture outright, by a single instantiation.

The argument. Let $u \neq 0$ with $\lVert u\rVert$ algebraic, and suppose $e^{u}$ were algebraic. If $u$ itself is algebraic, Hermite–Lindemann already gives a contradiction. Otherwise $u$ is transcendental, and so is $\overline{u}$, so both $(1, u)$ and $(1, \overline{u})$ are $\overline{\mathbb{Q}}$-linearly independent. Apply the strong four exponentials conjecture to

The four products are $1$, $\overline{u}$, $u$ and $u\overline{u} = \lVert u\rVert^{2}$. The first lies in $\widetilde{\mathcal{L}}$ by definition; $u$ and $\overline{u}$ lie in it because $e^{u}$ and $e^{\overline{u}} = \overline{e^{u}}$ are algebraic; and $\lVert u\rVert^{2}$ is algebraic, hence in $\overline{\mathbb{Q}} \cdot 1 \subseteq \widetilde{\mathcal{L}}$. That contradicts the conjecture.

Hermite–Lindemann is discharged from the Proved node DiazModulus.hermite_lindemann_holds, so the strong four exponentials conjecture is the only surviving hypothesis.

What this says about the rest of the mission, stated plainly. This mission carries a large decomposition of its root — several generations of case splits, a polar normal form, four-exponentials matrix machinery — and every open leaf of that tree is implied by the strong four exponentials conjecture. This node shows the same conjecture reaches the root directly, without any of it. So the tree should not be read as having reduced a hard problem to easier ones.

What the tree did do, and this is the part worth keeping, is isolate hypotheses strictly weaker than the strong four exponentials conjecture that still suffice. DiazModulus.recip_pi_not_log is one: it follows from the strong four exponentials conjecture and is not known to imply it, and two open leaves reduce to it. Weaker sufficient conditions are the honest description of what a decomposition of this kind produces, and they are what a reader should look for here rather than a ladder of progressively easier problems.

Not claimed. No converse. The strong four exponentials conjecture is open — it is the strengthening of the four exponentials conjecture in which linear independence is taken over $\overline{\mathbb{Q}}$ rather than $\mathbb{Q}$ — and nothing here makes it more tractable. This node closes nothing.