Companion note, version 1.7

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

Twelve results from the reading of Diaz, Roy and Waldschmidt, now machine-checked.

Version 1.6 attributed several statements to the literature. Some of them, and a few consequences, are now proved on the platform and mirrored in the library:

• The homogeneous companion of Diaz's question: for a non-real logarithm λ algebraically dependent on its conjugate, e^{|λ|} is transcendental (Diaz 1997, Prop. 2; Roy–Waldschmidt 1997, Cor. 7.4). The same holds for exp √((log 2)² + π²) whenever log 2 and π are algebraically dependent.
• Waldschmidt's remark in LN 402 (1974, p. 202). For ℚ-independent logarithms ℓ₁, ℓ₂ that are algebraically dependent, e^{ℓ₁²/ℓ₂} and e^{ℓ₂²/ℓ₁} are transcendental. In particular 2^{i log 2/π} is transcendental as soon as log 2 and π are algebraically dependent.
• Waldschmidt's strong five exponentials conjecture (1988), his sharp four exponentials conjecture, and his 2×2 determinant conjecture (2005) each imply both Diaz's conjecture and (S). The first is item (2) of §7.

Two couplings are proved alongside and recorded in the library, not in the note:

• for a candidate u, e^{|u|²/x} is transcendental for every logarithm x algebraic over ℚ(u) outside ℚu ∪ ℚū;
• for every candidate algebraic over ℚ(π), the real half of (S) holds at γ = |u|².

Appendix A gains rows for the statements the note already made. No text changed otherwise.

Checks at release

• Appendix A: 79 identifiers checked against the platform by script, 0 mismatches.
• Library: 224 of 224 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 to note-v1.6.