Every five-dimensional span(1, u, u⁻¹, QR₁/(uP), PR₂/(uQ)) with P/Q of degree 2 carries the configuration (1, P/Q) ⊗ (Q/u, R₂/u, QR₁/(uP))
ProvedDiazModulus.quadratic_two_orbit_space_carries_two_by_three_configurationLet be transcendental, that is, (the algebraic numbers); spans and linear independence are over . Let with and , and suppose has dimension . Then and are each linearly independent, and for all .
So every five-dimensional space of shape (D2a) 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 the row gives . Independence of : multiplying by gives , so , then . Independence of : the coefficient of in a relation vanishes; multiplying the relation by gives , so ; then gives . 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_two_orbit_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 P * aeval u R₂ / (u * aeval u Q)} : Set ℂ)) = 5) :
LinearIndependent (↥Qbar) ![1, aeval u P / aeval u Q] ∧
LinearIndependent (↥Qbar) ![aeval u Q / u, aeval u R₂ / u, aeval u Q * aeval u R₁ / (u * aeval u P)] ∧
∀ i j, ![1, aeval u P / aeval u Q] i *
![aeval u Q / u, aeval u R₂ / u, aeval u Q * aeval u R₁ / (u * aeval u P)] j ∈
Submodule.span Qbar ({1, u, u⁻¹, aeval u Q * aeval u R₁ / (u * aeval u P),
aeval u P * aeval u R₂ / (u * aeval u Q)} : Set ℂ) := by
sorry
end DiazModulus