Transcendence theory in Lean 4

This library proves classical theorems of transcendental number theory in Lean 4 with Mathlib, and applies them to one open problem: Diaz's conjecture that a non-zero logarithm of an algebraic number never has algebraic modulus.

It began as a study of that conjecture. Most of it is now the theory itself: the auxiliary-function method of Gel'fond and Schneider, Siegel's lemma and Liouville's inequality, a Schwarz lemma for Cartesian products, zero counts for exponential polynomials, and the theorems they prove. All 684 results build in CI and depend only on Lean's three standard axioms (propext, Classical.choice, Quot.sound).

The proofs are engineered as well as checked: cut into small results that later proofs import, with shared tools stated for general use, and with the size of every proof kept down. See "Proof engineering".

No new transcendence theorem is claimed. The library does have results of its own: chapter 14 of the blueprint lists those not found in the sources read and ranks the ones that are not routine. Not found is not a claim that they are new. The classical results are attributed below, and so are the Lean proofs written by others. The results about Diaz's conjecture are mostly negative: they show which methods cannot settle it.

The classical theorems

The blueprint at https://carlok.github.io/diaz-modulus-lean/ states each of them, and every result their proofs use, with a dependency graph, links to the Lean source and a PDF. Since October 2026 it also has chapters of the library's own results: the rank-one configurations near a point of a circle (Theorems A and B below, the power and Laurent hulls, separation, and the five-dimensional spaces, with the progression spaces classified and configurations up to degree two), the dichotomy for Li₂(1/2), quadratic relations near a point of a circle, and consequences in transcendence degree one, with results from the author's unpublished manuscript and reductions under Kirby's weak Schanuel conjecture. Its chapter "Results not found in the sources read" lists the blueprint's results not found in the literature checked and ranks those that are not routine; in the dependency graph they have a double border.

Result	Due to	Lean name	Lean proof
a non-zero logarithm of an algebraic number is transcendental	Hermite 1873, Lindemann 1882	Diaz.hermite_lindemann	derived here from the next row
e^{α₁}, …, e^{αₙ} are linearly independent over Q̄ for distinct algebraic αᵢ	Lindemann 1882, Weierstrass 1885	linearIndependent_exp, algebraicIndependent_exp	ported from Mathlib PR #28013 (unmerged)
e^{bℓ} is transcendental for algebraic irrational b and a non-zero logarithm ℓ	Gel'fond 1934, Schneider 1934	GelfondSchneider.gelfond_schneider	restructured from M. Karatarakis and F. Wiedijk
e^π is transcendental	Gel'fond 1929	Diaz.e_pi_transcendence	this project (the node was posed by another Prove2Me contributor)
the six exponentials theorem	Lang 1965–66, Ramachandra 1968	Diaz.six_exponentials	this project
Roy's strong six exponentials theorem: for x₁, x₂ and y₁, y₂, y₃ free over Q̄, some xᵢyⱼ is not in ℒ̃	Roy 1992, Cor. 2; DALAG Cor. 11.16, via Th. 11.21	Diaz.strongSixExponentials	this project, with no hypothesis, through an elementary case of the multiplicity estimate (DALAG Th. 8.1)
the five exponentials theorem: for x₀, x₁ and y₀, y₁ free over ℚ and algebraic η ≠ 0, one of e^{xᵢyⱼ}, e^{ηx₁/x₀} is transcendental	Waldschmidt 1988, Cor. 2.2; DALAG §11.3.3	Diaz.five_exponentials	this project, from Roy's theorem and Baker's, as in DALAG (Remark after Cor. 11.16)
Roy's rank bound: a d × l matrix M with entries in ℒ̃ has rank at least dθ/(1 + θ), θ read off the zero blocks of PMQ for algebraic P, Q	Roy 1992, Cor. 1; DALAG Th. 12.20, Cor. 12.21	Diaz.roy_rank_bound	this project, with no hypothesis, from the linear subgroup theorem (DALAG Th. 11.21)
Roy's Theorem 5: if U ⊆ ℂᵈ meets Q̄ᵈ only in 0 and no rational subspace other than ℂᵈ contains it, a Q̄-free family in U ∩ ℒ̃ᵈ has at most φ(dim U, d) elements, φ the largest Σ nᵢdᵢ/(dᵢ − nᵢ) over the decompositions (dim U, d) = Σ (nᵢ, dᵢ)	Roy 1992, Th. 5, Remark (i) (p. 37) and Lemma (p. 40); DALAG Cor. 11.15	Diaz.roy_theorem_five, Diaz.roy_theorem_five_dmin, Diaz.dalag_cor_11_15_psi, Diaz.dalag_cor_11_15_rat	this project, with no hypothesis, from Roy's Theorem 4; φ in closed form, and DALAG's table Ψ as its integer part; over ℚ too, for (ℚ, ℚ + ℒ)
the four exponentials theorem in transcendence degree one	Waldschmidt 1973, Brownawell 1974	Diaz.four_exponentials_trdeg_one	this project
two of xᵢ, yⱼ, e^{xᵢyⱼ} are algebraically independent when one column is algebraic	Waldschmidt 1973, Brownawell 1974	Diaz.two_algebraically_independent_of_exp_column	this project
one of e^e, e^{e²} is transcendental (Schneider's eighth problem)	Waldschmidt 1973, Brownawell 1974	Transcendence.exp_e_or_exp_e_sq_transcendental	this project
Roy's lemma on singular spaces of matrices	D. Roy (Dasgupta–Kakde II, Thm 2.2; a stronger form is DALAG Prop. 12.5)	Transcendence.singular_matrix_subspace_annihilating_pair	this project
Waldschmidt's transcendence criterion; zero counts for exponential polynomials	Waldschmidt 1971	Diaz.transcendence_criterion, Diaz.expPoly_zero_count	this project
Baker's theorem: 1 and ℚ-independent logarithms of algebraic numbers are linearly independent over Q̄	Baker 1966; the route of Bertrand–Masser 1980, as in DALAG Ch. 4	Transcendence.baker_linear_forms_in_logarithms	this project
the criterion of Schneider–Lang for ℂ^{d₀} × (ℂ^×)^{d₁} with d₀ ≤ 1	Schneider 1949, Lang 1966; this form is DALAG Cor. 4.2	Transcendence.schneider_lang_cartesian	this project
a Schwarz lemma for Cartesian products	DALAG Prop. 4.7	Transcendence.cartesian_schwarz	this project

Some results carry a conjecture as an explicit hypothesis: Schanuel's conjecture; the strong four, sharp four and strong five exponentials conjectures; Waldschmidt's 2×2 determinant conjecture; the case n = 2 of Kirby's weak Schanuel conjecture; and the case n = 1 of Schanuel's conjecture over the kernel. Each is a hypothesis of the statement that uses it, named in that statement's section below, so the library still assumes only Lean's three axioms ("What is assumed"). Others carry Roy's strong six exponentials theorem, which is proved in the literature, as the hypothesis hSSE. It is proved here too, with no hypothesis, through an elementary case of the multiplicity estimate (DALAG Th. 8.1) that is proved as well, and Diaz/RoyUnconditional.lean restates each of those results without hSSE; see "Roy's theorem from a multiplicity estimate".

Names are the library's own; MIRROR_CHECKLIST.md maps each to its name on Prove2Me.

Proof engineering

A proof that Lean accepts can still be hard to use. These proofs are also kept short enough to read, cut where other proofs can reuse their parts, and written the same way throughout.

• Small results. Every result is a separate statement with its own proof. The size rule, counting lines of content without blanks and comments: a proof of 400 lines or more becomes a tree of results, and in a proof of 300 to 399 lines any helper over 40 lines becomes a result of its own. Five proofs break it (measured 15 October 2026): Lindemann–Weierstrass as ported from Mathlib PR #28013; exists_iteratedDeriv_presentation and exists_iteratedDeriv_presentation_of_exp_factor in the four exponentials development; and two of October, mobius_progression_space_contains_square_or_reciprocal and quadratic_ratio_progression_space_eq_involution_pencil_space.
• Import, don't re-prove. A result is proved once and imported where it is needed. The known exception is a transcendence-degree helper that is also the result Transcendence.trdeg_adjoin_le_one_of_isAlgebraic_adjoin: sixteen proofs carry their own lemmas of that kind. The proof of Waldschmidt's 1973 Théorème reuses 33 results of the four exponentials development unchanged.
• Shared tools. Pieces that several proofs need are results of their own in the Transcendence namespace, stated for general use rather than for the proof that first needed them: Siegel's lemma with an entrywise bound, Liouville's inequality in house form, the Cauchy estimate for an exponential polynomial on a grid, the length of integer polynomials under sums and products.
• One layout. Almost every result proved on Prove2Me is one module in Diaz/Mirror/, generated by a script from the accepted proof; its statement is the platform's, up to the namespace. The whole library builds on one version of Lean and Mathlib in CI.

What this has done so far:

• Five size waves, from 25 to 30 September 2026, took 27 proofs from 14,553 lines to 3,424. In the three waves where the new shared results were counted too, 8,963 lines became 5,052.
• One proof went from 1,550 lines to 44. Another carried 183 lines that no theorem used.
• Gelfond–Schneider was first carried as a single 5,388-line module, adapted from Karatarakis and Wiedijk's formalisation. It is now a tree of eleven results, 1,409 lines in all, and shares its grid estimate with the four exponentials development.

The sections below record each wave.

Diaz's conjecture

Let ℒ = {u ∈ ℂ : eᵘ ∈ Q̄ˣ}, the logarithms of algebraic numbers. Diaz conjectured in 2004 that no non-zero element of ℒ has algebraic modulus. He also asked a question of method: how could the non-holomorphic maps z ↦ z̄ and z ↦ |z| enter a transcendence proof at all?

The companion note (tex/) gives the mathematical account. Every branch of the conjecture is either closed or reduced to two open statements. Each of the published conjectures above would settle it. The note also records which methods cannot: in particular, nothing homogeneous on a candidate's own data, and, for a single power through its hull, the strong six exponentials route stops at u³.

The observation

Suppose u ≠ 0 has eᵘ and |u| both algebraic, and put ρ = u ū. Then

ū = ρ / u

so the conjugate of a candidate is not independent data — it is a rational function of u with algebraic coefficients. Hence Q̄(u) is a rational function field carrying an involution, and complex conjugation on it is determined by the ring structure rather than being extra information that might fail to be matched. Consequently no statement about vanishing of matrix coefficients over Q̄ ⊕ Q̄u ⊕ Q̄ū can tell a candidate apart from an ordinary complex number placed on the same circle.

An entire style of attack — accumulate algebraic constraints on u and ū until they collide — cannot settle the conjecture.

Build

lake exe cache get && lake build Diaz

Lean 4.35.0, Mathlib v4.35.0.

Dependency graph

Generated from the sources, not drawn by hand; the colouring is cross-checked against #print axioms and agrees. Amber would mark a declaration imported as an axiom and blue one resting on such an import; there are none left, so every node is green, proved outright. The graph covers the original development only, not the mirrored Prove2Me results under Diaz/Mirror/. Helper lemmas are omitted here for legibility; dependency-graph.dot carries all 61, grouped by file. Both are transitively reduced: an edge implied by a longer path is not drawn, so a declaration's full dependency set is its ancestors, not just its parents.

Regenerate with scripts/depgraph.py after any change to the Lean; nothing here is hand-maintained.

flowchart TD
  subgraph Axioms["Axioms.lean"]
    hermite_lindemann("hermite_lindemann")
    exists_ringHom_of_transcendental("exists_ringHom_of_transcendental")
  end
  subgraph Closure["Closure.lean"]
    hull("hull")
    transcendental_ne_zero("transcendental_ne_zero")
    ne_zero_of_notMem("ne_zero_of_notMem")
    conj_eq_rho_div("conj_eq_rho_div")
    conj_mem_hull("conj_mem_hull")
    conj_not_linear("conj_not_linear")
    conj_not_linear_hull("conj_not_linear_hull")
    eqOn_hull("eqOn_hull")
    transcendental_of_candidate("transcendental_of_candidate")
    transcendental_of_base("transcendental_of_base")
    transcendental_candidate_over_base("transcendental_candidate_over_base")
  end
  subgraph Model["Model.lean"]
    norm_form("norm_form")
    sq_add_sq_notMem("sq_add_sq_notMem")
    norm_mem_iff("norm_mem_iff")
    indep("indep")
    conj_coords("conj_coords")
    transcendental_exp_I("transcendental_exp_I")
    exists_transcendental_on_circle("exists_transcendental_on_circle")
    exists_transcendental_on_circle_sq("exists_transcendental_on_circle_sq")
  end
  subgraph Exponential["Exponential.lean"]
    isAlgebraic_two_rpow("isAlgebraic_two_rpow")
    Exp0("Exp0")
    Exp0_add("Exp0_add")
    Exp0_swap_conj("Exp0_swap_conj")
    Exp0_isAlgebraic("Exp0_isAlgebraic")
    Exp0_eq_one_iff("Exp0_eq_one_iff")
    Exp0_pow_eq_one_iff("Exp0_pow_eq_one_iff")
    model_falsifies("model_falsifies")
  end
  subgraph Transfer["Transfer.lean"]
    conj_comm("conj_comm")
    coeff_transfer("coeff_transfer")
    Hmat_transfer("Hmat_transfer")
    exists_conj_intertwining("exists_conj_intertwining")
  end
  subgraph Rigidity["Rigidity.lean"]
    Hmat("Hmat")
    det_Hmat("det_Hmat")
    no_vanishing_coeff("no_vanishing_coeff")
    coeff_eq_matrix("coeff_eq_matrix")
    no_vanishing_coeff_matrix("no_vanishing_coeff_matrix")
    candidate_no_vanishing_coeff("candidate_no_vanishing_coeff")
  end
  subgraph Instantiation["Instantiation.lean"]
    Qbar("Qbar")
    QbarIsAlgebraic("QbarIsAlgebraic")
    mem_Qbar_iff("mem_Qbar_iff")
    conj_mem_Qbar("conj_mem_Qbar")
    candidate_no_vanishing_coeff_Qbar("candidate_no_vanishing_coeff_Qbar")
    exists_transcendental_on_circle_Qbar("exists_transcendental_on_circle_Qbar")
    candidate_indistinguishable("candidate_indistinguishable")
  end
  subgraph Nodes["Nodes.lean"]
    not_on_axes("not_on_axes")
    plane_norm("plane_norm")
    indep_three("indep_three")
    four_nodes("four_nodes")
    sq_notMem_of_transcendental("sq_notMem_of_transcendental")
    four_nodes_candidate("four_nodes_candidate")
  end
  conj_eq_rho_div --> conj_mem_hull
  hull --> conj_not_linear_hull
  hull --> eqOn_hull
  hermite_lindemann --> transcendental_of_candidate
  transcendental_of_base --> transcendental_candidate_over_base
  transcendental_of_candidate --> transcendental_candidate_over_base
  norm_form --> norm_mem_iff
  sq_add_sq_notMem --> norm_mem_iff
  conj_eq_rho_div --> indep
  sq_add_sq_notMem --> indep
  transcendental_ne_zero --> indep
  transcendental_of_candidate --> transcendental_exp_I
  transcendental_exp_I --> exists_transcendental_on_circle
  transcendental_of_base --> exists_transcendental_on_circle
  exists_transcendental_on_circle --> exists_transcendental_on_circle_sq
  Exp0 --> Exp0_add
  Exp0 --> Exp0_isAlgebraic
  isAlgebraic_two_rpow --> Exp0_isAlgebraic
  Exp0 --> Exp0_eq_one_iff
  Exp0_eq_one_iff --> Exp0_pow_eq_one_iff
  Exp0_isAlgebraic --> model_falsifies
  conj_eq_rho_div --> conj_comm
  eqOn_hull --> conj_comm
  Hmat --> Hmat_transfer
  conj_comm --> Hmat_transfer
  conj_comm --> exists_conj_intertwining
  exists_ringHom_of_transcendental --> exists_conj_intertwining
  transcendental_ne_zero --> exists_conj_intertwining
  Hmat --> det_Hmat
  ne_zero_of_notMem --> no_vanishing_coeff
  Hmat --> coeff_eq_matrix
  coeff_eq_matrix --> no_vanishing_coeff_matrix
  no_vanishing_coeff --> no_vanishing_coeff_matrix
  no_vanishing_coeff_matrix --> candidate_no_vanishing_coeff
  transcendental_candidate_over_base --> candidate_no_vanishing_coeff
  Qbar --> QbarIsAlgebraic
  Qbar --> mem_Qbar_iff
  mem_Qbar_iff --> conj_mem_Qbar
  Qbar --> candidate_no_vanishing_coeff_Qbar
  candidate_no_vanishing_coeff --> candidate_no_vanishing_coeff_Qbar
  conj_mem_Qbar --> exists_transcendental_on_circle_Qbar
  exists_transcendental_on_circle --> exists_transcendental_on_circle_Qbar
  conj_mem_Qbar --> candidate_indistinguishable
  exists_conj_intertwining --> candidate_indistinguishable
  exists_transcendental_on_circle_sq --> candidate_indistinguishable
  transcendental_candidate_over_base --> candidate_indistinguishable
  conj_eq_rho_div --> indep_three
  transcendental_ne_zero --> indep_three
  plane_norm --> four_nodes
  four_nodes --> four_nodes_candidate
  not_on_axes --> four_nodes_candidate
  sq_notMem_of_transcendental --> four_nodes_candidate
  transcendental_candidate_over_base --> four_nodes_candidate
  classDef ax fill:#f5c26b,stroke:#b8860b,color:#000
  classDef onax fill:#bcd9f5,stroke:#3a6ea5,color:#000
  classDef proved fill:#c6e9c6,stroke:#3c8a3c,color:#000
  class hermite_lindemann,exists_ringHom_of_transcendental,hull,transcendental_ne_zero,ne_zero_of_notMem,conj_eq_rho_div,conj_mem_hull,conj_not_linear,conj_not_linear_hull,eqOn_hull,transcendental_of_candidate,transcendental_of_base,transcendental_candidate_over_base,norm_form,sq_add_sq_notMem,norm_mem_iff,indep,conj_coords,transcendental_exp_I,exists_transcendental_on_circle,exists_transcendental_on_circle_sq,isAlgebraic_two_rpow,Exp0,Exp0_add,Exp0_swap_conj,Exp0_isAlgebraic,Exp0_eq_one_iff,Exp0_pow_eq_one_iff,model_falsifies,conj_comm,coeff_transfer,Hmat_transfer,exists_conj_intertwining,Hmat,det_Hmat,no_vanishing_coeff,coeff_eq_matrix,no_vanishing_coeff_matrix,candidate_no_vanishing_coeff,Qbar,QbarIsAlgebraic,mem_Qbar_iff,conj_mem_Qbar,candidate_no_vanishing_coeff_Qbar,exists_transcendental_on_circle_Qbar,candidate_indistinguishable,not_on_axes,plane_norm,indep_three,four_nodes,sq_notMem_of_transcendental,four_nodes_candidate proved

Loading

The shape of it was the point, and it has changed. Everything is green. Two thin chains used to be blue — transcendence of a candidate, and the existence of the isomorphism — each ending at an amber node, Hermite–Lindemann and the Steinitz extension. Both of those are now proved in Axioms.lean, so the chains rest on nothing but Lean's own axioms.

What is proved

Closure.lean

• conj_eq_rho_div — ρ / u = conj u. Everything rests on this line.
• conj_mem_hull — the subfield generated by K and u is stable under conjugation.
• conj_not_linear, conj_not_linear_hull — conjugation is not linear over any base containing a non-real number, stated on ℂ and on the hull. The hull form is the one the refuted claim needs, since ∀ z ∈ hull is the weaker universal and so has the stronger negation.
• eqOn_hull — two ring homomorphisms agreeing on K and at u agree on the whole hull.

Model.lean

• norm_form — (a t + b t̄)(a t̄ + b t) = (a²+b²) t t̄ + a b (t² + t̄²).
• sq_add_sq_notMem — the cross term is not in K, else t satisfies X⁴ − c X² + ρ².
• norm_mem_iff — the elements of the rational plane with algebraic modulus are exactly the rational multiples of t and of t̄.
• indep — t and t̄ are ℚ-independent, so plane coordinates are well defined.
• conj_coords — conjugation acts on the plane by swapping coordinates, which is what licenses stating the involution in coordinates.
• exists_transcendental_on_circle — such a t exists, with the explicit witness r·e^i. The hypotheses of the model results are not merely satisfiable in the abstract.

Exponential.lean

• isAlgebraic_two_rpow — 2^q is algebraic for rational q.
• Exp0_add, Exp0_swap_conj, Exp0_isAlgebraic — a homomorphism into the algebraic numbers commuting with the involution.
• Exp0_eq_one_iff, Exp0_pow_eq_one_iff — this Exp₀ has a divisible kernel and torsion-free image. See the caveat below: both are properties of the choice, not of the model.
• model_falsifies — the analogue of Diaz's conjecture is false in the model: a non-zero element of the plane with algebraic norm and an algebraic formal exponential.

Transfer.lean

• conj_comm — an isomorphism matching the generators automatically intertwines conjugation. Nothing has to be arranged.
• exists_conj_intertwining — the closure theorem with existence included: two candidates over the same base with the same ρ are carried onto one another by a conjugation-intertwining endomorphism.
• coeff_transfer, Hmat_transfer — vanishing of coefficients over K, and the matrix H, transfer.

Instantiation.lean

• Qbar — the algebraic numbers as a Subfield ℂ, with the Algebra.IsAlgebraic ℚ instance supplied. Mathlib has it, but it does not fire through the IntermediateField → Subfield coercion.
• conj_mem_Qbar — that base is conjugation-stable, as every result above assumes of its base.
• candidate_no_vanishing_coeff_Qbar, exists_transcendental_on_circle_Qbar — the end-to-end theorem and the model's existence hypothesis, over the base the note is actually about.
• candidate_indistinguishable — candidacy to indistinguishability in one statement: a candidate and an ordinary complex number on the same circle are carried onto one another by a conjugation-intertwining endomorphism fixing the base.

Nodes.lean

• not_on_axes — a candidate has conj u ≠ u and conj u ≠ -u, so it lies on neither axis.
• indep_three — 1, u, conj u are independent over the base, which is what makes W_u three-dimensional.
• plane_norm — `(a u + b conj u)(a conj u + b u) = (a-b)²·u conj u
  • ab·(u + conj u)²for rationala, b`.
• four_nodes, four_nodes_candidate — inside the rational plane the points of the circle z conj z = ρ are determined: the four coordinate pairs (±1,0), (0,±1), that is ±u and ±conj u. The second takes the arithmetic hypotheses and derives the rest. Their distinctness, and so the count four, is not part of the formal statement.

Rigidity.lean

• det_Hmat, coeff_factor, no_vanishing_coeff — H = [[u, r], [r, ū]] has vanishing determinant, yet the coefficient is non-zero for all non-zero w, v over K. Dependent over ℂ, independent over K. Needs only u ∉ K, not transcendence.
• coeff_eq_matrix, no_vanishing_coeff_matrix — the hand-written coefficient is wᵀ H v, so the two results above concern one object.
• candidate_no_vanishing_coeff — the end-to-end statement: if u is a Diaz candidate over a base algebraic over ℚ, then H has no vanishing coefficient. This is the only place where the arithmetic hypothesis, rather than mere transcendence, is what is assumed.

Where everything is

• Diaz/ — the Lean library. Everything here builds in CI.
• archive/prove2me/ — every accepted Prove2Me proof for this mission, verbatim, not built.
• archive/local/ — proofs written for the mission and never published on the platform, not built.
• MIRROR_CHECKLIST.md — which Prove2Me results are already in Diaz/. The goal is all of them, and it is met: the count is at the top of this README. It includes the four Schanuel.* results proved for the mission (six exponentials, Hermite–Lindemann, Lindemann–Weierstrass, Gelfond–Schneider) and e_pi_transcendence, another contributor's node closed with Gelfond–Schneider.
• scripts/refresh_prove2me_archive.py — refreshes the archive and regenerates the checklist.
• tex/ — the companion notes. The note selects from the library; the library does not select.

The companion note

tex/diaz_prove2me.tex (and its PDF) is the mathematical account of what the mirrored nodes say: the ceiling, the quantisation of the imaginary part, the precise open boundary, two barriers and the branch that returns to its start, and the exclusions that come from leaving the candidate's three-dimensional hull. Every numbered statement in it carries a row in its Appendix A naming the formal identifier, so a reader can check any claim against this repository or against the platform rather than take it.

It is a published copy: the working copy lives elsewhere and is copied here after a script re-checks each appendix row against the live board.

Stable version 1.0 (2026-09-21) is tagged note-v1.0, with the PDF attached to the matching GitHub release. It records the end of the case analysis: every branch of the conjecture is closed or reduced to one of three open statements, named in its last section; version 1.26 (14 October 2026) reduces every branch to two. The older tex/diaz-modulus.tex is a different and earlier note, about the model and the negative result, and is not superseded by it.

tex/diaz-roy-rank-three.tex (2 November 2026, written by Claude) is a separate research note and is not formal: none of it is in the Lean library. It shows that Roy's rank bound at rank at most three cannot exclude u⁴ or u⁴ + cu³ through their hulls. That is a barrier on one method, not progress on the conjecture. Its rank-three and hull theorems are computer-assisted, with the scripts in scripts/roy_rank/. Its statements were not found in the sources read, and the note lists what those were.

Backup of the Prove2Me nodes

Prove2Me holds the proofs; this repository is where they are kept. Anything proved there and worth keeping is mirrored here, because a platform is not a place to store the only copy of a result.

Multipliers.lean, SFE.lean, Quantisation.lean, Line.lean, Pencil.lean, Kernel.lean, CheapLine.lean and Distance.lean are that mirror. They are stated in the platform's vocabulary — LogAlg, LogAlgTilde, IsCandidate, mirroring its DiazModulus preamble — rather than in this repository's abstract-subfield style, so that the declarations read the same in both places.

Here	On the platform
diaz_of_sfe, diaz_of_sfe_hl	DiazModulus.diaz_of_sfe
candidate_multiplier_module	DiazModulus.candidate_multiplier_module
candidate_one_log_saturation	DiazModulus.candidate_one_log_saturation
no_algebraic_line	DiazModulus.no_algebraic_generalized_line
candidate_no_real_algebraic_line	DiazModulus.candidate_no_real_algebraic_line
candidate_distance_transcendental	DiazModulus.candidate_distance_transcendental
real_quantisation	Diaz.real_quantisation
quantisation_orbit_iff_re_ne_zero	Diaz.quantisation_orbit_iff_re_ne_zero
leaf_iff_one	DiazModulus.leaf_iff_one
exp_ratMul_isAlgebraic, exp_ratio_pow_eq_one_iff	same names
det_pencil_eq_conic, roy_conic_implies_empty	same names
candidate_re_transcendental, candidate_im_transcendental, candidate_vanishing_ideal	DiazModulus.candidate_re_transcendental, DiazModulus.candidate_im_transcendental, DiazModulus.candidate_vanishing_ideal
sixExponentials_cannot_refute_candidate	same name
fibre_at_most_two	Diaz.fibre_at_most_two
hermite_lindemann_holds	DiazModulus.hermite_lindemann_holds
q_translate_unique, order_quantisation, torsion_dichotomy, period_plane_norm, indep_of_algebraic_product, no_holo_stab	same names

Every one of them is sorry-free and depends on no axiom of this repository: #print axioms lists only propext, Classical.choice, Quot.sound.

That now includes diaz_of_sfe. Hermite–Lindemann is no longer assumed for it: HermiteLindemann.lean proves hermite_lindemann_holds, and diaz_of_sfe discharges its hypothesis from that theorem rather than from Axioms.lean, where it is now proved as well.

The transcendence inputs stay explicit hypotheses of each statement rather than joining Axioms.lean: on the platform they are carried the same way, and the point of a mirror is that it reads identically.

DiazModulus.diaz_of_schanuel, the last to arrive, is mirrored too. An earlier note here blamed a missing Algebra ↥R ↥F instance on the older Mathlib; that was wrong. A hand port had dropped open IntermediateField.algebraAdjoinAdjoin, and the mechanical port only needed the submission's open noncomputable section closed before the namespace ends.

HermiteLindemann.lean and Fibre.lean share the Lindemann–Weierstrass development ported from an unmerged Mathlib pull request. It is kept once, in the former, and imported by the latter.

The first two, in detail

Multipliers.lean was not part of the first versions of the note (its appendix now cites it). It is a local copy of two results published on Prove2Me in September 2026, kept here so that they survive independently of that platform. They are stated in the platform's own vocabulary — LogAlg, LogAlgTilde, IsCandidate, mirroring its DiazModulus preamble — rather than in this repository's abstract-subfield style, so that the declarations read the same in both places.

• candidate_multiplier_module — under Roy's strong six exponentials theorem and Hermite–Lindemann, the set of z ∈ ℒ̃ with u z ∈ ℒ̃ is exactly Q̄ + Q̄/u. Consequently u² ∉ ℒ̃, and 1/(u − a) ∉ ℒ̃ for every non-zero algebraic a, even though 1/u itself is necessarily in ℒ̃. These are cases of Diaz (J. Théor. Nombres Bordeaux 19, 2007, Théorème 4(1) and Corollaire 5) and of Waldschmidt's Variations on the six exponentials theorem (2005), Corollary 2.2. Node 69387a9d-5e97-4b55-b6e6-64fa30ba558f.
• candidate_one_log_saturation — a candidate lying in Q̄ + Q̄ℓ for a single ℓ ∈ ℒ lies in Qℓ; at ℓ = iπ this rules out candidates of the form a + bπ. Node cf5024d1-43b6-47ac-b3dd-5298beba22a4.

These two complement Nodes.lean and the dimension count behind it. That count bounds what the three-dimensional hull span_Q̄{1, u, ū} of a candidate can contain, and so says a six-exponentials template cannot be assembled inside it. The multiplier module says what an extension of the hull would have to be, and that no algebraic operation on u supplies one.

The transcendence inputs stay explicit hypotheses of each statement rather than joining Axioms.lean: on the platform they are carried the same way, and the point of a backup is that it reads identically. Neither theorem depends on any axiom of this repository — #print axioms on both lists only propext, Classical.choice, Quot.sound.

Four exponentials in transcendence degree one

Diaz/Mirror/ carries a complete proof of the four exponentials theorem in transcendence degree one, as DiazModulus.four_exponentials_trdeg_one. In the form the node states it: take a 2×2 matrix of non-zero logarithms of algebraic numbers with l₁₁l₂₂ = l₁₂l₂₁, and suppose the field they generate has transcendence degree at most one; then its rows or its columns are ℚ-dependent. Equivalently, two ℚ-independent pairs x₁, x₂ and y₁, y₂ whose four products xᵢyⱼ are all logarithms of algebraic numbers generate a field of transcendence degree at least two. The theorem is classical, proved independently by Brownawell (1974) and Waldschmidt (1973); no new mathematics is claimed for it.

The route is Waldschmidt's 1973 proof together with the toolbox of his 1971 paper, so it needs neither a lower bound for linear forms in logarithms nor Philippon's zero estimate. The printed 1973 proof meets one hypothesis of its Lemme 2 with Gel'fond's two-logarithm bound, which Baker generalised; the separation-free zero count of 1971 makes that hypothesis unnecessary:

• transcendence_criterion — Gel'fond's criterion in the 1971 form: a number approximated well enough by integer polynomials of controlled degree and height is algebraic. Under it, small_irreducible_factor, height_dvd_le and the resultant bound.
• expPoly_zero_count and its scaled form — Tijdeman's count of the zeros of an exponential polynomial in a disc, with no separation hypothesis on the frequencies. This is what replaces Baker.
• cauchy_estimate_with_zeros and extrapolation — the Schwarz step: high-order vanishing on a small grid makes the derivatives tiny on a grid fourteen times larger.
• trdeg_one_presentation, aux_linear_system, siegel_aux — the arithmetic of the auxiliary function: write everything over ℤ[ω, ω₁], turn the vanishing conditions into an integer linear system, and solve it by Siegel's lemma.
• norm_to_polynomial_alg — the value becomes an integer polynomial in one variable, small at ω. Instead of taking a norm, it takes the determinant of multiplication modulo the minimal relation, which avoids building the field extension at all.
• construction_core_1973, auxiliary_construction, small_polynomials_of_counterexample, rank_one_parametrization, construction_growth, construction_count_1973 — the assembly and its bookkeeping.

The theorem settles one case of the conjecture's branch structure (DiazModulus.diaz_of_exp_not_real_irrational_angle_period_aligned_norm_rat_mult). What still blocks that branch is one statement about 1/π: the real half of (S), that e^{-iγ/π} is transcendental for real algebraic γ ≠ 0. Until 2026-09-23 the imaginary half was carried too. Both branches that reach (S) produce a real γ, and two new reductions record this, so the imaginary half is no longer needed. By DiazModulus.recip_pi_not_log_real_or_imag, the two halves cannot both fail.

The theorem has consequences beyond that case, all in Diaz/Mirror/:

• log_pair_rigid_of_trdeg_one — two non-zero logarithms u, v with |u|²/|v|² rational, and u, ū, v, v̄ of transcendence degree at most one, satisfy v ∈ ℚu ∪ ℚū. For K = Q̄ this is an unconditional and stronger form of the conditional quadric_trdeg_two; quadric_trdeg_two_alg (milestone 183) states that form, with quadric_trdeg_two's hypothesis hIU dropped.
• candidate_monomial_not_log — for a candidate u, e^{c u^k} is transcendental when k ≥ 2 and |c|²|u|^{2(k−1)} is rational. One example is e^{u²/|u|}. It is the unconditional part of the exclusion u² ∉ ℒ̃, which needs Roy's strong six exponentials theorem.
• geometric_triple_not_logs — w, wz, wz² are not all logarithms of algebraic numbers when z ∉ ℚ and trdeg ℚ(w, z) ≤ 1. Hence exp_pi_sq_or_exp_i_pi_cube_transcendental: at least one of e^{π²} and e^{iπ³} is transcendental. Both are classical: Waldschmidt, Nombres transcendants (LN 402, 1974), Cor. 7.4.3, and Waldschmidt, J. Number Theory 5 (1973), Cor. 2, found independently by Brownawell (1974).
• diaz_number_forces_transcendence — if t² + π² is algebraic for a real logarithm t, then e^{it²/π}, e^{π²/t} and e^{(t²+π²)/(iπ)} are transcendental. Hence log_two_diaz_or_transcendental: at least one of √((log 2)² + π²) and 2^{i log 2/π} is transcendental. The first number is the smallest open instance of Diaz's conjecture. The third conclusion says that the two remaining open boundary statements cannot fail at the same number. Stronger forms of the first two conclusions are classical: they need only t algebraic over ℚ(π) (LN 402, p. 202), so 2^{i log 2/π} is transcendental as soon as log 2 and π are algebraically dependent.
• recip_pi_or_pi_cube, exp_i_div_pi_or_exp_i_pi_cube_transcendental — each instance of (S) has a partner; at least one of e^{i/π} and e^{iπ³} is transcendental. Classical: Waldschmidt 1973, Cor. 4 and the remark after it.
• candidate_harmonic_not_log — for a candidate, |u|²/(pu + qū) is not a logarithm of an algebraic number; in particular neither is the harmonic mean of u and ū.

With the six exponentials theorem, two candidates of commensurable moduli supply the dimension that one candidate lacks. log_ratio_multipliers identifies what u/v multiplies back into ℒ. candidate_quotient_rigid and candidate_product_relation_trivial prove that the arguments of the candidates on a circle of algebraic radius form a Sidon set up to conjugation, which is the first constraint on algebraically independent families of candidates. candidate_neg_one_pow_ratio makes (−1)^{u/ū} = e^{iπu/ū} transcendental for every candidate. The duality log_square_duality, the ℚ-linear form of Diaz 2007, Corollaire 4(3), gives two_pow_log_three_or_three_pow_log_two: at least one of 2^{log₃2} and 3^{log₂3} is transcendental.

At rational squared moduli the theorem gives four statements of 29 September 2026. None of them was found in the sources read, and each follows from the theorem in a few lines. nongeneric_rational_modulus_orbit: logarithms of algebraic numbers that are algebraic over ℚ(π) and have rational squared modulus are rational multiples of one another, up to conjugation. torsion_rational_modulus_unique: at most one pair ±t with e^t algebraic makes t² + π² rational, so log_two_log_three_not_both_rational: (log 2)² + π² and (log 3)² + π² are not both rational. recip_pi_log_of_torsion_rational_modulus: a rational value of t² + π² would make e^{iγ/π} transcendental at every rational γ ≠ 0, so Diaz's conjecture at t + iπ and the statement (S) cannot both fail at rational data. With Waldschmidt's 1973 theorem in its algebraic-independence form carried as a hypothesis, pi_e_exp_pi_sq_indep_of_exp_i_rat_div_pi specialises it: if e^{ir/π} is algebraic for a rational r ≠ 0, then two of π, e, e^{π²} are algebraically independent. The next section proves the theorem, and pi_e_exp_pi_sq_indep_of_exp_i_rat_div_pi_algebraic drops the hypothesis.

Waldschmidt 1973, and Schneider's eighth problem

DiazModulus.two_algebraically_independent_of_exp_column is the Théorème of Waldschmidt 1973 in full: if x₁, x₂ and y₁, y₂ are ℚ-independent and one column, e^{x₁y₂} and e^{x₂y₂}, is algebraic, then two of the eight numbers xᵢ, yⱼ, e^{xᵢyⱼ} are algebraically independent. Brownawell found it independently (1974). It reuses 33 nodes of the four exponentials development above unchanged. Twelve new nodes carry the column case, where e^{x₁y₁} and e^{x₂y₁} are only algebraic over ℚ(ω), so their powers cost degree. They are sampled along the short side of the interpolation grid, where the degree budget absorbs them. Three consequences follow:

• Transcendence.exp_e_or_exp_e_sq_transcendental — Schneider's eighth problem, which gave the 1973 paper its title: at least one of e^e and e^{e²} is transcendental.
• DiazModulus.algebraicIndependent_e_pi_of_exp_pi_sq_algebraic — if e^{π²} is algebraic, then e and π are algebraically independent (Corollaire 1 at α = −1).
• DiazModulus.pi_e_exp_pi_sq_indep_of_exp_i_rat_div_pi_algebraic — the previous section's specialisation, now unconditional.

No new mathematics is claimed for any of them.

Baker's theorem, by Schneider–Lang in several variables

Twenty-five nodes of 2 October 2026 prove Baker's theorem in its qualitative, inhomogeneous form: if l₁, …, lₙ are logarithms of algebraic numbers, linearly independent over ℚ, then b₀ + b₁l₁ + ⋯ + bₙlₙ ≠ 0 for algebraic b₀, …, bₙ not all zero. On the platform this is Schanuel.baker_linear_forms_in_logarithms, which had been Open; here it is Transcendence.baker_linear_forms_in_logarithms. The route is the one Bertrand and Masser found (1980), as Waldschmidt writes it in Chapter 4 of Diophantine Approximation on Linear Algebraic Groups:

• Transcendence.schneider_lang_cartesian — the criterion of Schneider–Lang for ℂ^{d₀} × (ℂ^×)^{d₁} with d₀ ≤ 1 (the book's Corollary 4.2), proved directly as in §4.6: Siegel's lemma, Liouville's inequality, a Schwarz lemma, and the first derivative that does not vanish. No zero estimate is needed.
• Transcendence.cartesian_schwarz — a Schwarz lemma for Cartesian products (the book's Proposition 4.7), from one-variable Hermite division, telescoped over the coordinates. Mixed derivatives are lists of directions, matched with iteratedFDeriv by Transcendence.partials_eq_iteratedFDeriv.
• Transcendence.baker_number_field_basis — the book's Theorem 4.5: Baker's theorem for a basis of a number field, through its trace form.
• DiazModulus.baker_two_logs — the two-logarithm form that the nodes below had assumed as hB.

Step 5 of §4.6 needed a repair: vanishing to a given order in each coordinate does not survive the change of variables the proof makes, while vanishing to a given total order does; only the constants change. M. Karatarakis's Lean formalisation of the same chapter makes the same repair. It is on the branch baker of github.com/mkaratarakis/mathlib4, public since 25 September 2026 and not yet in Mathlib, and formalises Baker's theorem by the same route, the book's Corollary 4.2 for every d₀ ≤ n, and Proposition 4.7; his branch baker-padic formalises Brumer's p-adic analogue. A survey of the other provers on 4 October 2026 found none of these results elsewhere. The 25 proofs total 3,320 lines; the largest is 261.

No new mathematics is claimed.

Roy's theorem from a multiplicity estimate

Twenty-six nodes of 29 October 2026 prove Roy's strong six exponentials theorem (Roy 1992, Cor. 2; DALAG Cor. 11.16) from one explicit hypothesis, hME : MultiplicityEstimateElem (Diaz/MultiplicityEstimate.lean). The proof follows DALAG: Roy's map Υ (§11.6.2) and the linear subgroup theorem, Th. 11.21 (§11.7.1). The theorem is classical, and this is a formalisation of its known proof.

• The hypothesis. MultiplicityEstimateElem is the case G⁻ = {e}, G⁺ = G of the multiplicity estimate of DALAG Th. 8.1 (Philippon 1986), for G = 𝔾ₐ^{A₀} × 𝔾ₘ^{A₁}, written in coordinates. It is a def of a proposition, not an axiom. These 26 nodes take it as the explicit hypothesis hME, and the 32 nodes of "The multiplicity side, and hME itself" below prove it directly (Diaz.multiplicityEstimateElem); Th. 8.1 in general is not formalised. So Roy's theorem holds here with no hypothesis. On Prove2Me it is the published definition MultiplicityEstimateElem, archived as archive/prove2me/Def_MultiplicityEstimateElem.lean.
• The headline. DiazModulus.strong_six_exponentials (milestone): under hME, for x₁, x₂ and y₁, y₂, y₃ free over Q̄, some xᵢyⱼ is not in ℒ̃. DiazModulus.linear_subgroup_transcendence (milestone) is DALAG Th. 11.21 in the case d₀ ≤ n, under hME.
• The interpolation determinant (Steps 3–5 of the proof of Th. 11.21): thetaN_ge_mul_sub, iteratedDeriv_det_eq_sum, iteratedDeriv_iteratedFDeriv_line, interpolation_det_order (DALAG Lemma 9.2), schwarz_order_at_zero (Lemma 2.4), iteratedFDeriv_expMono_eq_op, op_monomial_eval_norm_le, op_entry_denom_house, interp_det_upper, interp_det_liouville, exists_ne_zero_mulVec_eq_zero_of_minors and interp_kernel.
• The obstruction and the parameters (Steps 6–7): exists_coord_complement, obstruction_1123 (under hME), params_1122_eventually and params_exponents.
• Roy's argument: exists_sse_lifts (restriction of scalars), sse_independence_facts, intMatrix_ker_facts, rank_le_of_injOn_lattice, sse_setup, sse_tangent_count, sse_relRank_generic and sse_relRank_rational. The case analysis of the obstruction does not use that it is defined over Q̄, and does not use Baker's theorem.
• The bridge. Diaz.strongSixExponentials_of_multiplicityEstimateElem : MultiplicityEstimateElem → StrongSixExponentials (Diaz/StrongSixExponentials.lean) restates the headline in the library's name.

So the declarations that carry Roy's theorem as the hypothesis hSSE hold with no hypothesis; each is restated without it in Diaz/RoyUnconditional.lean (below). They are candidate_multiplier_module, algebraic_modulus_log_multiplier_rational, candidate_cube_and_axis_multiple_not_mem_logAlgTilde, candidate_div_sq_sub_not_mem_logAlgTilde, candidate_laurent_conj_hull_class_not_mem_logAlgTilde, candidate_power_pair_not_both_mem_logAlgTilde, candidate_rational_conj_hull_criterion_not_mem_logAlgTilde, candidate_real_pencil_not_both_mem_logAlgTilde, candidate_sum_div_sq_sub_not_mem_logAlgTilde, candidate_two_pole_not_both_mem_logAlgTilde, diaz_2007_cor1_PQ, diaz_2007_cor2_P_consequences, diaz_2007_cor3_Q, diaz_2007_cor4, diaz_2007_cor5, diaz_2007_cor6, diaz_2007_cor7, diaz_2007_th4, diaz_2007_th5, diaz_2007_th6, diaz_2007_th7, logAlgTilde_adjoin_circle_point_no_two_by_three_configuration and pi_powers_not_both_mem_logAlgTilde. Two more carry its four-logarithm quotient form, which strong_six_exponentials_iff_quotient_form makes equivalent: nonreal_two_point_fibre_pi_sq, and diaz_2007_cor2_P1, stated over any subfield K, of which the case K = Q̄ follows.

Clean room: the agents that designed and wrote these 26 proofs worked under the rule that no agent was to open another formalisation of Roy's theorem. The 26 modules have 4,159 lines in Diaz/Mirror/; three are over 300: interp_det_upper (454), interp_det_liouville (395) and op_entry_denom_house (357).

The Hilbert side of hME. Thirty more nodes of 29 October 2026 prove the Hilbert-function half of hME, at finite level: inequalities between dimensions of boxes of polynomials, with no Hilbert polynomials. They are finite-level forms of DALAG Ch. 5 and 8 (chapter 8 is by D. Roy), all routine. The vocabulary is Diaz/HilbertBox.lean, the platform's definition DiazHilbertBox carried verbatim (archived as archive/prove2me/Def_DiazHilbertBox.lean): the Hilbert function boxHilb F I T = dim_K image(F_T → S/I) of a filtration, the boxes, the torus ideal (YᵢZᵢ − 1)ᵢ, and the proposition UnmixedHeight.

• The hypothesis hU. UnmixedHeight S is Macaulay's unmixedness in the form the chain consumes: for every weakly regular sequence of S, every associated prime of the quotient has height at most its length. Like hME, it is a def of a proposition, not an axiom. The chain bound and the Hilbert side take it as the explicit argument hU, and it is proved for polynomial rings over an algebraically closed field (below).
• The headline. DiazModulus.torus_hilbert_side (milestone): on the boxes of hME, in K[X, Y, Z] modulo the torus ideal of 𝔾ₐ^{A₀} × 𝔾ₘ^{A₁}, λ·2^{r(r−1)/2} ≤ 2^{rd} D₀^{d₀} (2D₁)^{d₁}, under hU; with le_hME_constant (milestone) this is the constant of hME. Over ℂ it holds without hU: Diaz.torus_hilbert_side_complex (below).
• Hilbert functions of filtrations: boxHilb_add_finrank_inf (rank–nullity), boxHilb_mono, boxHilb_anti, card_le_boxHilb_of_linearIndependent, exists_boxHilb_family (milestone), boxHilb_map_algEquiv, sum_boxHilb_le_boxHilb_iInf (DALAG Ex. 8.5(a)) and exists_card_mul_boxHilb_le_translates (milestone).
• The chain bound (DALAG Th. 8.4 and 8.8, at finite level): boxHilb_sup_span_add_le (Lemma 8.5), nat_telescope_step, nat_telescope_iter, exists_mem_forall_notMem_of_not_subset, exists_mem_isSMulRegular_of_associatedPrimes, isSMulRegular_quotient_of_isWeaklyRegular_append, exists_isWeaklyRegular_append_of_height (under hU), boxHilb_chain_bound and boxHilb_le_of_height (under hU). An infinite field is assumed only where prime avoidance needs it.
• The torus model: restrictSupport_block_filtration, torus_reduce_mem_restrictSupport and torus_reduced_inf_eq_bot (together: reduced monomials are a basis modulo the torus ideal, over any field), boxHilb_torusIdeal (the exact count), isWeaklyRegular_torusList (the generators are weakly regular), exists_translation_algEquiv (milestone; translations act by automorphisms) and torus_coeff_poly (milestone).
• The Hilbert side: le_of_forall_mul_pow_le, box_ray_upper_bound, box_ray_lower_bound (milestone), boxHilb_hilbert_side (under hU), torus_hilbert_side and le_hME_constant.

The 30 modules have 2,326 lines in Diaz/Mirror/; none is over 200.

Unmixedness for polynomial rings. Five more nodes of 29 October 2026 prove hU for polynomial rings over an algebraically closed field. DiazModulus.unmixedHeight_mvPolynomial (milestone; [IsAlgClosed K] [Finite σ]) is UnmixedHeight (MvPolynomial σ K): the inequality half of Macaulay's unmixedness theorem for K[X_σ] (Macaulay 1916; Bruns–Herzog, Cohen–Macaulay Rings, Th. 2.1.6). The theorem is classical, and this is a formalisation of its known proof; the reverse inequality is not stated. The route is local and uses regular sequences only, with Rees' theorem from Mathlib (ModuleCat.exists_isRegular_tfae) as the one tool of depth theory:

• length_le_ringKrullDim_quotient_of_mem_associatedPrimes (Matsumura Th. 17.2, for regular sequences): in a Noetherian local ring, a weakly regular sequence in the maximal ideal is no longer than dim A/𝔭 for every associated prime 𝔭.
• exists_isRegular_quotient_ofList (Rees' theorem and the long exact Ext sequence): cutting by a weakly regular sequence ps shortens a regular sequence in the maximal ideal by at most the length of ps.
• height_le_length_of_mem_associatedPrimes: the local form of the unmixedness theorem, for a local ring with a regular sequence as long as its dimension.
• exists_isWeaklyRegular_vanishing: the Xᵢ − aᵢ form a weakly regular sequence in R[X_σ].
• unmixedHeight_mvPolynomial: localise at a maximal ideal, which by the Nullstellensatz is the ideal of a point.
• The bridge. Diaz.torus_hilbert_side_complex (Diaz/HilbertSide.lean) is torus_hilbert_side for K = ℂ with hU supplied by unmixedHeight_mvPolynomial: the Hilbert side of hME over ℂ holds without hU. Its other inputs, the height bound hH and the lower bound hlow, are what the multiplicity side has to supply.

The 5 modules have 563 lines in Diaz/Mirror/.

The multiplicity side, and hME itself. Thirty-two nodes of 30 October 2026 prove hME. DiazModulus.multiplicityEstimateElem (milestone) is MultiplicityEstimateElem: the case G⁻ = {e}, G⁺ = G of DALAG Th. 8.1 for G = 𝔾ₐ^{A₀} × 𝔾ₘ^{A₁} over ℂ, written in coordinates. For G⁻ = {e} and finite Σ, DALAG notes that Th. 8.1 is a special case of Philippon 1986, Th. 2.1. The proof is that of DALAG §8.4 (chapter 8 is by D. Roy), at finite level and through elementary arguments. The theorem is classical, and this is a formalisation of its known proof. The vocabulary is Diaz/Multiplicity.lean, the platform's definition DiazMultiplicity carried verbatim (archived as archive/prove2me/Def_DiazMultiplicity.lean): the group TorusGroup, its invariant derivations torusDeriv, the translations torusTransl, the ideal torusVanishing S of a set of points and the zero set torusZero I of an ideal, the stabiliser torusStab, and the section ideals and obstruction spans of DALAG §8.4.1.

• Zero sets and heights on the torus: isPrime_iInf_ker_eval_of_analytic, le_height_torusVanishing, torusVanishing_univ, torusVanishing_torusZero (the Nullstellensatz on the torus), torusTransl_algEquiv, ringKrullDim_quotient_sectionIdeal_le and card_le_height_add_of_ringKrullDim_quotient_le.
• Characters and subgroups: eval_eq_zero_of_sum_mul_char (Dedekind's lemma with polynomial coefficients), eval_eq_zero_on_span_of_addSubgroup, exists_coordinate_section_add, exists_coordinate_section_mul, linearIndependent_on_subgroup and torusStab_subgroup.
• Invariant derivations (DALAG Lemma 8.11): torusDeriv_mem_torusBox, torusDeriv_torusTransl, eval_torusDerivList_torusCoeffPoly, eval_torusDerivList_eq_zero and vanishOrd_ideal.
• Tangent duals and Wüstholz's argument (Lemmas 8.14–8.16 and (8.20)): exists_tangent_dual, exists_tangent_dual_cosets, derivation_pow_mul_mem, card_multiIndex and wustholz_le_boxHilb.
• The obstruction (§8.4.1): exists_chain_prime, obstructionSpan_vanishOrd, exists_le_translate_of_le_torusVanishing, le_height_obstruction, le_boxHilb_torusVanishing_subgroup, hlow_le_boxHilb and exists_obstruction. Then multiplicityEstimateElem compares the lower bound with the Hilbert side (torus_hilbert_side, with unmixedHeight_mvPolynomial) through le_hME_constant.
• The headline. DiazModulus.strong_six_exponentials_unconditional (milestone): Roy's strong six exponentials theorem with no hypothesis, strong_six_exponentials applied to multiplicityEstimateElem.
• The bridges. Diaz.strongSixExponentials : StrongSixExponentials (Diaz/StrongSixExponentials.lean) is strongSixExponentials_of_multiplicityEstimateElem multiplicityEstimateElem. Diaz/RoyUnconditional.lean gives each of the 25 declarations above that take hSSE a corollary <name>_unconditional, with the same binders and conclusion and no hSSE; where Baker's theorem hB or Hermite–Lindemann hHL is a hypothesis too, it is supplied as well (baker_two_logs, hermite_lindemann_holds). The two statements of the quotient form over a general space aLog are specialised to aLog = ℒ̃.

So Roy's strong six exponentials theorem is machine-checked in the library with no hypothesis, from four rounds of October 2026: C1.4 (Roy's theorem from hME), C1.1 (the Hilbert side of hME), C1.2 (unmixedness for polynomial rings) and C1.3 (the multiplicity side and hME), 93 nodes in all. The agents that designed and wrote the 32 proofs of C1.3 worked under a clean-room rule: no agent was to open another formalisation of the theorem. The 32 modules have 4,270 lines in Diaz/Mirror/; the largest has 251.

The five exponentials theorem

Three nodes of 1 November 2026. All three are classical results, formalised routinely.

• DiazModulus.five_exponentials (milestone) — Waldschmidt's five exponentials theorem (1988, Cor. 2.2, p. 378; DALAG §11.3.3, Example 1): if x₀, x₁ are linearly independent over ℚ, y₀, y₁ too, and η ≠ 0 is algebraic, one of e^{x₀y₀}, e^{x₀y₁}, e^{x₁y₀}, e^{x₁y₁}, e^{ηx₁/x₀} is transcendental. The proof is DALAG's Remark after Cor. 11.16 (p. 399): Baker's theorem (Transcendence.baker_linear_forms_in_logarithms) turns ℚ-independence into Q̄-independence, with y₂ = η/x₀ as the third column, and Roy's strong six exponentials theorem (Diaz.strongSixExponentials, above) concludes.
• DiazModulus.two_pow_pi_or_three_pow_pi_transcendental — one of 2^π, 3^π is transcendental: Waldschmidt's statement (2.2.3) (1988, p. 379) at t = π, β = i. It strengthens two_three_five_pow_pi_transcendental, the instance of the six exponentials theorem with 2^π, 3^π, 5^π.
• DiazModulus.exp_mul_or_exp_sq_mul_transcendental — for non-zero logarithms λ₀, λ₁ of algebraic numbers and algebraic β ≠ 0, one of e^{βλ₀λ₁}, e^{(βλ₀)²λ₁} is transcendental: DALAG Exercise 11.8(b), p. 415; at λ₀ = λ₁ = log 2, β = 1 it is Exercise 11.8(c), one of 2^{log 2}, 2^{(log 2)²}.

All three are milestones of the Prove2Me mission: 173 for the theorem, 181 and 182 for the corollaries. The 3 modules have 238 lines in Diaz/Mirror/. The sharp six exponentials theorem (Waldschmidt 1988, Cor. 2.1) is not formalised.

Roy's Corollary 1: the rank of a matrix of logarithms

Ten nodes of 13 November 2026. All are formal proofs of classical results (Roy 1992; DALAG §11.6 and §12.3); two steps were not found in the sources read in the form stated, and both are routine.

• DiazModulus.roy_rank_bound (milestone) — Roy 1992, Cor. 1 (p. 38), for Q̄ and ℒ̃: a d × l matrix M with entries in ℒ̃, d ≥ 1, has invertible algebraic P, Q and 0 < d′ ≤ d, l′ ≤ l such that the top right d′ × (l − l′) block of PMQ vanishes and d·l′ ≤ rank(M)·(d′ + l′). That is Roy's bound rank(M) ≥ dθ/(1 + θ). With no hypothesis: it applies multiplicityEstimateElem.
• DiazModulus.roy_theorem_four — Roy's Theorem 4 in the form of DALAG Prop. 11.19: at a rational subspace S minimising (n − dim(U ∩ S))/(d − dim S), the images in ℂᵈ/S satisfy ℓ′d′ ≤ n′(d′ + ℓ′) and n′/d′ ≤ n/d.
• DiazModulus.roy_slope_bound, roy_semistable_node — the proof: an induction on d. A semistable U gets one application of the linear subgroup theorem (linear_subgroup_transcendence, DALAG Th. 11.21) at Υ⁻¹(U); otherwise ℂᵈ splits along a rational subspace of maximal slope. DALAG (Th. 11.5 (3′), Lemma 11.24) and Roy (his Th. 2) pass through other intermediate statements.
• Six leaves: lifts through Roy's map Υ (roy_field_lifts), its dimension counts (roy_upsilon_dims, DALAG Lemma 11.18), the image of an integer kernel (roy_intKer_image), the rank of the relations returned by Th. 11.21 (roy_relation_rank_le), a space of periods (roy_period_space), and coordinates adapted to a rational subspace (roy_rational_adapted_basis). The second-to-last two are the steps not found in the sources read in this form.

Milestone 185 of the Prove2Me mission is the corollary; the other nine joined by import. The 10 modules have 2,497 lines in Diaz/Mirror/. Roy's Theorem 5 (DALAG Cor. 11.15) and the printed applications of the corollary (Waldschmidt's Variations and Further variations, DALAG §12.3, Fischler 2001) are formalised in the two sections below.

Roy's Theorem 5 and Waldschmidt's Variations

Eleven nodes of 14 November 2026. All are formal proofs of classical results: Roy 1992, Th. 5; DALAG Cor. 11.15; §§2–3 of Waldschmidt's Variations on the six exponentials theorem (2005); and Cor. 6.3 of his The role of complex conjugation in transcendental number theory. All hold with no hypothesis. Two printed corollaries of Variations needed a correction, and the formal statements are the corrected ones (see "Printed statements corrected while formalising" below).

• DiazModulus.roy_theorem_five (milestone) — Roy 1992, Th. 5 (p. 39), for Q̄ and ℒ̃: if U ⊆ ℂᵈ meets Q̄ᵈ only in 0 and ℂᵈ is the only rational subspace containing it, then 0 < dim U < d, and ℓ Q̄-free points of U ∩ ℒ̃ᵈ satisfy ℓ ≤ Σ nᵢdᵢ/(dᵢ − nᵢ) for some decomposition (dim U, d) = Σ (nᵢ, dᵢ) with 0 < nᵢ < dᵢ. Roy's φ(n, d) is the largest such sum, so this is ℓ ≤ φ(dim U, d). The proof is Roy's induction on d (pp. 39–40) through his Theorem 4 (roy_theorem_four, above), with two helpers: roy_theorem_four_exists (Theorem 4 at a rational subspace that minimises the ratio) and roy_hull_transport (coordinates adapted to a rational subspace of least dimension).
• DiazModulus.roy_theorem_five_dmin (milestone) — DALAG Cor. 11.15 (p. 398) for (Q̄, ℒ̃), in the same form: if V ∩ Q̄ᵈ = 0, then V ∩ ℒ̃ᵈ is finite-dimensional over Q̄, of dimension at most Σ nᵢdᵢ/(dᵢ − nᵢ) for a decomposition of (dim V, d_min), where d_min is the least dimension of a rational subspace containing V. The proof follows Roy, not DALAG's argument for the corollary. The bound in DALAG's printed form, with the table Ψ, is dalag_cor_11_15_psi (below).
• DiazModulus.variations_hyperplane_bound (milestone) — Variations Th. 3.1 (p. 347): a hyperplane of ℂᵈ that meets Q̄ᵈ only in 0 meets ℒ̃ᵈ in dimension at most d(d − 1) over Q̄; the hyperplane case of the previous item. DiazModulus.variations_cor_3_2 (milestone) — Cor. 3.2 (p. 348): for an m × ℓ matrix (Λᵢⱼ) over ℒ̃ with Q̄-free columns, Q̄-free x₁, …, x_m ∈ ℂ and ℓ > m(m − 1), some Σᵢ xᵢΛᵢⱼ is non-zero.
• DiazModulus.variations_theorem_2_11 (milestone) — Variations Th. 2.11 (p. 346; Role Th. 6.2): if the columns of (I_m, M) are Q̄-free for M = (Λᵢⱼ) over ℒ̃, 1, Λ₁, …, Λ_m ∈ ℒ̃ are Q̄-free and ℓ > m², some Σᵢ ΛᵢΛᵢⱼ is not in ℒ̃. From the hyperplane bound in ℂ^{m+1}.
• DiazModulus.role_cor_6_3 (milestone) — Role Cor. 6.3: for a 2 × 5 matrix over ℒ̃ with 1, Λ₁₁, Λ₂₁ Q̄-free and the seven columns of (I₂, M) Q̄-free, some Λ₁₁Λ₂ⱼ − Λ₂₁Λ₁ⱼ (j = 2, …, 5) is not in ℒ̃. This is the author's own correction of Variations Cor. 2.12, proved as printed from Th. 2.11.
• DiazModulus.variations_cor_2_13_corrected (milestone) — Variations Cor. 2.13, corrected: for (Λᵢⱼ) ∈ ℒ̃^{2×3} with Λ₁₁, Λ₂₁ each real or purely imaginary, 1, Λ₁₁, Λ₂₁ Q̄-free and 1, Λ₂₁, Λ₂₂, Λ₂₃, Λ̄₂₂, Λ̄₂₃ Q̄-free, one of Λ₁₁Λ₂₂ − Λ₂₁Λ₁₂, Λ₁₁Λ₂₃ − Λ₂₁Λ₁₃ is not in ℒ̃. From Cor. 6.3 and the stability of ℒ̃ under complex conjugation (logAlgTilde_conj_stable), with signs on the conjugate columns of the printed proof.
• DiazModulus.variations_cor_2_14 (milestone) — Variations Cor. 2.14 (p. 347): the same conclusion as Th. 2.11 for an m × ℓ matrix of logarithms with ℚ-free columns and ℚ-free logarithms λ₁, …, λ_m, ℓ > m². From Th. 2.11 and Baker's theorem (Transcendence.baker_linear_forms_in_logarithms), through baker_columns_qbar_independent: Baker's theorem in column form, ℚ-free columns over ℒ make the columns of (I_m, M) Q̄-free.

Milestones 186–193 of the Prove2Me mission are the eight printed results; the three helpers joined by import. The 11 modules have 1,269 lines in Diaz/Mirror/. Roy's closed form of φ (his Lemma on p. 40) and DALAG's table Ψ are formalised in "Further variations Th. 2.1 for every Y, Roy's Lemma, DALAG Cor. 11.15 and 12.23" below. Not formalised: Variations Th. 3.3 and Cor. 3.4–3.5, which rest on DALAG Cor. 11.6 rather than on Roy's theorem.

Applications of Roy's Corollary 1: Further variations, DALAG §12.3, Fischler

Eighteen nodes of 14 November 2026: the printed applications of Roy's Corollary 1 (roy_rank_bound, above) in Waldschmidt's Further variations on the six exponentials theorem (2005), in DALAG §12.3, and in Fischler's Orbits under algebraic groups and logarithms of algebraic numbers (2001). All are formal proofs of classical results, with no hypothesis.

• Further variations.
  • DiazModulus.fv_theorem_2_1 (milestone) — Th. 2.1 (p. 5), for finite-dimensional Y: if X, Y ⊆ ℂⁿ are Q̄-subspaces with dim X = d > n and μ(Y, ℂⁿ) > d/(d − n), then x · y ∉ ℒ̃ for some x ∈ X, y ∈ Y. Here x · y is the bilinear dot product and μ(Y, ℂⁿ) the least dim_Q̄(Y/(Y ∩ V))/codim V over all ℂ-subspaces V ≠ ℂⁿ. The printed statement allows any Y; its proof covers finite-dimensional Y, which is the case stated here, and fv_theorem_2_1_rank (below) proves the statement for every Y. The proof takes one ℂ-subspace of maximal slope for X (fv_max_slope) and a relative form of the semistable case (fv_semistable_core), with Roy's Corollary 1 applied once to a Gram matrix (fv_gram_zero_block) and the orthogonal for the dot product (fv_dot_orthogonal), in place of the printed reduction after Waldschmidt 1981, Lemmes 5.1–5.2.
  • DiazModulus.fv_theorem_1_2 (milestone) — Th. 1.2, the main result: if M ∈ ℒ̃^{2×3} and the five rows of (M; I₃) and the five columns of (I₂, M) are Q̄-free, one of the three 2 × 2 minors of M is not in ℒ̃. From Th. 2.1 at n = 2, d = 5, with the estimate (3.1) for lines (fv_two_by_three_lines).
  • DiazModulus.fv_lambda_squares (milestone) — the example of p. 3: if 1, Λ₁, Λ₂, Λ₃ ∈ ℒ̃ are Q̄-free, one of Λ₁² − Λ₂Λ₃, Λ₂² − Λ₃Λ₁, Λ₃² − Λ₁Λ₂ is not in ℒ̃.
  • DiazModulus.fv_cor_1_4 (milestone) — Cor. 1.4: for a 2 × 3 matrix of logarithms with ℚ-free rows and ℚ-free columns, one of its three 2 × 2 minors is not in ℒ̃; from Th. 1.2 and Baker's theorem in column form.
• DALAG §12.3.
  • DiazModulus.dalag_cor_12_21 (milestone) — Cor. 12.21 (p. 435): if Σᵢⱼ τᵢσⱼΛᵢⱼ ≠ 0 for all non-zero algebraic τ, σ, then rank M ≥ dℓ/(d + ℓ).
  • DiazModulus.dalag_cor_12_22 (milestone) — Cor. 12.22 (p. 436): the rank of a matrix over ℒ̃ is at least half its structural rank over Q̄. The structural rank is the rank of Σₖ XₖNₖ over Q̄(X₁, …, X_m) for a presentation M = Σₖ eₖNₖ with Q̄-free eₖ and algebraic Nₖ; the statement holds for every presentation. One helper: matrix_rank_le_of_zero_block.
  • DiazModulus.dalag_cor_12_24 (milestone) — Cor. 12.24 (p. 436): a d × ℓ matrix over ℒ̃ with Q̄-free rows, Q̄-free columns and dℓ > d + ℓ has rank at least 2. Proved from Th. 12.20 (Roy's Corollary 1) by a direct case analysis: the deduction from Cor. 12.22 that DALAG indicates gives only rank ≥ 1 for 2 × 3 matrices.
• Fischler 2001.
  • DiazModulus.fischler_centralizer (milestone) — Th. 1.2 (p. 169), complex case: if M ∈ ℒ̃^{n×n} has n² entries linearly independent over Q̄, its centraliser has dimension at most (n² + 1)/2. (Fischler's ℒ is ℒ̃ here.) The proof is Fischler's: fischler_prop_5_5 (Prop. 5.5, with Roy's Corollary 1 applied to ad M on the trace-zero matrices in coordinates, in place of Fischler's Cor. 2.2, so that the two subspaces are spanned by explicit algebraic matrices), fischler_commute_of_trace, and Rémond's lemma.
  • DiazModulus.remond_commuting_subspaces (milestone) — Fischler's Lemma 5.6, due to Rémond: subspaces U, V of Matₙ(ℂ) whose elements commute with each other have dim U + dim V ≤ n² + 1. From remond_commuting_end, the same statement for endomorphisms, by the printed induction on n.

Milestones 194–202 of the Prove2Me mission are the nine headline results; the other nine joined by import. The 18 modules have 1,851 lines in Diaz/Mirror/. Further variations Th. 2.1 for infinite-dimensional Y and DALAG Cor. 12.23 are formalised in the next section. Not formalised: Further variations Cor. 1.3; the ℚ + ℒ statement after DALAG Cor. 12.24; Fischler's Th. 1.1 and §4, on orbits under algebraic groups.

Printed statements corrected while formalising. Formalising these results met three printed statements that are false as stated, two of them used here: Variations Cor. 2.12, which the author corrected in Further variations §4 and in Role Cor. 6.3, and Variations Cor. 2.13, for which no correction was found in the sources consulted; the formal statements are the corrected ones. The third, DALAG Lemma 11.24, is not used by the formal proofs. The printed proof of Variations Cor. 2.13 also needs signs on two columns when one of Λ₁₁, Λ₂₁ is real and the other purely imaginary; DALAG's deduction of Cor. 12.24 from Cor. 12.22 does not give rank 2, so Cor. 12.24 is proved here from Th. 12.20; and the printed proof of Further variations Th. 2.1 covers finite-dimensional Y, which is how it is stated here; the next section proves the statement as printed. ERRATA.md gives each point with the printed text, a counterexample or the missing step, and the repair, with gaps in DALAG's proofs of Cor. 11.10/11.15, Prop. 11.19 (for (ℚ, ℚ + ℒ)), Th. 11.21, Lemma 12.9 and Prop. 12.13 and in Roy's proof of his Lemma on φ, a fourth false statement (DALAG Lemma 11.18 (2)), and a list of smaller slips.

Further variations Th. 2.1 for every Y, Roy's Lemma, DALAG Cor. 11.15 and 12.23

Fifteen nodes of 14 November 2026. All are formal proofs of classical results, with no hypothesis: Waldschmidt's Further variations Th. 2.1 as printed, for every Q̄-subspace Y; Roy's Lemma (Roy 1992, p. 40), the closed form of φ(n, d); DALAG Cor. 11.15 for (Q̄, ℒ̃) with DALAG's table Ψ; and DALAG Cor. 12.23. Each completes a result of the two sections above.

• DiazModulus.fv_theorem_2_1_rank (milestone) — Further variations Th. 2.1 (p. 5) as printed: Y is any Q̄-subspace of ℂⁿ, and the hypothesis μ(Y, ℂⁿ) > d/(d − n) is read with dim_Q̄ Y/(Y ∩ V) a cardinal. From fv_theorem_2_1_general, the same theorem with the hypothesis through finite-dimensional witnesses (for each V ≠ ℂⁿ, some finite-dimensional Y₀ ⊆ Y with d·(n − dim V) < (d − n)·dim_Q̄ Y₀/(Y₀ ∩ V)), and fv_rank_quot_witness (if dim_Q̄ Y/(Y ∩ V) ≥ N, some finite-dimensional Y₀ ⊆ Y has dim Y₀/(Y₀ ∩ V) ≥ N). The printed proof covers finite-dimensional Y (fv_theorem_2_1, above). fv_finite_approx supplies the missing step: for every Y and every integer B, one finite-dimensional Y₀ ⊆ Y has dim Y₀/(Y₀ ∩ V) ≥ min(dim Y/(Y ∩ V), B) for every ℂ-subspace V at once. Its proof maximises a bounded integer attached to the intersection of the subspaces V where a finite-dimensional subspace falls short of B, with three dimension counts as helpers (fv_rho_excess, fv_rho_inf, fv_rho_sInf); no topology on Grassmannians is used.
• DiazModulus.roy_lemma_phi (milestone) — Roy's Lemma (Roy 1992, p. 40; not Roy's lemma on singular spaces of matrices in the table above): for 0 < n < d, the largest Σ nᵢdᵢ/(dᵢ − nᵢ) over the decompositions (n, d) = Σ (nᵢ, dᵢ), 0 < nᵢ < dᵢ, is nd/(d − n) if n = 1 or d − n = 1, and (d − n)/(d − n − 1) + (n − 1)n otherwise, which Roy writes φ(1, d − n) + φ(n − 1, n). The proof is not Roy's exchange argument but roy_phi_closed_form_superadd: the closed form bounds a single part and is superadditive, so it bounds every decomposition by induction on the number of parts.
• DiazModulus.dalag_cor_11_15_psi (milestone) — DALAG Cor. 11.15 (p. 398) for (Q̄, ℒ̃) in its printed form: if V ∩ Q̄ᵈ = 0, then dim_Q̄(V ∩ ℒ̃ᵈ) ≤ Ψ(dim V, d_min), with DALAG's table Ψ (p. 394), and dim V < d_min when V ≠ 0. From roy_theorem_five_dmin (above) and dalag_psi_floor_roy_phi: Ψ(n, d) = ⌊φ(n, d)⌋, row by row from Roy's Lemma.
• DiazModulus.dalag_cor_12_23 (milestone) — DALAG Cor. 12.23 (p. 436): a matrix with entries in ℚ + ℒ has rank at least half its structural rank over ℚ, for every presentation M = Σₖ eₖNₖ with ℚ-free eₖ ∈ ℚ + ℒ and rational Nₖ. From dalag_cor_12_22 (above) and three helpers: baker_rat_add_logAlg_free, Baker's theorem for ℚ + ℒ (elements free over ℚ are free over Q̄), through logAlg_exists_rat_basis (a ℚ-basis chosen among finitely many logarithms); and matrix_rank_map_field (a homomorphism of fields preserves the rank of a matrix). DALAG's Lemma 12.9 is not needed; the affine form of p. 435 is dalag_cor_12_23_affine (below).

Milestones 203–206 of the Prove2Me mission are the four printed results; the other eleven joined by import. The 15 modules have 1,330 lines in Diaz/Mirror/. DALAG Cor. 11.15 for (ℚ, ℚ + ℒ) and DALAG Lemma 12.9 are formalised in the next two sections.

Printed proofs completed while formalising. The proof of Further variations Th. 2.1 covers finite-dimensional Y only, and the statement as printed is true: the finite approximation above reduces it to that case. Roy's proof of his Lemma concludes that a maximising decomposition has two parts from two exclusions that leave parts (nᵢ, dᵢ) = (1, 2) free: for (n, d) = (3, 7) the decomposition (1, 3), (1, 2), (1, 2) meets every condition of the printed argument and has three parts. One exchange on three parts repairs it, and the Lemma is correct. DALAG's proof of Lemma 12.9 leaves a dehomogenisation implicit, and its table Ψ does not define Ψ(0, 0), which Cor. 11.15 uses at V = 0. ERRATA.md gives each point with the printed text, the evidence and the repair.

DALAG Cor. 11.15 for (ℚ, ℚ + ℒ), by Roy's route over ℚ

Eight nodes of 14 November 2026. All are formal proofs of classical results: DALAG Cor. 11.15 (p. 398) for (ℚ, ℚ + ℒ), with no hypothesis, and on the way Roy's Theorems 4 and 5 over ℚ. Roy's Remark (i) (p. 37) says that his Theorem 4 holds over every subfield F of Q̄, with F + F·ℒ in place of ℒ̃; here F = ℚ, and ℚ + ℒ is the ℚ-span of 1 and ℒ. A subspace is rational over ℚ when it is spanned by vectors with rational coordinates.

• DiazModulus.dalag_cor_11_15_rat (milestone) — DALAG Cor. 11.15 (p. 398) for (ℚ, ℚ + ℒ) in its printed form: if V ⊆ ℂᵈ meets ℚᵈ only in 0, then V ∩ (ℚ + ℒ)ᵈ is finite-dimensional over ℚ and dim_ℚ(V ∩ (ℚ + ℒ)ᵈ) ≤ Ψ(dim V, d_min), with DALAG's table Ψ (p. 394) and d_min the least dimension of a subspace rational over ℚ that contains V; and dim V < d_min when V ≠ 0. From roy_rat_theorem_five and dalag_psi_floor_roy_phi (above), with Ψ(n, ·) non-increasing above n.
• DiazModulus.roy_rat_theorem_five — Roy 1992, Th. 5 (p. 39) over ℚ: if U ⊆ ℂᵈ meets ℚᵈ only in 0, then ℓ ℚ-free points of U ∩ (ℚ + ℒ)ᵈ satisfy ℓ ≤ Σ nᵢdᵢ/(dᵢ − nᵢ) for some subspace S ⊇ U rational over ℚ and some decomposition (dim U, dim S) = Σ (nᵢ, dᵢ) with 0 < nᵢ < dᵢ. By an induction on d that splits along a subspace of maximal slope, with the slope bound on the subspace and the induction on the quotient, so that Roy's hypothesis that ℂᵈ is the least subspace rational over ℚ containing U is not needed.
• DiazModulus.roy_rat_slope_bound, roy_rat_semistable_node — Roy's Theorem 4 over ℚ, in the slope form of roy_slope_bound, by the same induction as over Q̄: a semistable U gets one application of the linear subgroup theorem (linear_subgroup_transcendence, DALAG Th. 11.21), for Roy's map Υ(x, y) = x + y. The additive part of the obstruction it returns is replaced by the span of its rational vectors, so no subgroup has to be selected and DALAG Prop. 11.19 is not used. Both take the multiplicity estimate hME as a hypothesis, as their Q̄ versions do; roy_rat_theorem_five discharges it with multiplicityEstimateElem.
• Four leaves: ratLogAlg_mem_iff (the ℚ-span of 1 and ℒ is ℚ + ℒ, which gives the lifts through Υ), and three ℚ analogues of leaves of "Roy's Corollary 1" above: roy_rat_adapted_basis (coordinates adapted to a subspace rational over ℚ, by a rational matrix), roy_rat_relation_rank_le (the rank of the relations returned by Th. 11.21) and roy_rat_period_space (a space of periods).

Milestone 207 of the Prove2Me mission is the corollary; the other seven joined by import. Apart from linear_subgroup_transcendence, multiplicityEstimateElem and dalag_psi_floor_roy_phi, they import nothing proved earlier; in particular not Baker's theorem. The 8 modules have 2,138 lines in Diaz/Mirror/.

A printed proof that misses this case. DALAG proves Cor. 11.15 (p. 403) from Prop. 11.19, whose proof reads Th. 11.5 (3′) at the trivial subgroup. For (ℚ, ℚ + ℒ) that step fails: Th. 11.5 ranges over subgroups defined over Q̄, and for U = ℂ(1, √2, 0) + ℂ(log 2, log 3, log 5) in ℂ³ a subgroup with tangent space ℂ(1, √2, 0) × {0} ties with the trivial one and is the one (3′) selects. The example refutes the inference, not the inequality, and Prop. 11.19 is true; the route above proves the corollary without it. The tie comes from the algebraic vector (1, √2, 0) of U, which the second clause of DALAG Lemma 11.18 (2) would exclude; that clause is false, since U ∩ kᵈ = 0 does not give U ∩ Q̄ᵈ = 0. For (Q̄, ℒ̃) the printed step is right. ERRATA.md gives both points (A4, B9) with the printed text and the evidence.

DALAG Lemma 12.9, and Cor. 12.23 in the affine form of p. 435

Four nodes of 14 November 2026, formal proofs of classical results with no hypothesis. DALAG §12.1.4 defines the structural rank of a matrix M with entries in a field K, over a subfield k, through an injective k-linear map from the span of its entries into the linear forms kX₁ + ⋯ + kXₙ; Lemma 12.9 (p. 427) allows the affine forms k + kX₁ + ⋯ + kXₙ. As in dalag_cor_12_22, the structural rank is computed from a presentation M = Σⱼ eⱼNⱼ, with k-free eⱼ and Nⱼ over k: it is the rank of Σⱼ ZⱼNⱼ over k(Z₁, …, Z_m).

• DiazModulus.dalag_lemma_12_9 (milestone) — DALAG Lemma 12.9 (p. 427), for any field k: if φ : K → k + kX₁ + ⋯ + kXₙ is k-linear and injective on the span of the eⱼ, the rank of φ(M) over k(X₁, …, Xₙ) is the structural rank of M. From two helpers, the two steps the printed proof leaves implicit: dalag_lemma_12_9_dehomog, dehomogenisation keeps the rank (N₀ + Σᵢ XᵢNᵢ over k(X₁, …, X_m) and Y₀N₀ + Σᵢ YᵢNᵢ over k(Y₀, …, Y_m) have the same rank); and dalag_lemma_12_8_linear, DALAG Lemma 12.8 (p. 426) for every k-linear map into linear forms that is injective on the span of the eⱼ, not only for one given by a basis. Both rest on matrix_rank_map_field (above).
• DiazModulus.dalag_cor_12_23_affine (milestone) — DALAG Cor. 12.23 (p. 436) with the matrix of p. 435: if M = M₀ + Σₖ λₖNₖ with rational M₀, Nₖ, λₖ ∈ ℚ + ℒ and 1, λ₁, …, λ_m linearly independent over ℚ, then rank_{ℚ(X₁, …, X_m)}(M₀ + Σₖ XₖNₖ) ≤ 2·rank M. By Lemma 12.9 the left side is the structural rank over ℚ. From dalag_cor_12_23 (above) and dalag_lemma_12_9_dehomog.

Milestones 208 and 209 of the Prove2Me mission are the lemma and the corollary; the other two joined by import. The 4 modules have 356 lines in Diaz/Mirror/. Not formalised: DALAG Prop. 12.13, whose proof uses Lemma 12.9.

Printed proofs completed while formalising. DALAG's proof of Lemma 12.9 (p. 428) obtains the structural rank as the rank of a homogenised matrix and leaves the dehomogenisation implicit; it also applies Lemma 12.8 to a map not given by a basis, which the proof of Lemma 12.8 covers. Its proof of Prop. 12.13, (iv) ⇒ (iii) (p. 430), applies (iv) to a matrix whose entries need not lie in the space E that (iv) is about; multiplying that matrix by x₀ gives one over E with the same rank and, by Lemma 12.9, full structural rank, and the proposition is correct. Two slips nearby: "k-vector subspace" for "K-vector subspace" in the proof of Prop. 12.7 (p. 426), and "a r × r matrix" in the remark before Lemma 12.9 (p. 427), meant for a matrix k-equivalent to one with a regular r × r block. ERRATA.md gives each point (B7, B8, C10, C11) with the printed text, the evidence and the repair.

Consequences of Roy's strong six exponentials theorem

Ten nodes of 1 October 2026 carry Roy's strong six exponentials theorem as the hypothesis hSSE (later rounds added more), in the form of candidate_multiplier_module: if x₁, x₂ and y₁, y₂, y₃ are linearly independent over Q̄, one of the six products xᵢyⱼ is not in ℒ̃. Every statement was read on the page first. Since 30 October 2026 they hold with no hypothesis: Diaz/RoyUnconditional.lean states each as <name>_unconditional.

• DiazModulus.strong_six_exponentials_iff_quotient_form — Diaz 2007, Théorème 3: the theorem is equivalent to its four-logarithm quotient form. No hypothesis; it also connects the two forms in which earlier nodes carry the theorem.
• DiazModulus.diaz_2007_cor1_PQ, diaz_2007_cor2_P_consequences, diaz_2007_cor4, diaz_2007_cor5 — Diaz 2007, Corollaires 1 (PQ), 2 (P) 2) with its Conséquences 1–3, 4 and 5, in general.
• DiazModulus.candidate_cube_and_axis_multiple_not_mem_logAlgTilde — every candidate has u³ ∉ ℒ̃, and λu ∉ ℒ̃ for every transcendental λ ∈ ℒ̃ on the real or imaginary axis; so e^{βπu} is transcendental for every algebraic β ≠ 0. Diaz's general proofs use Baker's theorem; at a candidate, Hermite–Lindemann does that step.
• DiazModulus.pi_powers_not_both_mem_logAlgTilde — π² and π³, π² and 1/π, 1/π and 1/π² are pairwise not both in ℒ̃ (Diaz's own instances at λ = iπ). An exception to (S) would therefore make e^{π²} transcendental.
• DiazModulus.algebraic_modulus_log_multiplier_rational — with Baker's theorem as a second hypothesis: if λ ∈ ℒ ∖ {0}, u ∈ ℒ̃, and |u| and e^{uλ} are algebraic, then u ∈ ℚ or uλ/λ̄ ∈ ℚ. For arbitrary u this is an open question in Waldschmidt's book (2000, p. 399), which derives it from the strong four exponentials conjecture (algebraic_modulus_log_multiplier_rational_of_sfe, below); the derivation of the case u ∈ ℒ̃ was not found in the sources read.
• Two helpers: logAlgTilde_conj_stable and quadratic_eq_zero_of_not_mem_Qbar.
• The rest of Diaz 2007 §2, added the same day: diaz_2007_cor3_Q, diaz_2007_th4, diaz_2007_cor6, diaz_2007_th5, diaz_2007_cor7 (the modular statement (C4) of Diaz 1997 when τ or 1/τ lies in ℒ̃), diaz_2007_th6 and diaz_2007_th7 (u, u², u³ not all in ℒ̃). Parts that need it carry Baker's theorem as a second hypothesis.

Apart from that one derivation, no new mathematics is claimed.

Where the strong six exponentials route stops

DiazModulus.power_hull_strong_six_exp_configuration_iff: for transcendental u and k ≥ 1, a configuration of the strong six exponentials theorem with all six products in Q̄u⁻ᵏ + Q̄u⁻¹ + Q̄ + Q̄u + Q̄uᵏ exists iff k = 2 or k = 3. At a candidate, ℒ̃ contains 1, u and ū = |u|²/u, and with uᵏ also ūᵏ; so the theorem, fed with the candidate's own data, excludes u² and u³ from ℒ̃ and no higher power. The proof counts orders at 0 of polynomials supported on {0, k−1, k, k+1, 2k}. Not found in the sources read; Diaz (2007, p. 390) remarks that inside that theorem one cannot hope to go very far.

No 2×3 configuration on generic data (Theorem A)

DiazModulus.generic_circle_point_no_two_by_three_configuration (4 October 2026): let u ≠ 0 with uū algebraic, and let w₁, …, w_m be numbers such that u, w₁, …, w_m are algebraically independent over Q̄. Then no Q̄-independent x₁, x₂ and y₁, y₂, y₃ have all six products x_i y_j in Q̄ + Q̄u + Q̄ū + ΣQ̄w_j.

For a candidate and logarithms w_j, this means Roy's strong six exponentials theorem cannot refute the candidate on generic data, and neither can any statement whose hypothesis is a rank-one 2×3 configuration, whatever logarithms are added.

• The case m = 0 is Roy's (1995, Th. 3.4).
• The case m = 1, w = iπ is DiazModulus.generic_no_strong_six_exp_configuration.
• The proof is algebra: polynomials of total degree at most two, and the ring map X₀ ↦ 0.

Which four-dimensional extensions carry one (Theorem B)

DiazModulus.circle_point_extension_two_by_three_configuration_iff (5 October 2026): let u ∉ Q̄ with uū algebraic, and z ∉ H₀ = Q̄ + Q̄u + Q̄ū. Then H₀ + Q̄z carries Q̄-independent x₁, x₂ and y₁, y₂, y₃ with all six products in it exactly when z ∈ H₀ + Q̄w for w = u², w = ū² or w = 1/(u − a) with a algebraic and non-zero.

• With Roy's strong six exponentials theorem, these are Diaz's exclusions at a candidate (2007, Cor. 5(1) and 5(4)). Every configuration in such a space is a geometric progression b, bh, bh², bh³, the shape of Fischler (2001, Lemma 6.1) and Diaz (2007, Th. 7(2)).
• The classification was not found in these terms in the sources read, but it is routine: its steps are printed (Bachoc–Serra–Zémor, Lemma 4; for the Möbius step, rank-three quadrics through a rational normal curve: Park 2024, Park–Sim 2025, Arbarello–Harris 1981). Since ℒ̃ is closed under conjugation, z ∈ ℒ̃ brings z̄ with it; the five-dimensional spaces H₀ + Q̄z + Q̄z̄ are the next section.
• Five nodes: the progression lemma, a normal form for cubics with P₁P₂ = P₀², the progression step, the three configurations, and the equivalence.

Five-dimensional spaces that Theorem B cannot see

DiazModulus.circle_point_conjugate_pair_configuration_invisible_to_four_dimensional_extensions (6 October 2026): let u ∉ Q̄ with ρ = uū algebraic, a ∈ Q̄ non-zero, and z = u/(u² − a) if aā ≠ ρ², or z = u/(u² − a)² if aā = ρ². Then W = H₀ + Q̄z + Q̄z̄ carries a configuration (the progression b, bu², bu⁴, bu⁶), but no four-dimensional H₀ + Q̄w inside W does.

• The configuration's shape is printed (Diaz 2004, Th. 2; Diaz 2007, Th. 6(1) and 7(1)), and so are, up to one substitution, its consequences at a candidate: u/(u² − a) ∉ ℒ̃ is Diaz 2004, Th. 2 at x = (u, ū), and u/(u² − a)² ∉ ℒ̃ is Diaz 2007, Th. 6(3) (DiazModulus.candidate_div_sq_sub_not_mem_logAlgTilde).
• What was not found in the sources read is the invisibility to Theorem B's spaces; the proof is short (parity in u).
• For aā = ρ² the conjugation-stable H₀ + Q̄·u/(u² − a) carries none (DiazModulus.conj_stable_circle_point_extension_no_two_by_three_configuration): the conjugate z̄ is what lets the strong six exponentials theorem see u/(u² − a).
• Five nodes: the configuration, the exclusion of u², ū² and 1/(u − b), the invisibility, the contrast, and the exclusions at a candidate.

Separation, a normal form, and Laurent hulls

Eighteen nodes of 8 October 2026 put the previous sections into one mechanism, over any subfield K of ℂ.

• Separation (DiazModulus.rank_one_config_separation): for K ≤ F, a K-space V₀ ⊆ F and w₁, …, w_m algebraically independent over F, every p×q configuration (p, q ≥ 2) in V₀ + Kw₁ + … + Kw_m lies in V₀. The numbers iπ of generic_period_never_enters and the w_j of Theorem A above are cases.
• The normal form (DiazModulus.circle_point_two_by_two_normal_form): for u transcendental over K with uū ∈ K, the 2×2 configurations in H₀ = K + Ku + Kū are exactly x = μ·P(1, u), y = μ⁻¹·Q(1, ū) with P, Q ∈ GL₂(K): one orbit, that of the certificate (1, u) ⊗ (1, ū). Their constant terms form the invertible matrix P·diag(1, ρ)·Q (DiazModulus.circle_point_config_constant_matrix_det_ne_zero), so at a candidate every row and column has an entry outside the Q̄-span of the logarithms (DiazModulus.candidate_two_by_two_config_entry_not_mem_span_logAlg, with Baker's theorem).
• Laurent hulls (DiazModulus.laurent_hull_config_iff): span_K{uˢ : s ∈ S}, S finite, carries a p×q configuration iff S contains a sumset A + B with |A| = p, |B| = q. The power hulls above are the case S = {0, ±1, ±k}. For S = {0, ±1, ±k, ±l} with 4 ≤ k < l, a 2×3 configuration exists iff l ∈ {k+1, k+2, 2k−1, 2k, 2k+1, 3k} (DiazModulus.power_pair_hull_two_by_three_iff); and the hull of {0, ±1} ∪ {±4ʲ : j ≥ 1} carries none (DiazModulus.four_pow_hull_no_two_by_three), so the strong six exponentials theorem, used through Laurent hulls, cannot exclude "u^{4ʲ} ∈ ℒ̃ for all j" at a candidate.
• The tools: the trailing-degree count, linear Cauchy–Davenport in K[X] (a case of Eliahou–Lecouvey, Th. 6.2, as stated in Bachoc–Serra–Zémor 2017, Th. 2), and p + q ≤ dim V₀ + 1 for configurations in K(u).
• Separation, the normal form and the Laurent criterion were not found in the sources read. The pairs of powers excluded at a candidate (DiazModulus.candidate_power_pair_not_both_mem_logAlgTilde) are not claimed: each case is one substitution in Diaz (2007, Cor. 2(P)(1), Th. 7(1), Cor. 5).

Two poles, and Kirby's weak Schanuel conjecture

Seven nodes of 9 October 2026.

• Two poles (DiazModulus.circle_point_two_pole_configuration_invisible_to_four_dimensional_extensions): for u ∉ Q̄ with uū algebraic and any distinct non-zero algebraic a₁, a₂, the space H₀ + Q̄u/(u² − a₁) + Q̄u/(u² − a₂) carries a configuration (the progression b, bu², bu⁴, bu⁶) that no four-dimensional H₀ + Q̄w inside it carries. This drops the conjugation condition of the five-dimensional section's first family and covers the third family, a₁ā₁ = a₂ā₂ = ρ². At a candidate, u/(u² − a₁) and u/(u² − a₂) are not both in ℒ̃, and in the third family their sum is not; both are one substitution in Diaz (2007, Th. 7(2)), which is Fischler (2001, Lemma 6.1), and are not claimed.
• Kirby's weak Schanuel conjecture (Kirby 2018, Conj. 1.5), only its case n = 2, as a hypothesis: every candidate has Im u ∈ πℚ (DiazModulus.candidate_im_mem_pi_rat_of_weak_schanuel), and Diaz's conjecture is equivalent to the single relation "t² + π² is transcendental for real t ≠ 0 with eᵗ algebraic" (DiazModulus.diaz_iff_single_relation_of_weak_schanuel). Not found in the sources read. The weak form says nothing about that relation itself, whose logarithms always satisfy 2·iπ ∈ 2πiℤ.

Every involution of the u-line

Four nodes of 10 October 2026 extend the two-pole spaces to every Möbius involution τ of the u-line.

• τ is given by its pencil q₁, q₂ (coprime quadratics). For non-zero l₁, l₂ in the pencil, the space H₀ + Σᵢ Q̄ q₁(u)ⁱq₂(u)³⁻ⁱ/(u l₁(u) l₂(u)) carries a configuration (the progression with ratio q₁(u)/q₂(u)). It contains none of u², u⁻² and 1/(u − b), so no four-dimensional space of Theorem B inside it carries one (DiazModulus.involution_pencil_configuration_invisible_to_four_dimensional_extensions). τ: u ↦ −u is the previous section.
• Conversely, every five-dimensional space containing a progression with ratio rational in u is visible to Theorem B or of this form (DiazModulus.progression_space_contains_square_or_reciprocal_or_eq_involution_pencil_space, 12 October 2026). The ratio has degree at most 2 (DiazModulus.progression_space_ratio_degree_le_two, through the degree formula in Mathlib's proof of Lüroth's theorem); degree 1 is the next section's index-one node, degree 2 gives the involution space (DiazModulus.quadratic_ratio_progression_space_eq_involution_pencil_space). The progression step is Bachoc–Serra–Zémor (2017, Lemma 4) and stays in the research notes.
• A configuration whose products fill the space can be invisible too: Q̄u⁻¹ + Q̄ + Q̄u + Q̄u³ + Q̄u⁴ (DiazModulus.laurent_case_two_configuration_invisible). That space is not stable under conjugation.
• Not found in the sources read.

Conjugation-stable configurations that are not progressions

Seven nodes of 11 October 2026.

• The family. For u ∉ Q̄, s ∈ Q̄ real with s² = uū, λ ∈ Q̄ with |λ| = 1 and f real, the span of 1, u, ū, f, f/(s + λu) is stable under conjugation and carries the configuration (1, u) ⊗ (u⁻¹, 1, f/(s + λu)) (DiazModulus.conj_stable_real_pencil_space_carries_two_by_three_configuration). Conversely, if 1, u, ū, g, ug are free and ḡ ∈ Q̄ + Q̄u + Q̄ug, the span of 1, u, ū, g, ug is one of these (DiazModulus.conj_equivariant_degree_one_space_eq_real_pencil_space).
• An invisible member with no progression. For λ = 1 and f = u²/s² + s²/u², the space contains none of u², ū² and 1/(u − b), so no four-dimensional space of Theorem B inside it carries a configuration (DiazModulus.real_pencil_quartic_configuration_invisible_to_four_dimensional_extensions). Its polar divisor has degree 5, so it contains no progression: conjugation-stable invisible spaces need not contain a progression.
• At a candidate, under Roy's strong six exponentials theorem, f and f/(|u| + λu) are not both in ℒ̃ (DiazModulus.candidate_real_pencil_not_both_mem_logAlgTilde). This is one substitution in Diaz (2007, Th. 7(1)) and is not claimed.
• Index one is visible. If h is a Möbius function of u and Q̄ + Q̄u + Q̄u⁻¹ + Σ_{k≤3} Q̄ c hᵏ has dimension 5, it contains u², u⁻² or some 1/(u − b) (DiazModulus.mobius_progression_space_contains_square_or_reciprocal). The proof uses only one relation c u p(u) = r(u) between the progression and Q̄ + Q̄u + Q̄u⁻¹, not the divisor argument of the notes.
• Two hypotheses. Kirby's weak Schanuel conjecture for n = 2, with Schanuel's conjecture over the kernel 2πiℚ for n = 1, implies Diaz's conjecture (DiazModulus.diaz_of_weak_schanuel_and_kernel_schanuel). The second hypothesis contains the algebraic independence of e and π, which is open.
• Not found in the sources read, except the candidate statement; all routine.

Case II beyond degree one

Eleven nodes of 14 October 2026 and four of 15 October, from the R12 research notes.

• A space with no factor of degree one. For u ∉ Q̄ and s ∈ Q̄ real with s² = uū, put F = u³/s³ + u²/s². The span of 1, u, ū, F, F̄ is stable under conjugation, the six products of (1, u²) and (ū, u + s, F̄) span it, and it is invisible to Theorem B (DiazModulus.laurent_cubic_configuration_invisible_to_four_dimensional_extensions). No configuration in it has a Möbius ratio (DiazModulus.laurent_cubic_space_no_mobius_ratio_configuration), so it is none of the real pencil spaces above.
• Two orbits of u ↦ −u. The span of 1, u, u⁻¹, α/(u − a) + β/(u + a), γ/(u − b) + δ/(u + b) carries a spanning configuration with factor (1, u²) and is invisible when α ≠ β or γ ≠ δ (DiazModulus.two_orbit_configuration_invisible_to_four_dimensional_extensions); α = β, γ = δ is the two-pole family. With |a| = |b| = |u| and β/α, δ/γ real it is stable under conjugation (DiazModulus.conj_stable_two_orbit_space), and its configuration is then that of Diaz's Théorème 7(1) of 2007 at v = u.
• No factor of degree three or more. If 1, u, u⁻¹ lie in the span of c, ch, ch², ck, chk with h = p(u)/q(u), then max(deg p, deg q) ≤ 2 (DiazModulus.progression_pair_span_ratio_degree_le_two, through the degree formula in Mathlib's proof of Lüroth's theorem).
• Visibility for Laurent f. For a real Laurent polynomial f of width k in u/s, the real pencil space W(λ, f) is invisible when k ≥ 3, or k = 2 and f(−λ̄) ≠ 0, and contains u² when k = 2 and f(−λ̄) = 0 (DiazModulus.laurent_real_pencil_configuration_invisible_to_four_dimensional_extensions, DiazModulus.laurent_real_pencil_space_contains_square_of_root).
• Orbits exchanged by conjugation, and the cyclic case. With g = a₁/(u − a) + a₂/(u + a), |a| ≠ |u| and a₁ ≠ a₂, conjugation exchanges the orbits ±a and ±s²/ā, and the span of 1, u, u⁻¹, g, ḡ is stable under conjugation, carries a spanning configuration and is invisible (DiazModulus.conj_swapped_two_orbit_configuration_invisible_to_four_dimensional_extensions). With v = u/s, the span of 1, u, ū, G₁ = 1/(v − 1) + 2/(v + 1) and G₂ = 1/(v − 1)² + 1/(v − 1) − 2/(v + 1)² + 2/(v + 1) is stable under conjugation and invisible, (1, u²) acts on G₁, G₂ as a Jordan block modulo 1, u, ū, and no configuration in it has a Möbius ratio (DiazModulus.cyclic_pair_configuration_invisible_to_four_dimensional_extensions, DiazModulus.cyclic_pair_space_no_mobius_ratio_configuration). Both configurations are that of Diaz's Théorème 7(1) at v = u, with w = ug and w = uG₂.
• The classification of the degree-two case is formal without conjugation, as Theorem NF below, and the visibility criterion in the form of "Which degree-one spaces Theorem B sees". In the research notes only, not formalised: the three conjugation-stable families of the degree-two case, for every involution of the u-line that commutes with conjugation: two of its orbits fixed or exchanged by conjugation, and a cyclic family. Each family has a formal member above, all for the involution u ↦ −u.
• Not found in the sources read, except the configurations of the conjugation-stable spaces: each is that of Diaz's Théorème 7(1) of 2007 at v = u (for the Laurent cubic space w = u² + su, so F ∉ ℒ̃ at a candidate is one substitution there). What was not found is their invisibility and the absence of Möbius ratios. All routine. At a candidate they add nothing: Roy's theorem already excludes every such space.

Polynomial hulls, and a barrier

Ten nodes of 16 October 2026, from a research note in this repository (tex/diaz-theorem-c.tex, written by Claude agents and refereed by agents and computer algebra; the parts below are now formal).

• Theorem C. For u ∉ Q̄ with uū algebraic and P ∈ Q̄[X], the span of 1, u, ū, P(u), P(u)‾ carries a 2×3 configuration exactly when deg P is 2 or 3 (DiazModulus.polynomial_hull_two_by_three_configuration_iff). The configurations are Diaz's Théorème 7(1) of 2007 (and his Théorème 2 of 2004); the case P = Xᵏ of the converse is the power-hull theorem above. For deg P ≥ 4 the proof counts orders at 0 and degrees together, with DiazModulus.five_point_sumset_rigid and DiazModulus.polynomial_submodule_degrees_card (DiazModulus.polynomial_hull_no_two_by_three_configuration).
• Real polynomials in Re u and Im u with algebraic coefficients carry no configuration in their hull (DiazModulus.real_polynomial_hull_no_two_by_three_configuration, from Theorem B). So at a candidate, Roy's theorem cannot exclude (Re u)² or Re u · Im u from ℒ̃ one number at a time.
• A barrier. Over subfields K ⊆ F, a 2×3 configuration in V₀ + Ku + Ku⁻¹, with V₀ ⊆ F and u transcendental over F, has its products in V₀ (DiazModulus.rank_one_config_inverse_adjoin). So, under Roy's theorem, ℒ̃ + Q̄u + Q̄ū carries no configuration when uū is algebraic and u is transcendental over the field of ℒ̃ (DiazModulus.logAlgTilde_adjoin_circle_point_no_two_by_three_configuration).
• The rest of the research note is formal too: its Theorem E, the classification of all polynomials in u and ū, and the rest of its Theorem D (Baker's and Gel'fond–Schneider's theorems, the six exponentials theorem over Q and the four exponentials theorem in transcendence degree one, in the same model). See below.
• Not found in the sources read, except the configurations of degrees 2 and 3; all routine.

Which degree-one spaces Theorem B sees

Six nodes of 18 October 2026. A degree-one space W_g = span(1, u, ū, g, ug) always carries the configuration (1, u) ⊗ (ū, 1, g). Theorem B sees it through a four-dimensional subspace exactly when u·R(u)·g = N(u) for some R ≠ 0 of degree at most 2 and N of degree at most 3 (DiazModulus.degree_one_space_visible_to_four_dimensional_extensions_iff_cubic_over_quadratic). This is the completeness criterion of the research notes, stated without divisors on P¹, which Mathlib does not have.

• Rational data. For g = P(u)/Q(u) in lowest terms, W_g is visible exactly when max(deg P, deg Q) ≤ 2 + [Q(0) = 0] (DiazModulus.rational_degree_one_space_visible_to_four_dimensional_extensions_iff_natDegree_le).
• Pencil spaces. For W(λ, f) = span(1, u, ū, f, f/(s + λu)) with |λ| = 1 and f = P(u)/Q(u), the bound is max(deg P, deg Q + 1) ≤ 2 + [Q(0) = 0] + [P(−sλ̄) = 0] (DiazModulus.rational_pencil_space_visible_to_four_dimensional_extensions_iff_natDegree_le). For Laurent f it contains DiazModulus.laurent_real_pencil_configuration_invisible_to_four_dimensional_extensions, and it does not need f real.
• Not found in the sources read; all routine.

Polynomials in u and ū: Theorem E

Twenty-five nodes of 18 October 2026, from the research note tex/diaz-theorem-c.tex, whose proof two referee agents checked independently before formalisation. For u ∉ Q̄ with uū algebraic, s = |u| and v = u/s, let z be any polynomial in u and ū with algebraic coefficients, that is, a Laurent polynomial in v, and W = span(1, u, ū, z, z̄) its hull.

• Theorem E. W carries a 2×3 configuration exactly when it is five-dimensional and in one of three classes: (P) it contains αu² + βu³ ≠ 0 (Theorem C's hulls); (Q) a family in the exponents ±2, ±3 with an involution exchanging 0 and ∞; (R) the real pencil spaces with Laurent data of degree at least 2 (DiazModulus.laurent_conj_hull_two_by_three_configuration_iff). The classes are disjoint, and each forces dimension 5.
• Corollary E. If some exponent has absolute value at least 4, only (R) remains; for exponents within ±3, with z ≡ Aū³ + Bū² + Cu² + Du³, N = |A|² − |D|² and Δ = AC̄ − BD̄, a configuration exists exactly when NΔ(|Δ|² − |u|²N²) = 0 (DiazModulus.cubic_window_conj_hull_two_by_three_configuration_iff_criterion).
• At a candidate, under Roy's theorem, no member of the three classes lies in ℒ̃ (DiazModulus.candidate_laurent_conj_hull_class_not_mem_logAlgTilde).
• The formal proof goes pencil by pencil: a configuration factors through a coprime pencil of degree at most 2, one width count rules out two of the four pencils, and the other two give (R) and (Q).
• The configurations are printed or substitutions: (P) is Diaz 2007, Théorème 7(1); (Q) is the configuration of the proof of Diaz 2004, Théorème 2. The "only if" half, the family (Q) and the criterion were not found in the sources read; Theorem E is the second entry of the blueprint's list of results not found and not routine.

Theorem D: what these theorems cannot refute

Sixteen nodes of 18 October 2026, the rest of Theorem D of the research note tex/diaz-theorem-c.tex. Let u be a point of a circle (uū algebraic) that is transcendental over the field generated by ℒ̃; such points exist, since that field is countable. Put ℒ_u = ℒ + ℚu + ℚū.

• Theorem D (DiazModulus.logAlg_adjoin_circle_point_theorem_D). ℒ_u contains ℒ and u, is stable under conjugation, and satisfies, with ℒ replaced by ℒ_u: Baker's theorem, Hermite–Lindemann, Gel'fond–Schneider, the six exponentials theorem over Q and the four exponentials theorem in transcendence degree one; and Roy's theorem for ℒ̃ implies it for ℒ̃_u = Q̄ + Q̄ℒ_u.
• The barrier (DiazModulus.theorem_D_barrier). So some ℚ-space L ⊇ ℒ has all these properties and a non-zero element of algebraic modulus: these theorems, used as properties of (ℒ, ℒ̃) together with conjugation, cannot prove Diaz's conjecture. ℒ itself has the same properties, and the conjecture says exactly that it has no such element (DiazModulus.span_logAlg_theorem_D_properties). The model concerns membership in ℒ only, not the exponential function.
• The six exponentials clause needs neither Roy's theorem nor Gel'fond–Schneider: Baker's theorem for ℒ_u covers the dependent cases, and otherwise the inversion lemma above puts the products in ℒ.
• Each clause restates a classical theorem with ℒ replaced by ℒ_u; not found in the sources read; routine.

Rational functions of u: Theorem F

Twenty-two nodes of 23 October 2026. They take up next step (2) of the research note tex/diaz-theorem-c.tex: Theorem E's question for every z rational in u. Let u ∉ Q̄, and let W be a five-dimensional space containing 1, u and u⁻¹. Say that W satisfies (D1) if t_j and u·t_j lie in W for three independent t_j; (D2a, two-orbit) if W = span(1, u, u⁻¹, Q(u)S₁(u)/(uP(u)), P(u)S₂(u)/(uQ(u))); and (D2b, cyclic) if W = span(1, u, u⁻¹, Q(u)S₁(u)/(uP(u)), Q(u)(Q(u)S₁(u) + P(u)S₂(u))/(uP(u)²)); here P, Q are coprime with max(deg P, deg Q) = 2, and deg S₁, deg S₂ ≤ 2.

• Theorem NF (DiazModulus.degree_two_configuration_normal_form). If W carries a 2×3 configuration whose ratio x₂/x₁ is p(u)/q(u), with p, q coprime and max(deg p, deg q) = 2, then W satisfies (D1), (D2a) or (D2b). W is not assumed to lie in Q̄(u). The proof is elementary: the resultant of the pencil is non-zero, so 1 and J(u)/q(u), for the Wronskian J, are free over Q̄(p(u)/q(u)); at most two values of λ are bad; and multiplication by q(u)/(p(u) − λq(u)) modulo span(1, u, u⁻¹) is a 2×2 matrix over Q̄, scalar, with two eigenvalues, or one Jordan block. The statement is Theorem 2 of the R12 research notes, proved there with vector bundles on P¹.
• Theorem F (DiazModulus.rational_conj_hull_two_by_three_configuration_iff). Let uū be algebraic and z ∈ Q̄(u). The hull W_z = span(1, u, ū, z, z̄) carries a 2×3 configuration exactly when either dim W_z = 4 and z ∈ span(1, u, ū, 1/(u − a)) for some algebraic a with aā = uū, or dim W_z = 5 and W_z satisfies (D1), (D2a) or (D2b). In dimension 5 conjugation plays no part: a five-dimensional W ⊆ Q̄(u) containing 1, u and u⁻¹ carries one exactly when it satisfies (D1), (D2a) or (D2b) (DiazModulus.rational_space_two_by_three_configuration_iff).
• The degree-one case. W satisfies (D1) exactly when it contains u², u⁻² or some 1/(u − a) with a ≠ 0, so that Theorem B sees it, or W = span(1, u, u⁻¹, g, ug) (DiazModulus.degree_one_multiplier_space_visible_or_degree_one_space). If W is also stable under conjugation, it is visible or a real pencil space W(λ, f) (DiazModulus.conj_stable_degree_one_multiplier_space_visible_or_real_pencil_space).
• Theorem F builds on Theorem B. Six more nodes of 23 October 2026 settle what it left open; all six are routine, and none was found in the sources read:
• Agreement with Theorem E (DiazModulus.laurent_conj_hull_configuration_shape_iff_class): for Laurent z with dim W_z = 5, W_z satisfies (D1), (D2a) or (D2b) exactly when it is in class (P), (Q) or (R). The proof goes through Theorem E, so Theorem E's explicit criteria still do not follow from Theorem F.
• (P) is two-orbit (DiazModulus.laurent_polynomial_class_conj_hull_two_orbit_form): a hull of class (P) is the (D2a) space of the pencil (X², 1).
• (Q) is cyclic (DiazModulus.laurent_involution_class_space_cyclic_form): the span of class (Q) is the (D2b) space of the pencil (sX, X² + βs²), where s² = uū.
• (R) is degree one (DiazModulus.laurent_real_pencil_class_space_u_multiplier_triple): in a hull of class (R), (u⁻¹, 1, g) is a free triple whose u-multiple stays in the hull, so (D1) holds.
• Uniqueness in Theorem NF (DiazModulus.degree_two_configuration_multiplier_space_eq): for the ratio h = x₂/x₁ = p(u)/q(u), the f ∈ W with hf ∈ W are exactly x₁·span(y), so the span depends only on W and h.
• At a candidate (DiazModulus.candidate_rational_conj_hull_criterion_not_mem_logAlgTilde): under Roy's theorem, no z ∈ Q̄(u) whose hull meets Theorem F's criterion lies in ℒ̃; each instance is one substitution in Roy's theorem.
• The four-dimensional configuration is printed: rescaled, it is Diaz's Théorème 7(1) of 2007 at v = 1/(u − a), and its exclusion at a candidate is his Corollaire 5(4). When the six products span only four dimensions, the configuration is a progression by Bachoc–Serra–Zémor (2017, Lemma 4). The "only if" half of Theorem F and the proof of Theorem NF without vector bundles were not found in the sources read. Of the literature on scrolls and rank-two bundles on P¹ only a textbook chapter was read (Reid, Chapters on algebraic surfaces, Ch. 2): it prints the ingredients of the bundle proof but not the three shapes. Theorem F with its key step Theorem NF is the third entry of the blueprint's list of results not found and not routine.

Invisible degree-two spaces: Q1.4–Q1.7

Seventeen nodes of 1 November 2026 answer four questions of the R12 research notes about the two-orbit (D2a) and cyclic (D2b) shapes of Theorem NF. In both, P, Q are coprime with max(deg P, deg Q) = 2 and deg S₁, deg S₂ ≤ 2. Say that P and S have a common zero on the projective line if they are not coprime or their coefficients of X² both vanish (a common zero at ∞). "Visible" means visible to the four-dimensional extensions: some w ∈ W outside H₀ = span(1, u, u⁻¹) makes H₀ + Q̄w carry a 2×3 configuration.

• Q1.4, visibility (DiazModulus.two_orbit_space_visible_to_four_dimensional_extensions_iff_common_zero, DiazModulus.cyclic_space_visible_to_four_dimensional_extensions_iff_common_zero; milestones): for uū algebraic and dim W = 5, a two-orbit space is visible exactly when P and S₁, or Q and S₂, have a common zero on the projective line; a cyclic space, exactly when P and S₁ do. Visibility means containing u², u⁻² or some 1/(u − a) with a ≠ 0 (visible_to_four_dimensional_extensions_iff_visible_element_mem, a restatement of Theorem B); the scalar shape is always visible (scalar_quadratic_space_visible_element_mem).
• Q1.5, no degree one (DiazModulus.invisible_two_orbit_space_u_multiplier_space_eq, DiazModulus.invisible_cyclic_space_u_multiplier_space_eq; milestones): with no common zero, W has dimension 5 and the f with f, uf ∈ W are exactly span(1, u⁻¹), so (D1) fails. No hypothesis on uū is needed.
• Q1.6, the involution is unique (DiazModulus.invisible_two_orbit_space_configuration_ratio_mobius, DiazModulus.invisible_cyclic_space_configuration_ratio_mobius; milestones): with no common zero, every configuration in W has ratio x₁/x₀ a Möbius function of P(u)/Q(u), at every position of the orbits, ramified orbits included. Without the hypothesis it fails: span(u⁻², u⁻¹, 1, u, u²) carries ratios u² − u and u², neither a Möbius function of the other.
• Q1.7, conjugation (DiazModulus.conj_stable_invisible_quadratic_space_conj_ratio_mobius; milestone): if such a W is stable under complex conjugation σ, the conjugate of P(u)/Q(u) is a Möbius function of P(u)/Q(u), that is, στσ = τ.
• The tools: binary_quadratic_dvd_of_coprime_mul_eq (Euclid's lemma for binary forms, with formal degrees, so that a zero at ∞ counts), quadratic_space_mem_iff_numerator, u_multiplier_space_le_span_no_degree_one_no_visible_element, quadratic_fraction_extension_visible_element_mem_of_common_zero, degree_two_configuration_pencil_normal_form (Theorem NF with the configuration's own pencil kept), configuration_ratio_quadratic_of_not_degree_one, invisible_two_orbit_space_pole_pencil and invisible_cyclic_space_pole_pencil.

The questions, and proofs of them through orders of poles, are the research notes' (rounds R12 and R20). The formal proofs run on divisibility of binary forms instead of orders of poles. No novelty is claimed: all seventeen are routine. Checked on 1 November 2026 against the literature on products of spaces (Bachoc–Serra–Zémor 2017, Bachoc–Couvreur–Zémor 2018, Couvreur–Zémor 2024, Wessel 2024) and Reid's notes on the cubic scroll S(1, 2): the criterion and Q1.5–Q1.7 were not found in the sources read; Eisenbud–Harris 1987 and Eisenbud's Geometry of Syzygies, Ch. 6, were not read. The 17 modules have 2,805 lines in Diaz/Mirror/; the largest, invisible_cyclic_space_configuration_ratio_mobius, has 304.

The Matrix Coefficient Conjecture sees nothing homogeneous either

• Transcendence.singular_matrix_subspace_annihilating_pair — Roy's lemma (Dasgupta–Kakde II, Thm 2.2; a stronger form is Waldschmidt's book, Prop. 12.5): over an infinite field, a linear space of singular n × n matrices has non-zero v, w with wᵀAv = 0 for all its elements.
• DiazModulus.generic_no_homogeneous_relation — for u and π algebraically independent with |u|² algebraic, no non-zero homogeneous polynomial over Q̄ vanishes at (u, ū, iπ) (an instance of the book's Prop. 12.13).
• DiazModulus.generic_matrix_coefficient_barrier — in that setting every singular n × n matrix over ℚu + ℚū + ℚiπ (resp. Q̄u + Q̄ū + Q̄iπ) has non-zero rational (resp. algebraic) v, w with wᵀMv = 0: the Matrix Coefficient Conjecture of Dasgupta and Kakde, and its Q̄ form, hold on these matrices in every size, as the four exponentials conjecture does at n = 2.

Strong four, sharp four and strong five exponentials

Three nodes of 2026-10-01, each carrying a conjecture as a hypothesis:

• DiazModulus.sharp_four_and_strong_five_exponentials_of_strong_four — the strong four exponentials conjecture (the hypothesis of diaz_of_sfe), with Baker's theorem, implies the sharp four exponentials conjecture, and that one implies the strong five (Waldschmidt's remark, 1988, p. 379). Both conclusions are stated in the forms of diaz_of_sharp_four_exponentials and diaz_of_strong_five_exponentials, and plug into them.
• DiazModulus.algebraic_modulus_log_multiplier_rational_of_sfe — the open question of Waldschmidt's book, p. 399, for every u, from the strong four exponentials conjecture as the book says: if λ ∈ ℒ ∖ {0} and |u|, e^{uλ} are algebraic, then u ∈ ℚ or uλ/λ̄ ∈ ℚ. No Baker.
• DiazModulus.exp_log_mul_log_transcendental_of_strong_five — under the strong five exponentials conjecture, (log a)(log b) ≠ log c for non-zero logarithms (Waldschmidt 1988, p. 379); so e^{λ²} and e^{π²} are transcendental (Waldschmidt 2005).

No new mathematics is claimed for these three.

Diaz's (Qr2) in transcendence degree one

Four nodes of 2 October 2026, from the four exponentials theorem in transcendence degree one:

• DiazModulus.log_mul_real_trichotomy_of_trdeg_one and DiazModulus.log_mul_imaginary_mixed_of_trdeg_one — for non-zero logarithms λ, μ such that λ, λ̄, μ, μ̄ generate a field of transcendence degree at most one: a real product λμ has both factors real, both purely imaginary, or μ ∈ ℚλ̄; a purely imaginary product has one factor on each axis.
• DiazModulus.diaz_2007_qr2_of_trdeg_one — Diaz's conjecture (Qr2) (2007, p. 376) in transcendence degree one: for logarithms ℓ₀, ℓ₁ off both axes, a real or purely imaginary ℓ₁/ℓ₀ is rational.
• DiazModulus.candidate_log_mul_real_iff_rat_conj — for a candidate u and a logarithm μ algebraic over ℚ(u): uμ is real exactly when μ ∈ ℚū, and it is never purely imaginary.

They are immediate from Diaz 2007, who proves (Qr2) from the four exponentials conjecture with the same 2×2 matrix and quotes the theorem in transcendence degree one without combining the two. The transcendence-degree-one form was not found in the sources read.

A dichotomy for Li₂(1/2)

DiazModulus.dilog_half_irrational_or_exp_i_div_pi_transcendental: Li₂(1/2) = π²/12 − (log 2)²/2 is irrational, or e^{iγ/π} is transcendental for every rational γ ≠ 0.

• Waldschmidt lists the irrationality of Li₂(1/2) as unknown (Open Diophantine Problems, 2004, p. 274). Two 2026 preprints report it proved (Tan–Zhang, arXiv:2611.01066; Lai, arXiv:2610.06838), with public Lean developments. The preprints are unrefereed, and this project has not built those developments. If the result stands, the first alternative holds and the corollary says nothing about e^{iγ/π}. The second alternative is open: e^{i/π} is the smallest case of the real half of (S).
• It comes from DiazModulus.recip_pi_log_of_rational_quadratic_relation: if a·t² + b·π² is rational, with a ≠ 0, then e^{iγ/π} is transcendental. That is Brownawell's Corollary 5 (1974) in general form.
• The dichotomy was not found in the sources read.

From the manuscript, through Waldschmidt 1973

Carlo Perassi's unpublished manuscript on the conjecture had three results that seemed to need Roy–Waldschmidt 1997. They are direct instances of Waldschmidt's 1973 Corollaire 4:

• DiazModulus.candidate_pair_dichotomy (Theorem 2.5): two candidates with a rational ratio of squared moduli are rational multiples of each other, or of the conjugate, exactly when they are algebraically dependent;
• DiazModulus.candidate_axis_ratio (Theorem 2.3): for two distinct candidates whose difference is real or purely imaginary, a rational ratio of squared moduli, equal moduli, and v = ±ū are equivalent;
• DiazModulus.candidate_mixed_rigidity (Theorem 3.9): for a candidate u and a logarithm μ outside ℚu ∪ ℚū, the numbers u, μ and e^{uū/μ} generate transcendence degree at least two.

Baker's theorem as a hypothesis, discharged

With Baker's theorem proved, four nodes of 2 October 2026 drop it:

• DiazModulus.no_algebraic_generalized_line_unconditional;
• DiazModulus.candidate_one_log_saturation_unconditional, which drops Hermite–Lindemann as a hypothesis too;
• DiazModulus.no_first_order_arithmetic_operator_unconditional, through DiazModulus.candidate_qbar_independent_one_u_conj: for a candidate u, the numbers 1, u, ū are linearly independent over Q̄, which is Baker's theorem at a candidate.

A barrier: the four exponentials conjecture sees nothing homogeneous

A candidate certifies three logarithms: u, ū and iπ. On them, the four exponentials conjecture (ℚ-independent rows and columns, products in ℒ) is already a theorem, so it can give nothing.

• generic_conj_pair_no_quadratic_relation — if |u|² is algebraic and u, πi are algebraically independent over Q̄, no rational quadratic form vanishes at (u, ū, iπ). It does not use e^u.
• generic_conj_pair_four_exp_barrier — hence every singular 2×2 matrix over ℚu + ℚū + ℚiπ has ℚ-dependent rows or columns. det_zero_linear_forms_rank_one is the classical linear-algebra step.
• candidate_nongeneric_four_exp_barrier — the same conclusion for candidates algebraic over ℚ(π), where the proved four exponentials theorem in transcendence degree one does the work.
• recip_pi_log_four_exp_barrier — the same on ℚ·γ/(iπ) + ℚ·iπ, the data an exception to (S) would certify.

A configuration that does detect a counterexample needs an entry with a constant term, as in diaz_of_sfe. For a generic candidate the constant is all it can add:

• generic_quadratic_relation_is_norm — with algebraic coefficients and a constant coordinate, the only quadratic relation among 1, u, ū, iπ is the norm X₁X₂ − ρX₀², up to a factor.
• generic_period_never_enters — in a singular 2×2 matrix over Q̄ + Q̄u + Q̄ū + Q̄iπ with Q̄-independent rows and columns, the coefficient of iπ in every entry is zero. det_zero_linear_forms_rank_one_field is the linear-algebra step, over any field of characteristic zero.
• generic_qbar_homogeneous_four_exp_barrier — with algebraic coefficients but no constant there is still no 2×2 configuration over Q̄u + Q̄ū + Q̄iπ.
• generic_no_strong_six_exp_configuration — no 2×3 configuration even over Q̄ + Q̄u + Q̄ū + Q̄iπ: the proved strong six exponentials theorem gives nothing against a generic candidate, even with iπ added.

Points of a circle can carry homogeneous relations; candidates cannot. For a candidate algebraic over ℚ(π) with Im u ∉ ℚπ, Théorème 0.2 of Roy–Waldschmidt (Ann. Sci. École Norm. Sup. 30, 1997) excludes every rational quadratic relation among u, ū, iπ. That theorem is not formalised here. What the nodes below add is that no 2×2 configuration sees an anisotropic relation:

• conj_pair_quadratic_relation_iff — for u off the axes with Im u ∉ ℚπ, the rational quadratic relations among u, ū, iπ are exactly the identities Q(Im u, π) = s|u|².
• anisotropic_relation_four_exp_barrier — a relation whose form has no rational zero never yields a configuration, because every 2×2 determinant of rational linear forms has one (det_linear_forms_isotropic). It uses the transcendence of π, not e^u.
• anisotropic_relation_on_circle — such relations occur: Re(u²) = π² at points of every circle of algebraic radius greater than π. By Roy–Waldschmidt, e^u is transcendental at those points, so none of them is a candidate.

Indistinguishability also holds with π fixed:

• circle_points_indistinguishable — two points of a circle, transcendental over a conjugation-stable field K containing the squared radius, are indistinguishable over K.
• exists_noncandidate_transcendental_on_circle — every circle of positive radius has a point transcendental over a given countable field, with e^t transcendental.
• generic_indistinguishable_over_pi — with K the algebraic closure of ℚ(π), a candidate algebraically independent of π cannot be told from a non-candidate point of its circle by any vanishing statement with coefficients in K.

The companion note (since version 1.8) states all of this precisely.

From the literature, formalised

The reading of Diaz, Roy and Waldschmidt on 24 September 2026 produced twelve more nodes, all in Diaz/Mirror/. Most are published results, formalised and attributed as such; two are new couplings.

Known results, now machine-checked:

• exp_abs_transcendental_of_conj_algebraic — for a non-real logarithm λ with λ̄ algebraic over ℚ[λ], e^{|λ|} is transcendental (Diaz 1997, Prop. 2; Roy–Waldschmidt 1997, Cor. 7.4). At λ = iπ it gives e^π. It is the unconditional form of Diaz.log_modulus_forces_independence, which log_modulus_forces_independence_alg (milestone 184) states with that node's hypothesis hMaster dropped.
• exp_abs_log_two_add_i_pi_transcendental — if log 2 is algebraic over ℚ(π), then exp √((log 2)² + π²) is transcendental (Roy–Waldschmidt's example, 1997, p. 792).
• log_pair_square_ratio_transcendental — for ℚ-independent logarithms ℓ₁, ℓ₂ with ℓ₁ algebraic over ℚ[ℓ₂], both e^{ℓ₁²/ℓ₂} and e^{ℓ₂²/ℓ₁} are transcendental (Waldschmidt, LN 402, 1974, p. 202).
• log_two_pi_dependent_forces_transcendence — its case log 2, iπ: if log 2 and π are algebraically dependent, 2^{i log 2/π} and e^{π²/log 2} are transcendental. This strengthens log_two_diaz_or_transcendental.

Weaker published conjectures that already give Diaz's conjecture and (S). Each is inlined as an explicit hypothesis, as the strong four exponentials conjecture is in diaz_of_sfe:

• diaz_of_strong_five_exponentials, recip_pi_not_log_of_strong_five_exponentials — Waldschmidt's strong five exponentials conjecture (1988), which he calls weaker than the strong four exponentials conjecture of that paper: the sharp four exponentials conjecture of the next item, not the hypothesis of diaz_of_sfe. With x₁ = y₁ = 1 its fifth exponential is one of the four.
• diaz_of_sharp_four_exponentials, recip_pi_not_log_of_sharp_four_exponentials — the sharp four exponentials conjecture (Waldschmidt 2005; 1988, p. 377).
• diaz_of_two_by_two_determinant_conjecture, recip_pi_not_log_of_two_by_two_determinant_conjecture — Conjecture 1.6 of Waldschmidt's Further variations on the six exponentials theorem (2005): a 2×2 matrix over ℒ̃ with suitably independent rows and columns has determinant outside ℒ̃. For Diaz the matrix is H(u, |u|).

Two new couplings, both from the four exponentials theorem in transcendence degree one:

• candidate_norm_div_log_not_log — for a candidate u and a logarithm x algebraic over ℚ[u] outside ℚu ∪ ℚū, e^{|u|²/x} is transcendental. It generalises candidate_harmonic_not_log.
• candidate_norm_recip_pi_not_log — its analogue at x = iπ: for every candidate algebraic over ℚ(π), the real half of (S) holds at γ = |u|². A non-generic counterexample to Diaz's conjecture never yields, through its squared modulus, a counterexample to (S).

Five more the same day. They came from a size audit of the library that applied the platform's own rule on how large a helper may be before it becomes a node:

• Transcendence.trdeg_adjoin_le_one_of_isAlgebraic_adjoin — for fields K ⊆ L, elements algebraic over K[x] generate a K-algebra of transcendence degree at most one. Sixteen proofs in this library carry local lemmas of this kind, most written before it became a result; two of October (candidate_im_mem_pi_rat_of_weak_schanuel, diaz_of_weak_schanuel_and_kernel_schanuel) carry copies instead of importing it.
• log_pair_algebraicIndependent_of_mul_eq_rat_pi_sq — Diaz 1997, Proposition 1: if ℓ₁ℓ₂ = cπ² with c ∈ ℚ^× and e^{ℓ₁} not a root of unity, then ℓ₁, ℓ₂ are algebraically independent, and so are ℓ₁, 2πi.
• exp_two_pi_I_mul_transcendental_of_normSq_rat — the case of Diaz's property (4-1) where τ is algebraic over ℚ(π): for non-real τ with |τ|² ∈ ℚ, e^{2πiτ} is transcendental.
• div_not_mem_logAlgTilde_of_sfe — under the strong four exponentials conjecture, Λ₂/Λ₁ ∉ ℒ̃ whenever Λ₁, Λ₂ ∈ ℒ̃ and Λ₁, Λ₂/Λ₁ are transcendental (Waldschmidt 2005, Consequence 1.7). His Consequence 1.6 is the case Λ₂ = 1, and at Λ₁ = iπ it gives 1/(iπ) ∉ ℒ̃.
• e_pi_transcendence — e^π is transcendental (Gelfond 1929), as an instance of the Gelfond–Schneider theorem proved here. It closes another contributor's node, which had been open since June 2026.

On 25 September the same audit took four general results out of proofs that carried them inline, and made each a node:

• exp_abs_transcendental_of_isAlgebraic_adjoin — if e^λ is algebraic, λ is not real, and λ, λ̄ are algebraic over one ring ℚ[x], then e^{|λ|} is transcendental.
• qbar_dependent_of_det_linear_forms — if each product x_i y_j of a 2×2 block is an algebraic linear form in four fixed numbers, and the block's determinant vanishes identically as a quadratic form, then the x's or the y's are linearly dependent over Q̄.
• Transcendence.circle_vanishing_ideal — for a subfield K of ℂ, a point of the circle x² + y² = ρ ≠ 0 whose y is transcendental over K lies on no curve over K except multiples of the circle.
• dvd_of_small_values_at_scale — one scale of Gel'fond's transcendence criterion.

Nine results were proved again, importing these or a node they had re-proved. On the platform those nine proofs went from 2,865 lines to 856. Here, seven mirror modules were regenerated from the new proofs, and Kernel.lean now derives candidate_vanishing_ideal from the circle node: 130 lines instead of 472.

A second wave the same day took apart aligned_norm_free_no_rational_log_matrix, until then a single 1,550-line proof, most of which it never used. It is now 44 lines, from three new nodes:

• Transcendence.quadratic_coeffs_eq_zero_of_transcendental — a transcendental number is a root of no non-zero quadratic with algebraic coefficients.
• four_exp_barrier_of_no_quadratic_relation — if numbers satisfy no rational quadratic relation, a singular 2×2 matrix of rational linear forms in them has rationally dependent rows or columns. The *_four_exp_barrier results each proved this step inline.
• aligned_norm_free_no_quadratic_relation — in the aligned, norm-free case, u, ū and 2πi satisfy no rational quadratic relation.

recip_pi_log_four_exp_barrier, generic_conj_pair_four_exp_barrier and period_free_split_nondegenerate were proved again from them. The four proofs went from 2,725 lines to 320.

A third wave took on the two proofs of Waldschmidt's 1973 Lemmas 4 and 7, aux_linear_system and norm_to_polynomial_alg. Each carried the same 1,046-line block of helpers. Eight nodes replace it:

• Transcendence.length_sum_le and Transcendence.length_mul_le — the length of integer polynomials (the sum of the absolute values of the coefficients) of a finite sum, and of a product.
• Transcendence.exists_int_pow_repr — scaled powers of an algebraic number are integer combinations of a fixed basis, with coefficients at most Aⁿ.
• Transcendence.exists_modByMonic_length_le — reduction modulo any polynomial multiplies the length by at most Cⁿ.
• exists_iteratedDeriv_presentation — the derivatives of an exponential polynomial at a grid point, presented through the four exponentials, for any coefficients. exists_iteratedDeriv_reduced_presentation adds the unknowns and the reduction modulo Q.
• exists_pow_mul_pow_le_exp_sq_mul_sqrt_log — the asymptotic estimate at the scale N²/√log N.
• exists_int_norm — the core of Lemma 7, the norm from ℚ(ω, ω₁) down to ℚ(ω) with size control.

The two proofs went from 4,068 lines to 458, and 2,173 with the new nodes.

A fourth wave took on the remaining proofs of 300 lines or more: extrapolation, siegel_aux, small_irreducible_factor and trdeg_one_presentation in the four exponentials subtree, and the six exponentials steps SX.descent_step and SX.exists_aux_expSum. Eight nodes:

• Transcendence.siegel_entrywise — Siegel's lemma with an entrywise bound: with at least twice as many unknowns as equations and entries at most B, a non-zero integer solution of size at most nB.
• Transcendence.expPoly_grid_estimate — the Cauchy estimate for an exponential polynomial that vanishes to order n on a grid of ℚ-linearly independent points, at any point of a larger grid.
• extrapolation_numbers — the numerical inequality of the four exponentials extrapolation.
• Transcendence.norm_resultant_le_max_norm_eval — a Liouville inequality through the resultant, the complex form of Roy–Waldschmidt 1997, Corollary 3.7.
• Transcendence.exists_irreducible_factor_cofactor_bound — the multiplicative step of Gel'fond's lemma.
• Transcendence.exists_monic_integral_model and Transcendence.exists_monic_integral_model_presentation — finitely many numbers algebraic over ℚ(ω), presented over one monic integral model.
• Transcendence.exists_denom_house_monomial_le — one denominator and a house bound for every monomial of bounded degree in a number field.

The six proofs went from 2,661 lines to 906, and 1,881 with the new nodes.

A fifth wave, on 30 September 2026, took the six proofs still at 300 lines or more, measured on the mirror: …_period_aligned_norm_rat_mult, transfer_breaks_exactly, transcendence_criterion_continuous, construction_growth, expPoly_value_le_derivs and GelfondSchneider.deriv_upper. Most of their length re-proved something that already existed: the non-generic four exponentials barrier, the grid estimate above, or Mathlib (Polynomial.supNorm, StrictMonoOn.Iic_union_Ici, Complex.real_algHom_eq_id_or_conj). One of them carried 183 lines that no theorem used. One node is new: Transcendence.expPoly_iteratedDeriv_le, which bounds every derivative of an exponential polynomial at a point by its first N there, geometrically in the order. The six proofs went from 2,234 lines to 884, and 998 with the node.

What is assumed

Nothing beyond Lean's own three axioms: propext, Classical.choice, Quot.sound. Every theorem in the library depends on those alone, and no sorry appears anywhere; one would show up as sorryAx.

It used to be two more. Axioms.lean imported two classical transcendence results as axiom, with citations, so that #print axioms made the boundary between proved and assumed machine-checkable. Both are now proved, under the same names and with the same statements, so nothing that used them changed.

• hermite_lindemann — if u ≠ 0 and exp u is algebraic, then u is transcendental: the contrapositive of the usual statement. Proved from the Lindemann–Weierstrass development in LindemannWeierstrass.lean, which comes from mathlib PR #28013 by way of a Prove2Me submission. That module depends on Mathlib alone, which is what lets Axioms.lean import it without an import cycle through the rest of the library.
• exists_ringHom_of_transcendental — Steinitz: if u and t are both transcendental over a subfield K of ℂ, some ring endomorphism of ℂ fixes K pointwise and sends u to t. Proved from Mathlib's transcendence bases; the proof was accepted on Prove2Me before it was brought here.

The file keeps its name so the import graph and older references stay stable. It no longer declares anything as an axiom.

A hypothesis is not an axiom. MultiplicityEstimateElem (Diaz/MultiplicityEstimate.lean), like the conjectures above, is a def of a proposition; the results that need it take it as the argument hME, so #print axioms lists only the three axioms for them too. Unlike the conjectures, it is proved: Diaz.multiplicityEstimateElem. The same holds for UnmixedHeight (Diaz/HilbertBox.lean), the argument hU of the Hilbert side of hME, which DiazModulus.unmixedHeight_mvPolynomial proves for polynomial rings over an algebraically closed field. So neither is assumed by Roy's strong six exponentials theorem, Diaz.strongSixExponentials.

Gelfond–Schneider is proved too: GelfondSchneider.gelfond_schneider in Diaz/Mirror/gelfond_schneider.lean. For a non-zero logarithm l of an algebraic number and an algebraic irrational b, exp (b * l) is transcendental. Since 24 September 2026 the proof is a tree of eleven modules, each a Prove2Me node. It restructures the formalization of M. Karatarakis and F. Wiedijk (arXiv:2603.24823; Apache 2.0), which the library first carried as a single 5,388-line module.

Two general tools:

• Transcendence.liouville_house: Liouville's inequality in house form, with an integer denominator;
• Transcendence.expSum_first_nonvanishing: the first non-vanishing derivative of an exponential sum at 1, …, m.

Eight steps of Gelfond's method, in GelfondSchneider.:

• common_field;
• system_entry_house_le;
• aux_coeffs, the Siegel step, through Mathlib's Siegel lemma over rings of integers;
• deriv_identity;
• rho_denominator;
• rho_house_le;
• deriv_upper, through the four exponentials subtree's grid estimate Transcendence.expPoly_grid_estimate;
• main_estimate.

The final theorem assembles the last of these with common_field. All together, 1,409 lines. scripts/gelfond_schneider_port/ still rebuilds the earlier single-file submission from Karatarakis and Wiedijk's sources and lists every change. Its first consumer is salem_quartic_relations_of_logs, the unconditional form of salem_quartic_relations for a real and a purely imaginary logarithm of algebraic numbers. The older statement keeps Gelfond–Schneider as its explicit hypothesis hGS. The others: recip_pi_log_rational_line and recip_pi_log_on_axis (the exceptions to (S) form at most one rational line, lying on an axis), recip_pi_not_log_real_or_imag (the two halves of (S) cannot both fail), and pi_log_two_or_pi_log_three_transcendental. The first three are Diaz's Théorèmes 4 and 5 (J. Théor. Nombres Bordeaux 16, 2004) at v = −1/π. The six exponentials theorem gives two_three_five_pow_pi_transcendental: at least one of 2^π, 3^π, 5^π is transcendental. The five exponentials theorem gives one of 2^π, 3^π (Waldschmidt, New Advances in Transcendence Theory, 1988, (2.2.3)): two_pow_pi_or_three_pow_pi_transcendental ("The five exponentials theorem").

What is not proved

Stated plainly, because an adversarial audit found these and a reader should not have to.

• The transfer of rank and structural rank is not formalized. Only the matrix-coefficient third of "every assertion transfers" is proved. The accompanying note says so explicitly rather than claiming the whole transfer.
• The no-contradiction corollary is not formalized, being a statement about derivations rather than a theorem. What is formalized is what makes it true: the transfer, and the existence of the comparison point.
• The two analytic obstructions are now formalized, as DiazModulus.no_first_order_arithmetic_operator and DiazModulus.kronecker_factorisation in Diaz/Mirror/: the exponential system attached to a candidate admits no first-order arithmetic differential operator, and its interpolation matrix on a Cartesian lattice factors as a Kronecker product with non-zero determinant. Neither needed real analysis in the end. The first is Baker's theorem, carried as an explicit hypothesis until Baker's theorem was proved here (no_first_order_arithmetic_operator_unconditional), plus the fact that a polynomial vanishing on ℤ² is zero; the second is Matrix.det_kronecker and a Vandermonde determinant. The first is stated for polynomial coefficients, where the note states it for rational functions regular on ℤ²; clearing denominators is not formalized.

Caveat on Exponential.lean

Exp0_eq_one_iff and Exp0_pow_eq_one_iff are facts about 2^ℚ, not about the model. The only constraints the model puts on a formal exponential are that it be a homomorphism into the algebraic numbers commuting with the involution, and those are also met by

Exp'(a, b) = exp(2πi(a − b)) · 2^(a+b)

whose values are a root of unity times a rational power of two, hence algebraic, and whose kernel is a rank-one lattice. So a lattice kernel does not by itself escape the model.

Why formalize this rather than the analytic obstructions

Because this is where the error was. An earlier draft described the involution as a Q̄-algebra involution, which asserts that it fixes every algebraic number. It does not — it conjugates them — and the closure theorem does not survive that reading. conj_not_linear_hull is that error stated as a refuted proposition.

The analytic obstructions need real analysis, their formalization cost is high, and their risk is low.

How the model is realised

Rather than building K(T) with σ T = ρ / T, the same configuration is realised inside ℂ: take t transcendental over K on the circle z · conj z = ρ. Then conj t = ρ / t on the nose, so complex conjugation is the involution and none has to be constructed. This also sidesteps a real awkwardness — σ is semilinear, so Mathlib's liftAlgHom does not apply to it.

Method

Almost all of this library was written by AI agents, working on the Prove2Me platform under Carlo Perassi's direction: Anthropic's Claude, run through Claude Code. The agents wrote the Lean statements and proofs, the texts of the platform pages, most of the companion note, the literature checks and two adversarial audits. Carlo chose the problem and the direction, set the rules the agents work under, and approved every publication. Carlo read the statements and the companion note, not the Lean proofs line by line.

Lean checks that every proof proves its statement, with only the three standard axioms. It does not check that a statement says what the cited source says. Agents compared each statement and attribution with the primary sources, often from page images, and several claims of novelty died that way. What survives is what survived that. A reading of the published work of Diaz, Roy, Waldschmidt and Dasgupta–Kakde on 24 September 2026 moved several more results from "possibly known" to known. Since version 1.6, the note and the node texts on the platform attribute each one.

Code written by others is credited where it is used:

• Lindemann–Weierstrass, from Mathlib PR #28013;
• Gelfond–Schneider, from M. Karatarakis and F. Wiedijk;
• eight results contributed to the Diaz mission by the Prove2Me contributor Nickrobbins95 (3–4 October 2026), mirrored here with their proofs: s0_conj_mem, s0_add_mem, s0_rat_scale_mem and s0_bridge_halves_imp_parent on the set S₀ of the statement (S); real_axis_exp_unit_circle, real_axis_root_of_unity_implies_pi_sq_rat and imag_axis_div_normalisation on the axes; and normSq_of_modulus_conjecture;
• construction_count, a counting inequality for the auxiliary construction of the four exponentials proof, proved by the Prove2Me contributor cm_beta (23 September 2026);
• pair_dichotomy_exclusive and conj_combination_off_rays, proved by the Prove2Me contributor amorphic (8 September 2026);
• diaz_of_exp_eq_one, proved by the Prove2Me contributor curiyu (8 September 2026).

e_pi_transcendence answers a node that another Prove2Me contributor posed; its proof is this project's.

Palomar submission surface

This repository also carries the files the Palomar registry requires. The Lean project is at the repository root, so the project path is ..

File	Purpose
Challenge.lean	The advertised statement surface, one deliberate sorry per theorem
Solution.lean	The proved counterparts, delegating to Diaz
comparator.json	The declarations Comparator compares
formalization.yaml	Project metadata to the mathlib-initiative standard
tex/diaz-modulus.tex	The earlier note, on the model and the negative result: the informal account of exactly these statements
LICENSE	Apache-2.0

The compared surface is the axiom-free core: conj_eq_rho_div, eqOn_hull, conj_comm, exists_algHom_of_transcendental, no_vanishing_coeff_matrix, coeff_indistinguishable, with the definitions hull and Hmat. #print axioms on each lists only propext, Classical.choice and Quot.sound.

Two differences from the development described above, both deliberate:

• The existence theorem is proved on K⟮u⟯, not on all of ℂ. Mathlib's RatFunc.algEquivOfTranscendental gives it without the Steinitz axiom, and nothing in the compared surface evaluates the map outside the hull.
• hermite_lindemann and exists_ringHom_of_transcendental, once imported as axioms, are now proved in Diaz/Axioms.lean and used elsewhere in the development. No compared declaration depends on either.

Submissions to Palomar go to https://submit.palomar-registry.org/ and are made by a responsible author or maintainer. Local verification:

lake build                                          # Diaz, Challenge, Solution
ruby scripts/validate-formalization.rb formalization.yaml
./scripts/verify-comparator.sh                      # Linux only: Landrun uses Landlock