For u ∉ Q̄ and real algebraic s with s² = uū, the cyclic space with double poles at ±s is conjugation-stable, spanned by a 2×3 configuration and invisible to Theorem B
ProvedDiazModulus.cyclic_pair_configuration_invisible_to_four_dimensional_extensionsLet and let be real with (so ). With , put and , and let be the -span of (poles at , each a double pole). Then is stable under conjugation, the six products of and span it, and for no outside does carry a configuration.
is the cyclic member of the classification of conjugation-stable invisible spaces with a configuration factor of degree two (research notes R12, Q1.7): the factor acts on modulo as a Jordan block, where R14's two-orbit spaces have two eigenvalues.
Proof. Write . Then and (clear denominators and reduce modulo ), so conjugation maps the five generators into , and induction on the span finishes. The six products of and are , , , , and : all in , and they give back and , so they span . The pair is free as , and is free as the five generators are, both by DiazModulus.cyclic_pair_space_excludes_squares_and_reciprocals. Invisibility: if carries a configuration for some outside , Theorem B puts in with , or ; by exchange , which the same node excludes.
Novelty. The configuration is printed: rescaled by , it is the configuration of Diaz (2007, Th. 7(1)) at , (credited here on 16 October 2026). That no four-dimensional extension of inside carries a configuration was not found in the sources read; routine.
import Definitions.Def_DiazModulus
open Complex ComplexConjugate
namespace DiazModulus
theorem cyclic_pair_configuration_invisible_to_four_dimensional_extensions
(u s : ℂ) (hu : u ∉ Qbar) (hs : s ∈ Qbar) (hsr : conj s = s) (hss : s * s = u * conj u) :
(∀ w ∈ Submodule.span Qbar ({1, u, conj u, (s / (u - s) + 2 * s / (u + s)), (s * s / (u - s) ^ 2 + s / (u - s) - 2 * (s * s) / (u + s) ^ 2 + 2 * s / (u + s))} : Set ℂ), conj w ∈ Submodule.span Qbar ({1, u, conj u, (s / (u - s) + 2 * s / (u + s)), (s * s / (u - s) ^ 2 + s / (u - s) - 2 * (s * s) / (u + s) ^ 2 + 2 * s / (u + s))} : 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, (s / (u - s) + 2 * s / (u + s)), (s * s / (u - s) ^ 2 + s / (u - s) - 2 * (s * s) / (u + s) ^ 2 + 2 * s / (u + s))} : Set ℂ)) ∧
Submodule.span Qbar (Set.range (fun p : Fin 2 × Fin 3 => x p.1 * y p.2)) = Submodule.span Qbar ({1, u, conj u, (s / (u - s) + 2 * s / (u + s)), (s * s / (u - s) ^ 2 + s / (u - s) - 2 * (s * s) / (u + s) ^ 2 + 2 * s / (u + s))} : Set ℂ)) ∧
∀ w ∈ Submodule.span Qbar ({1, u, conj u, (s / (u - s) + 2 * s / (u + s)), (s * s / (u - s) ^ 2 + s / (u - s) - 2 * (s * s) / (u + s) ^ 2 + 2 * s / (u + s))} : 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