Companion note, version 1.4

Correction (24 September 2026). This release says that no proved theorem is known to exclude a candidate carrying an anisotropic relation such as Re(u²) = π². That is wrong. Théorème 0.2 of D. Roy and M. Waldschmidt (Ann. Sci. École Norm. Sup. 30, 1997) excludes every rational quadratic relation among u, ū, iπ for a candidate algebraic over ℚ(π) with Im u ∉ ℚπ, so no such candidate carries one. The formal results of this version are unaffected; version 1.5 of the note corrects the text.

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

Version 1.3 left three statements about the four exponentials barrier proved on paper only. Version 1.4 has all three machine-checked, and the section that stated them informally now states them as numbered results.

New in this version

• The period never enters (Theorem 5.6). For u algebraically independent of π, the only quadratic relation with algebraic coefficients among 1, u, ū, iπ is the norm X₁X₂ − ρX₀². A singular 2×2 matrix over Q̄ + Q̄u + Q̄ū + Q̄iπ with independent rows and columns has no iπ in any entry. The configurations that could detect a candidate use the constant term, u and ū, and nothing else.
• The relations a non-generic candidate can carry (Proposition 5.7). For u off the axes with Im u ∉ ℚπ they are exactly the identities Q(Im u, π) = s|u|². A relation whose form has no rational zero, such as Re(u²) = π², never produces a four exponentials configuration: the determinant of a 2×2 matrix of rational linear forms always has one. Such relations occur on every circle of algebraic radius greater than π. No proved theorem is known to exclude a candidate carrying one.
• Indistinguishability with π fixed (Theorem 5.2). With K the algebraic closure of ℚ(π), a point transcendental over K cannot be told from a non-candidate point of its circle by any vanishing statement with coefficients in K. The non-candidate is found by countability, which is now formal too.
• The abstract gains one sentence for this.

None of this is new mathematics. Each result is elementary, or a short consequence of the transcendence of π and the Steinitz extension lemma.

Checks at release

• Appendix A: every identifier checked against the platform by script, 0 mismatches.
• Library: 210 of 210 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.3.