Companion note, version 1.5

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

A correction, and two more barrier results.

Correction

Version 1.4 said that a relation such as Re(u²) = π² is excluded by nothing the note knows of. That was wrong, and it contradicted the note's own boundary section. Théorème 0.2 of Roy and Waldschmidt (Ann. Sci. École Norm. Sup. 30, 1997), the quadric version of the four exponentials theorem in transcendence degree one, excludes every rational quadratic relation among u, ū, iπ for a candidate algebraic over ℚ(π) with Im u ∉ ℚπ. Proposition 5.7 and the text after it now say so. No formal statement was affected. The node texts on the platform that repeated the claim have been corrected.

New in this version

• Theorem 5.4(c): with algebraic coefficients but no constant term, a generic candidate's logarithms still hold no 2×2 configuration.
• Theorem 5.6(c): no 2×3 configuration lies over Q̄ + Q̄u + Q̄ū + Q̄iπ. So Roy's strong six exponentials theorem gives nothing against a generic candidate, even with iπ added.
• The boundary section cites Roy–Waldschmidt's Corollaire 7.4, the homogeneous companion of the smallest open instance: if log 2 and π were algebraically dependent, exp √((log 2)² + π²) would be transcendental.

Checks at release

• Appendix A: 72 identifiers checked against the platform by script, 0 mismatches.
• Library: 212 of 212 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.4.