Companion note, version 1.1

The Diaz modulus conjecture: a machine-checked spine and the shape of its obstruction, version 1.1.

Version 1.0 said that every branch of the conjecture is closed or reduced to one of three open statements. There are two:

1. for real algebraic γ ≠ 0, e^{−iγ/π} is transcendental (the real half of the statement (S));
2. the transcendence of |u| for a generic conjugate pair of logarithms, which is equivalent to the conjecture itself.

The third statement in version 1.0, the imaginary half of (S), is no longer needed. Both branches that reach (S) produce a real γ, and two new machine-checked reductions record this. The imaginary half stays open, and the two halves cannot both fail.

New in this version

• By Gelfond–Schneider, the exceptions to (S) form at most one rational line, lying on an axis. Hence at least one of its two halves holds, and at least one of π log 2 and π log 3 is transcendental.
• Two logarithms with rationally related moduli in transcendence degree one are rational multiples of each other or of each other's conjugate. For a hypothetical candidate u this makes e^{u²/|u|}, and more generally e^{c u^k}, transcendental: the unconditional part of an exclusion that previously needed Roy's strong six exponentials theorem.
• Geometric triples w, wz, wz² are not all logarithms in transcendence degree one. Hence at least one of e^{π²} and e^{iπ³} is transcendental.
• The six exponentials theorem, where it has room: at least one of 2^π, 3^π, 5^π is transcendental.
• Bibliography corrected. Diaz's "Utilisation de la conjugaison complexe…" is J. Théor. Nombres Bordeaux 16 (2004), 535–553. His 2007 paper is listed separately.

None of this is new mathematics. Each result is a short consequence of Gelfond–Schneider, of the four exponentials theorem in transcendence degree one (Brownawell 1974; Waldschmidt 1973), or of the six exponentials theorem.

Checks at release

• Appendix A: 42 identifiers, each checked against the platform by script, 0 mismatches.
• Library: 182 of 182 proved results mirrored; lake build Diaz is clean; the only axioms are propext, Classical.choice and Quot.sound.

The PDF attached here is built from tex/diaz_prove2me.tex at this tag. Version 1.0 remains available under note-v1.0.