Companion note, version 1.2

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

Version 1.1 left the smallest open instance of the conjecture, "is √((log 2)² + π²) algebraic?", untouched. It now has a partner.

New in this version

• If t² + π² is algebraic for a real logarithm t of an algebraic number, then e^{it²/π}, e^{π²/t} and e^{(t²+π²)/(iπ)} are transcendental. In particular, at least one of √((log 2)² + π²) and 2^{i log 2/π} is transcendental. The third number shows that the two open statements the development still depends on cannot fail at the same number.
• Two candidates of commensurable moduli supply the dimension that one candidate lacks, and the six exponentials theorem starts to work. The arguments of the candidates on a circle of algebraic radius form a Sidon set up to conjugation: the first constraint on families of candidates that are algebraically independent. And (−1)^{u/ū} is transcendental for every candidate.
• For a candidate, the harmonic mean of u and ū is not a logarithm of an algebraic number.
• At least one of e^{i/π} and e^{iπ³} is transcendental.
• At least one of 2^{log₃ 2} and 3^{log₂ 3} is transcendental.

None of this is new mathematics: each result is a short consequence of the six exponentials theorem, Gelfond–Schneider, or the four exponentials theorem in transcendence degree one.

Checks at release

• Appendix A: 55 identifiers, each checked against the platform by script, 0 mismatches.
• Library: 195 of 195 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. Earlier versions remain under note-v1.0 and note-v1.1.