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.