For u ∉ Q̄ and real algebraic s with s² = uū, the span of 1, u, ū, u³/s³ + u²/s², ū³/s³ + ū²/s² is five-dimensional and contains none of u², ū², 1/(u − b)
ProvedDiazModulus.laurent_cubic_space_excludes_squares_and_reciprocalsdiaz-modulus-leannumber-theorytranscendence
Let and let be real with (so ; with , conjugation acts as on coefficients). Put and let be the -span of (in : ). Then the five numbers are free over , and contains none of , and for non-zero .
Proof. From , and , the number for is a polynomial of degree in with coefficients ; as is transcendental, every coefficient of a vanishing combination is zero. So the five numbers are free; because the and coefficients are tied, and because the and coefficients are; for , the cleared identity at gives .
Novelty. Not found in the sources read; it is short.
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem laurent_cubic_space_excludes_squares_and_reciprocals
(u s : ℂ) (hu : u ∉ Qbar) (hs : s ∈ Qbar) (hsr : conj s = s) (hss : s * s = u * conj u) :
LinearIndependent (↥Qbar) ![1, u, conj u, (u ^ 3 / (s * s * s) + u ^ 2 / (s * s)), (conj u ^ 3 / (s * s * s) + conj u ^ 2 / (s * s))] ∧
u ^ 2 ∉ Submodule.span Qbar ({1, u, conj u, (u ^ 3 / (s * s * s) + u ^ 2 / (s * s)), (conj u ^ 3 / (s * s * s) + conj u ^ 2 / (s * s))} : Set ℂ) ∧
conj u ^ 2 ∉ Submodule.span Qbar ({1, u, conj u, (u ^ 3 / (s * s * s) + u ^ 2 / (s * s)), (conj u ^ 3 / (s * s * s) + conj u ^ 2 / (s * s))} : Set ℂ) ∧
∀ b ∈ Qbar, b ≠ 0 → (u - b)⁻¹ ∉ Submodule.span Qbar ({1, u, conj u, (u ^ 3 / (s * s * s) + u ^ 2 / (s * s)), (conj u ^ 3 / (s * s * s) + conj u ^ 2 / (s * s))} : 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).