Companion note, version 1.24

Version 1.24 answers the question Remark 5.10 left open, and adds two formal results around it.

• Proposition 5.11. 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)); conversely, every space Q̄ + Q̄u + Q̄ū + Q̄g + Q̄ug whose configuration conjugation maps to one of the same shape is of this form. For λ = 1 and f = u²/s² + s²/u² the space contains none of u², ū², 1/(u − b), so no four-dimensional space of Theorem 5.5 inside it carries a configuration, and it contains no progression. At a candidate, under Roy's theorem, f and f/(|u| + λu) are not both in ℒ̃: one substitution in Diaz 2007, Th. 7(1).
• Remark 5.10. Its index-one step is now formal: a five-dimensional space containing a progression whose ratio is a Möbius function of u contains u², u⁻² or some 1/(u − b).
• Remark 2.3. Kirby's weak Schanuel conjecture for n = 2, with Schanuel's conjecture over the kernel 2πiℚ for n = 1, implies Diaz's conjecture; formal. The second hypothesis contains the algebraic independence of e and π, which is open.

Statements (i)–(iii) of Proposition 5.11 and the index-one step were not found in the sources read; they are short. Seven new formal results (milestones 121–125 on the Diaz mission); the mirrored project holds all 400.

Companion note, version 1.23

Version 1.23 extends Proposition 5.8 from the involution u ↦ −u to every Möbius involution of the u-line.

• Theorem 5.9. For u ∉ Q̄ with ρ = uū algebraic, let q₁, q₂ ∈ Q̄[X] be coprime quadratics (the orbit pencil of an involution τ) and l₁, l₂ non-zero members of the pencil. The space Q̄ + Q̄u + Q̄ū + Σᵢ Q̄ q₁(u)ⁱq₂(u)³⁻ⁱ/(u l₁(u) l₂(u)) carries a 2×3 configuration and contains none of u², ū², 1/(u − b), so no four-dimensional space of Theorem 5.5 inside it carries one.
• Remark 5.10. Conversely (proved in the text, not formalised), every five-dimensional space that contains a four-term progression and is invisible to Theorem 5.5 is of this form; the progression step is Bachoc–Serra–Zémor, Lemma 4. A configuration whose products fill the space can be invisible too (Q̄u⁻¹ + Q̄ + Q̄u + Q̄u³ + Q̄u⁴, not stable under conjugation). Not found in the sources read.

Four new formal results (milestones 119–120 on the Diaz mission); the mirrored project holds all 393.

Companion note, version 1.22

Version 1.22 adds two short results and makes one remark formal.

• Proposition 5.8. For u ∉ Q̄ with ρ = uū algebraic and distinct non-zero algebraic a₁, a₂, the space Q̄ + Q̄u + Q̄ū + Q̄u/(u² − a₁) + Q̄u/(u² − a₂) carries a 2×3 configuration, but no four-dimensional Q̄ + Q̄u + Q̄ū + Q̄w inside it does; no conjugation condition is needed, and the third family of Remark 5.7 is the case a₁ā₁ = a₂ā₂ = ρ². At a candidate, under Roy's theorem, the two terms are not both in ℒ̃, and in the third family their sum is not: one substitution in Diaz 2007, Théorème 7(2) (Fischler 2001, Lemma 6.1), not claimed.
• Remark 2.3 is now formal: under the case n = 2 of Kirby's weak Schanuel conjecture, every candidate has Im u ∈ πℚ, and Diaz's conjecture is equivalent to the single relation of Theorem 3.5 (t² + π² transcendental for real t ≠ 0 with eᵗ algebraic).

Seven new formal results (milestones 116–118 on the Diaz mission); the mirrored project holds all 389.

Companion note, version 1.21

Version 1.21 puts the rank-one results of Section 5 into one mechanism, over any subfield K of ℂ.

• Theorem 5.12. Separation: numbers algebraically independent over F never enter a p×q configuration (p, q ≥ 2) in V₀ + Kw₁ + … + Kw_m with V₀ ⊆ F. Near a point of a circle, configurations in K + Ku + Kū have p + q ≤ 4, and the 2×2 ones are exactly x = μ·P(1, u), y = μ⁻¹·Q(1, ū) with P, Q ∈ GL₂(K). With generic numbers added they stay 2×2, their constant terms form an invertible matrix, and at a candidate every row and column has an entry outside the Q̄-span of the logarithms.
• Proposition 5.13. A Laurent hull span{uˢ : s ∈ S} carries a p×q configuration iff S contains a sumset A + B with |A| = p, |B| = q. For {0, ±1, ±k, ±l}, 4 ≤ k < l, a 2×3 configuration exists iff l ∈ {k+1, k+2, 2k−1, 2k, 2k+1, 3k}; the hull of {0, ±1} ∪ {±4ʲ} carries none.
• Remark 5.14. The pairs of powers excluded at a candidate are substitutions in Diaz 2007; linear Cauchy–Davenport is a case of Eliahou–Lecouvey, as stated by Bachoc–Serra–Zémor. Separation, the normal form and the Laurent criterion were not found in the sources read.
• Theorem 4.1 (no vanishing coefficient) now assumes only u ∉ K, as its Lean statement does.

Eighteen new formal results (milestones 111–115 on the Diaz mission); the mirrored project holds all 382.

Companion note, version 1.20

Version 1.20 adds the five-dimensional case left open by Theorem 5.5.

• Proposition 5.6. For u ∉ Q̄ with ρ = uū algebraic and a ∈ Q̄ non-zero, let z = u/(u² − a) if aā ≠ ρ², or z = u/(u² − a)² if aā = ρ². Then W = Q̄ + Q̄u + Q̄ū + Q̄z + Q̄z̄ carries a 2×3 configuration, but no four-dimensional space Q̄ + Q̄u + Q̄ū + Q̄w inside it does; and for aā = ρ² the conjugation-stable space Q̄ + Q̄u + Q̄ū + Q̄·u/(u² − a) carries none.
• Remark 5.7. The configuration's shape is printed (Diaz 2004, Théorème 2; Diaz 2007, Théorèmes 6(1) and 7(1)), and so are, up to one substitution, its consequences at a candidate: u/(u² − a) ∉ ℒ̃ is Diaz 2004, Théorème 2 at x = (u, ū), and u/(u² − a)² ∉ ℒ̃ is Diaz 2007, Théorème 6(3). That the configuration is invisible to the four-dimensional spaces of Theorem 5.5 was not found in the sources read.
  Five new formal results (milestones 108–110 on the Diaz mission); the mirrored project holds all 364.

Companion note, version 1.19

Version 1.19 adds two remarks from a check of the 24 September literature sweep.

• Remark 2.3. Kirby's weak form of Schanuel's conjecture (J. Kirby, Variants of Schanuel's conjecture, arXiv:1801.08765, Conjecture 1.5) forces Im u ∈ πℚ at a candidate. So under it Diaz's conjecture is equivalent to statement (ii) of Theorem 3.5: t² + π² is transcendental for every real t ≠ 0 with e^t algebraic. The weak form says nothing about that statement itself, nor about (S). This reduction was not found in the sources read.
• Section 4. For 2×2 matrices, the extension of the Matrix Coefficient Conjecture to ℚ + ℒ that Dasgupta and Kakde expect is the sharp four exponentials conjecture with rational constants (Waldschmidt, Hopf algebras and transcendental numbers, p. 4). It would settle the candidates with |u|² ∈ ℚ, and (S) for rational γ.
  No new formal results; the mirrored project still holds all 359.

Companion note, version 1.18

Version 1.18 records what the batch of 5 October 2026 machine-checks.

• Theorem 5.5. Let u ∉ Q̄ with uū algebraic, and z ∉ H₀ = Q̄ + Q̄u + Q̄ū. Then H₀ + Q̄z carries a rank-one 2×3 configuration (two Q̄-independent x_i, three Q̄-independent y_j, all six products x_i y_j in the space) 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, Corollaire 5(1) and 5(4)).
  • Every configuration in such a space is a geometric progression b, bh, bh², bh³, the shape of Fischler's Lemma 6.1 (2001) and Diaz's Théorème 7(2) (2007).
  • The classification was not found in the sources read. A hypothesis z ∈ ℒ̃ brings z̄ with it, and the five-dimensional spaces H₀ + Q̄z + Q̄z̄ are not covered.
• Appendix A. One new row, with the five Lean identifiers of the theorem and its steps. The mirrored project holds all 359 proved results of the development.

Companion note, version 1.17

Version 1.17 records what the batch of 4 October 2026 machine-checks.

• Proposition 3.9 and Corollary 3.10. If a·t² + b·π² is rational for a real logarithm t ≠ 0 of an algebraic number, with a ≠ 0, then e^{iγ/π} is transcendental for every rational γ ≠ 0.
  • Hence Li₂(1/2) = π²/12 − (log 2)²/2 is irrational, or e^{iγ/π} is transcendental for every rational γ ≠ 0. Both alternatives are open.
  • The proposition is Brownawell's Corollary 5 (1974) in general form.
• Theorem 5.4. On generic data no rank-one 2×3 configuration has its products in Q̄ + Q̄u + Q̄ū + ΣQ̄w_j. Generic data means u ≠ 0 with uū algebraic and numbers w_j such that u, w₁, …, w_m are algebraically independent.
  • So Roy's strong six exponentials theorem cannot refute a candidate on generic data, whatever logarithms are added.
• Corollaries 6.11 and 6.12 and Theorem 6.13. These are Theorems 2.5, 2.3 and 3.9 of the author's manuscript, as direct instances of Waldschmidt's 1973 Corollaire 4.
• Credits. Brownawell's 1974 Corollaries 5 and 7 are credited where they apply, and so is M. Karatarakis's Lean formalisation of Baker's theorem along the same route.
• Appendix A. Six new rows. 121 identifiers were checked against the platform, with 0 mismatches, and the mirrored project holds all 346 proved results.

Companion note, version 1.16

Version 1.16 records what the batches of 2 October 2026 machine-check.

• Baker's theorem, in its qualitative inhomogeneous form, is now proved in the formal development, along the route of Bertrand and Masser in Chapter 4 of Waldschmidt's book: the criterion of Schneider–Lang for ℂ^{d₀} × (ℂ^×)^{d₁}, d₀ ≤ 1, with a Schwarz lemma for Cartesian products. Section 1 says so, and the four appendix rows that had read "Proved, assuming Baker" now name unconditional forms and read Proved.
• A new subsection, "Products on the axes", adds Proposition 6.11, Theorem 6.12 and Corollary 6.13: Diaz's conjecture (Qr2) of 2007 in transcendence degree one, with the classification of real and purely imaginary products of two logarithms behind it, and the case of a candidate. They are immediate from Diaz's own argument with the four exponentials theorem in transcendence degree one in place of the conjecture; that combination was not found in the sources read.
• The title of Brownawell's 1974 paper is corrected.

The appendix was checked against the live board (115 identifiers, no mismatch); the Lean project holds all 340 proved results.

Companion note, version 1.15

Version 1.15 records what the third batch of 1 October 2026 machine-checks. Each result carries a conjecture as a hypothesis.

• The strong four exponentials conjecture (Conjecture 1.2), with Baker's theorem, implies the sharp four exponentials conjecture, and that one implies Waldschmidt's strong five exponentials conjecture. Item (2) of Section 7 is corrected: Waldschmidt's 1988 remark that the strong five is "clearly" weaker compares it with the sharp four (that paper's "strong four"), not with Conjecture 1.2. The order the list claims now has a proof.
• The second open statement on p. 399 of Waldschmidt's book follows from Conjecture 1.2 in full, without Baker's theorem: if λ ∈ ℒ ∖ {0} and |u|, e^{uλ} are algebraic, then u ∈ ℚ or uλ/λ̄ ∈ ℚ.
• Under the strong five exponentials conjecture, (log a)(log b) ≠ log c for non-zero logarithms (Waldschmidt 1988), so e^{λ²} and e^{π²} are transcendental.
• One sentence in Section 5: the homogeneous form of the conjecture on algebraic independence of logarithms holds at a generic candidate's own logarithms u, ū, iπ, so it cannot refute a generic candidate through them.

No new mathematics is claimed. The mirrored library holds 307 results.