For u ∉ Q̄ and non-zero algebraic a, b, α, β, γ, δ with a² ≠ b², the span of 1, u, u⁻¹, α/(u − a) + β/(u + a), γ/(u − b) + δ/(u + b) is five-dimensional and excludes u², u⁻², 1/(u − c)
ProvedDiazModulus.two_orbit_space_excludes_squares_and_reciprocalsdiaz-modulus-leannumber-theorytranscendence
Let , let with and , put , , and let be the -span of . Then the five numbers are free over , and contains none of , and for non-zero .
Proof. One residue lemma: if with the and all coefficients in \overline{\mathbb{Q}}, clearing denominators gives a polynomial vanishing at the transcendental , hence zero, and its value at gives . Applied at the five distinct poles : in a vanishing combination the residues , , vanish, so the five numbers are free. A membership of or would leave algebraic or a residue at ; one of forces, at (or ), both residues of that pair to match , impossible since , and for any other a sixth pole with residue .
Novelty. Not found in the sources read; it is short.
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem two_orbit_space_excludes_squares_and_reciprocals
(u : ℂ) (hu : u ∉ Qbar) (a b α β γ δ : ℂ) (ha : a ∈ Qbar) (hb : b ∈ Qbar) (hα : α ∈ Qbar) (hβ : β ∈ Qbar)
(hγ : γ ∈ Qbar) (hδ : δ ∈ Qbar) (ha0 : a ≠ 0) (hb0 : b ≠ 0) (hab : a ^ 2 ≠ b ^ 2)
(hα0 : α ≠ 0) (hβ0 : β ≠ 0) (hγ0 : γ ≠ 0) (hδ0 : δ ≠ 0) :
LinearIndependent (↥Qbar) ![1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))] ∧
u ^ 2 ∉ Submodule.span Qbar ({1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))} : Set ℂ) ∧
(u ^ 2)⁻¹ ∉ Submodule.span Qbar ({1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))} : Set ℂ) ∧
∀ e ∈ Qbar, e ≠ 0 → (u - e)⁻¹ ∉ Submodule.span Qbar ({1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))} : Set ℂ) := by
sorry
end DiazModulus
Source
Not found in the sources read. R14 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 14 October 2026 (C. Perassi).