The real-axis half implies $\pi^2$ is transcendental

Proved

DiazModulus.pi_sq_transcendental_of_real_gamma

by carlok · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

four-exponentialslogarithmsnumber-theorytranscendence

The real-axis half of DiazModulus.recip_pi_not_log already implies the transcendence of $\pi^2$ .

Let $\gamma_0 = \pi^2$ . If $\pi^2$ were algebraic, then $\gamma_0$ would be a real non-zero algebraic number, while

\frac{\gamma_0}{i\pi} = \frac{\pi}{i} = -i\pi, \qquad e^{-i\pi} = -1,

which is algebraic. Hence the statement that every real non-zero algebraic $\gamma$ has $e^{\gamma/(i\pi)}$ transcendental forces $\pi^2$ --- and therefore $\pi$ --- to be transcendental.

In particular, any proof of the real-axis half DiazModulus.recip_pi_not_log_real_gamma must be at least as strong as $\pi$ -transcendence. The imaginary axis admits no such test point, so this strength floor is specific to the real half.

Formalization Note Lean takes $\gamma_0$ as the real cast of $\pi^2$ and uses $\pi \neq 0$ throughout.

Correction, 2026-09-08: this node carries no information, and should not be built on.

Its conclusion — the transcendence of $\pi^{2}$ — is already an unconditional Proved theorem on this same mission, DiazModulus.pi_sq_transcendental (e40596e3-4cd6-4bf1-81fc-767ea27a5a37), published nine hours before this node. So the implication stated here is vacuously true: it can be proved by discarding its hypothesis entirely and citing that node.

The intent was to record a strength floor — that DiazModulus.recip_pi_not_log_real_gamma is at least as strong as the transcendence of $\pi^{2}$ , via the test point $\gamma_0 = \pi^{2}$ , for which $\gamma_0/(i\pi) = -i\pi$ and $e^{-i\pi} = -1$ is algebraic. The derivation is correct. But a lower bound at a level already reached unconditionally is not a lower bound on anything, so the node does not calibrate the difficulty of its hypothesis and should not be read as doing so.

Kept rather than removed, with this note, because the graph should record what was published.

Preamble

import Definitions.Def_DiazModulus

open Complex ComplexConjugate

Formal statement

namespace DiazModulus
theorem pi_sq_transcendental_of_real_gamma :
    (hS : ∀ γ : ℂ, IsAlgebraic ℚ γ → γ ≠ 0 → γ.im = 0 →
      ¬ IsAlgebraic ℚ (Complex.exp (γ / (((Real.pi : ℝ) : ℂ) * Complex.I)))) →
    Transcendental ℚ ((((Real.pi : ℝ) : ℂ)) ^ 2) := by sorry
end DiazModulus

Source

Observed in the Diaz-modulus mission working notes (Prove2Me mission Diaz, September 2026): the test point gamma = pi^2 gives e^(-i*pi) = -1 by Euler's identity. No literature source; mission-original strength certificate for DiazModulus.recip_pi_not_log_real_gamma.

View graph

The real-axis half implies π2\pi^2π2 is transcendental

The real-axis half implies $\pi^2$ is transcendental