Repository navigation
Companion note, version 1.11
Adds three corollaries on rational squared moduli, each machine-checked on 29 September 2026. If t² + π² is rational for a real t ≠ 0 with e^t algebraic, then e^{iγ/π} is transcendental for every rational γ ≠ 0 (Corollary 3.8), so the two remaining open statements cannot both fail at rational data. Logarithms of algebraic numbers that are algebraic over ℚ(π) and have rational squared moduli are rational multiples of one another, up to conjugation (Corollary 6.9). At most one pair ±t makes t² + π² rational; in particular (log 2)² + π² and (log 3)² + π² are not both rational (Corollary 6.10). None was found in the sources read; each follows in a few lines from the four exponentials theorem in transcendence degree one. Section 4 adds a specialisation of Waldschmidt's 1973 theorem, machine-checked with that theorem as a hypothesis: if e^{ir/π} is algebraic for a rational r ≠ 0, two of π, e and e^{π²} are algebraically independent. The mirrored library holds 267 results.