For u ∉ Q̄ with uū algebraic and distinct non-zero algebraic a₁, a₂, the space Q̄ + Q̄u + Q̄ū + Q̄u/(u² − a₁) + Q̄u/(u² − a₂) carries a 2×3 configuration
ProvedDiazModulus.circle_point_two_pole_extension_carries_two_by_three_configurationdiaz-modulus-leannumber-theorytranscendence
Let with algebraic, let be non-zero algebraic numbers, , and . Then there are , linearly independent over , and , linearly independent over , with all six products in .
The configuration is , , : contains the progression . For this is the first family of DiazModulus.circle_point_conjugate_pair_extension_carries_two_by_three_configuration; no conjugation condition is needed here.
Proof. Take and with . The six products are , each in by partial fractions, using : , , , . Both families are free because is transcendental over .
Novelty. Not asserted for the shape: it is the progression of Fischler (2001, Lemma 6.1) and Diaz (2007, Th. 7(2)), with ratio .
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem circle_point_two_pole_extension_carries_two_by_three_configuration (u a₁ a₂ : ℂ)
(hu : u ∉ Qbar) (hρ : IsAlgebraic ℚ (u * conj u)) (ha₁ : a₁ ∈ Qbar) (ha₂ : a₂ ∈ Qbar)
(ha₁0 : a₁ ≠ 0) (ha₂0 : a₂ ≠ 0) (ha : a₁ ≠ a₂) :
∃ (x : Fin 2 → ℂ) (y : Fin 3 → ℂ), LinearIndependent (↥Qbar) x ∧ LinearIndependent (↥Qbar) y ∧
∀ i j, x i * y j ∈ Submodule.span Qbar ({1, u, conj u, u / (u ^ 2 - a₁), u / (u ^ 2 - a₂)} : Set ℂ) := by
sorry
end DiazModulus
Source
The configuration is the progression of S. Fischler, Orbits under algebraic groups and logarithms of algebraic numbers, Acta Arith. 100 (2001), 167–187, Lemma 6.1 (p. 184), repeated in G. Diaz, Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques : conjectures et résultats partiels, J. Théor. Nombres Bordeaux 19 (2007), 373–391, Th. 7(2) (p. 390), with ratio u². R7 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 9 October 2026 (C. Perassi).