For u ∉ Q̄ and the pencil of any Möbius involution, the space Q̄ + Q̄u + Q̄u⁻¹ + Σ Q̄ q₁(u)ⁱq₂(u)³⁻ⁱ/(u l₁(u)l₂(u)) carries a 2×3 configuration
ProvedDiazModulus.involution_pencil_space_carries_two_by_three_configurationLet . Let be coprime of degree at most , one of them of degree exactly , so that is the pencil of quadratics of a Möbius involution of the -line (its members vanish on the -orbits). Let be non-zero, and let be the -span of and of , . Then there are , free over , and , free over , with all six products in : contains the progression with ratio .
Proof. Put and ; then , , are the four extra spanning elements, so , has all six products in . Since is transcendental, , and are non-zero, and : otherwise as polynomials, against coprimality and the degree condition. So is transcendental, and are free.
Novelty. Not asserted for the shape: it is the progression of Fischler (2001, Lemma 6.1) and Diaz (2007, Th. 7(2)); that a configuration whose products span four dimensions is a progression is Bachoc–Serra–Zémor (2017, Lemma 4).
import Definitions.Def_DiazModulus
open Complex ComplexConjugate
namespace DiazModulus
theorem involution_pencil_space_carries_two_by_three_configuration
(u : ℂ) (hu : u ∉ Qbar) (q₁ q₂ l₁ l₂ : Polynomial ↥Qbar)
(hq₁ : q₁.natDegree ≤ 2) (hq₂ : q₂.natDegree ≤ 2) (hdeg : q₁.natDegree = 2 ∨ q₂.natDegree = 2)
(hcop : IsCoprime q₁ q₂)
(hl₁ : l₁ ∈ Submodule.span ↥Qbar ({q₁, q₂} : Set (Polynomial ↥Qbar))) (hl₁0 : l₁ ≠ 0)
(hl₂ : l₂ ∈ Submodule.span ↥Qbar ({q₁, q₂} : Set (Polynomial ↥Qbar))) (hl₂0 : l₂ ≠ 0) :
∃ (x : Fin 2 → ℂ) (y : Fin 3 → ℂ), LinearIndependent (↥Qbar) x ∧ LinearIndependent (↥Qbar) y ∧
∀ i j, x i * y j ∈ Submodule.span Qbar (({1, u, u⁻¹} : Set ℂ) ∪ Set.range (fun i : Fin 4 =>
Polynomial.aeval u q₁ ^ (i : ℕ) * Polynomial.aeval u q₂ ^ (3 - (i : ℕ)) /
(u * Polynomial.aeval u l₁ * Polynomial.aeval u l₂))) := by
sorry
end DiazModulus