Every five-dimensional span(1, u, u⁻¹, QR₁/(uP), Q(QR₁ + PR₂)/(uP²)) with P/Q of degree 2 carries a 2×3 configuration with ratio P/Q
ProvedDiazModulus.quadratic_cyclic_space_carries_two_by_three_configurationLet be transcendental, that is, (the algebraic numbers); spans and linear independence are over . Let with and , put and , and suppose has dimension . Then and are each linearly independent, and for all .
So every five-dimensional space of shape (D2b) carries a configuration with ratio . and need not be coprime.
Proof. Write and . As has dimension , the family is independent; in particular , so . Every with lies in , so a relation forces and . The products are explicit (values at ): , and , while the row gives . Independence of : multiplying by gives , so . Independence of : a relation reads , so and , whence . No transcendence is used beyond .
Novelty. Not found in the sources read; routine. Explicit identities: the existence of a configuration is the easy direction; the classification is Theorem NF (DiazModulus.degree_two_configuration_normal_form).
import Definitions.Def_DiazModulus
open Complex ComplexConjugate
namespace DiazModulus
open Polynomial in
theorem quadratic_cyclic_space_carries_two_by_three_configuration (u : ℂ) (hu : u ∉ Qbar)
(P Q R₁ R₂ : (↥Qbar)[X]) (hdeg : max P.natDegree Q.natDegree = 2)
(hR₁ : R₁.natDegree ≤ 2) (hR₂ : R₂.natDegree ≤ 2)
(h5 : Module.finrank (↥Qbar) (Submodule.span Qbar ({1, u, u⁻¹, aeval u Q * aeval u R₁ / (u * aeval u P),
aeval u Q * (aeval u Q * aeval u R₁ + aeval u P * aeval u R₂) / (u * aeval u P ^ 2)} : Set ℂ)) = 5) :
LinearIndependent (↥Qbar) ![1, aeval u P / aeval u Q] ∧
LinearIndependent (↥Qbar) ![aeval u Q / u, aeval u Q * aeval u R₁ / (u * aeval u P),
aeval u Q * (aeval u Q * aeval u R₁ + aeval u P * aeval u R₂) / (u * aeval u P ^ 2)] ∧
∀ i j, ![1, aeval u P / aeval u Q] i *
![aeval u Q / u, aeval u Q * aeval u R₁ / (u * aeval u P),
aeval u Q * (aeval u Q * aeval u R₁ + aeval u P * aeval u R₂) / (u * aeval u P ^ 2)] j ∈
Submodule.span Qbar ({1, u, u⁻¹, aeval u Q * aeval u R₁ / (u * aeval u P),
aeval u Q * (aeval u Q * aeval u R₁ + aeval u P * aeval u R₂) / (u * aeval u P ^ 2)} : Set ℂ) := by
sorry
end DiazModulus