For u ∉ Q̄ with uū algebraic and the two-orbit space of a, b, α, β, γ, δ with α ≠ β or γ ≠ δ: a spanning 2×3 configuration that no Q̄ + Q̄u + Q̄ū + Q̄w inside it carries
ProvedDiazModulus.two_orbit_configuration_invisible_to_four_dimensional_extensionsLet , let with and , put , , and let be the -span of . Suppose or , and that is algebraic; put . Then the six products of and lie in and span it, and for no outside does carry a configuration.
For , the space is R7's two-pole family, whose configuration is a progression; here the products span the whole space.
Proof. With and : gives , and likewise for , so the six products lie in ; their span contains because or is non-zero, hence equals . is free since , and by DiazModulus.two_orbit_space_excludes_squares_and_reciprocals. Since , every with lies in , and Theorem B (DiazModulus.circle_point_extension_two_by_three_configuration_iff) with exchange would put , (so ) or some in , which the same node excludes.
Novelty. Not found in the sources read; it is short.
import Definitions.Def_DiazModulus
open Complex ComplexConjugate
namespace DiazModulus
theorem two_orbit_configuration_invisible_to_four_dimensional_extensions
(u : ℂ) (hu : u ∉ Qbar) (a b α β γ δ : ℂ) (ha : a ∈ Qbar) (hb : b ∈ Qbar) (hα : α ∈ Qbar) (hβ : β ∈ Qbar)
(hγ : γ ∈ Qbar) (hδ : δ ∈ Qbar) (ha0 : a ≠ 0) (hb0 : b ≠ 0) (hab : a ^ 2 ≠ b ^ 2)
(hα0 : α ≠ 0) (hβ0 : β ≠ 0) (hγ0 : γ ≠ 0) (hδ0 : δ ≠ 0)
(hαγ : α ≠ β ∨ γ ≠ δ) (hρ : IsAlgebraic ℚ (u * conj u)) :
(∃ (x : Fin 2 → ℂ) (y : Fin 3 → ℂ), LinearIndependent (↥Qbar) x ∧ LinearIndependent (↥Qbar) y ∧
(∀ i j, x i * y j ∈ Submodule.span Qbar ({1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))} : Set ℂ)) ∧
Submodule.span Qbar (Set.range (fun p : Fin 2 × Fin 3 => x p.1 * y p.2)) = Submodule.span Qbar ({1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))} : Set ℂ)) ∧
∀ w ∈ Submodule.span Qbar ({1, u, u⁻¹, (α / (u - a) + β / (u + a)), (γ / (u - b) + δ / (u + b))} : Set ℂ), w ∉ Submodule.span Qbar ({1, u, conj u} : Set ℂ) →
¬ ∃ (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, w} : Set ℂ) := by
sorry
end DiazModulus