Companion note, stable version 1.0

The Diaz modulus conjecture: a machine-checked spine and the shape of its obstruction — stable version 1.0.

This is the companion note to the library in this repository, fixed at the point where the formal case analysis ends. Every branch of Diaz's conjecture is either closed by a machine-checked proof or reduced, by a machine-checked reduction, to one of three statements, and the note names them:

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

All three follow from the strong four exponentials conjecture. None of them is a formalisation problem.

What is in this version

• The spine: strong four exponentials settles the conjecture by one instantiation; on the irrational-angle branch, the statement (S) settles the case where the fibre carries a second point of algebraic modulus; its counterexamples cannot be roots of unity.
• The obstruction: matrix-of-logarithms arguments fail on one branch, a second branch returns to its start, and the natural interpolation route is blocked — no first-order arithmetic operator on the lattice, and an interpolation determinant that factors as a Kronecker product blind to the candidate's arithmetic.
• The four exponentials theorem in transcendence degree one (Brownawell; Waldschmidt), now formalised along Waldschmidt's 1973 and 1971 route, and the precise reason it cannot reach the three open statements.

Checks at release

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

The PDF attached here is built from tex/diaz_prove2me.tex at this tag.