Strong four exponentials implies that no algebraic multiple of $1/(i\pi)$ is a logarithm

The strong four exponentials conjecture implies DiazModulus.recip_pi_not_log: that no non-zero algebraic $\gamma$ has $\gamma/(i\pi)$ a logarithm of an algebraic number.

The configuration. Write $\lambda = \gamma/(i\pi)$ and suppose $e^{\lambda}$ is algebraic. Apply the strong four exponentials conjecture to

The four products are $1$, $i\pi$, $\lambda$, and $\lambda \cdot i\pi = \gamma$. All four lie in $\widetilde{\mathcal{L}}$: the first by definition; $i\pi$ because $e^{i\pi} = -1$ is algebraic; $\lambda$ by the assumption being contradicted; and $\gamma$ because it is algebraic, and $\widetilde{\mathcal{L}}$ is a $\overline{\mathbb{Q}}$-vector space containing $1$. That contradicts the conjecture, provided both rows are $\overline{\mathbb{Q}}$-linearly independent.

What supplies the independence, and it is not $\pi$-transcendence. Both $(1,\lambda)$ and $(1,i\pi)$ are independent as soon as $\lambda$ and $i\pi$ are transcendental, and Hermite–Lindemann alone gives both — no separate input on the transcendence of $\pi$ is needed. For $i\pi$: it is non-zero, and if it were algebraic then $e^{i\pi} = -1$ would be transcendental. For $\lambda$: it is non-zero since $\gamma \neq 0$, and if it were algebraic then $e^{\lambda}$ would be transcendental, against the assumption. Hermite–Lindemann is available on this mission as the Proved node DiazModulus.hermite_lindemann_holds, so it is discharged rather than carried, and the strong four exponentials conjecture is the only hypothesis this node retains.

What it is for. DiazModulus.recip_pi_not_log is open and two further open leaves of Diaz's modulus conjecture reduce to it. This node records exactly what strength would settle it, and pins that strength to a named conjecture rather than to a vague appeal. It does not make the parent easier: the strong four exponentials conjecture is open, and is itself the assumption the whole modulus conjecture currently rests on.