For u ∉ Q̄ and coprime p, q ∈ Q̄[X] of maximal degree 2: a five-dimensional Q̄ + Q̄u + Q̄u⁻¹ + Σ Q̄ c (p(u)/q(u))ᵏ is R9's involution-pencil space for (p, q)
ProvedDiazModulus.quadratic_ratio_progression_space_eq_involution_pencil_spacediaz-modulus-leannumber-theorytranscendence
Let , let be coprime, , let be non-zero, and let be the -span of and . Suppose . If , then is the -span of and , , for some non-zero .
and span the pencil of a Möbius involution of the -line, and these are exactly the spaces of R9, which carry a configuration invisible to Theorem B.
Proof. is transcendental, so are free, and gives two free elements of with : , . Write with coprime of degree at most , and . Then , and have no common zero, so . One has degree , so and is a non-zero constant: with . Splitting over \overline{\mathbb{Q}} gives the pencil members with .
Novelty. Not found in the sources read; it is short.
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem quadratic_ratio_progression_space_eq_involution_pencil_space
(u : ℂ) (hu : u ∉ Qbar) (p q : Polynomial ↥Qbar) (hcop : IsCoprime p q)
(hdeg : max p.natDegree q.natDegree = 2) (c : ℂ) (hc : c ≠ 0)
(hdim : Module.finrank (↥Qbar) (Submodule.span Qbar (({1, u, u⁻¹} : Set ℂ) ∪
Set.range (fun k : Fin 4 => c * (Polynomial.aeval u p / Polynomial.aeval u q) ^ (k : ℕ)))) = 5) :
∃ l₁ l₂ : Polynomial ↥Qbar,
l₁ ∈ Submodule.span ↥Qbar ({p, q} : Set (Polynomial ↥Qbar)) ∧ l₁ ≠ 0 ∧
l₂ ∈ Submodule.span ↥Qbar ({p, q} : Set (Polynomial ↥Qbar)) ∧ l₂ ≠ 0 ∧
Submodule.span Qbar (({1, u, u⁻¹} : Set ℂ) ∪
Set.range (fun k : Fin 4 => c * (Polynomial.aeval u p / Polynomial.aeval u q) ^ (k : ℕ))) =
Submodule.span Qbar (({1, u, u⁻¹} : Set ℂ) ∪ Set.range (fun i : Fin 4 =>
Polynomial.aeval u p ^ (i : ℕ) * Polynomial.aeval u q ^ (3 - (i : ℕ)) /
(u * Polynomial.aeval u l₁ * Polynomial.aeval u l₂))) := by
sorry
end DiazModulus
Source
Not found in the sources read. R13 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 12 October 2026 (C. Perassi).