For z ≡ a v̄³ + b v̄² + c v² + d v³ mod span(1, v, v̄), the hull is in the real pencil class exactly when |a c̄ − b d̄| = ||a|² − |d|²| ≠ 0
ProvedDiazModulus.cubic_window_hull_real_pencil_class_iffdiaz-modulus-leannumber-theorytranscendence
Let with . Let and let with , and let (no assumption is made on ). Then with , for some with and some with and , if and only if
Proof. Here with ; write and (the dimension of is not needed: already makes free modulo ). If and are the coefficients of , then for ; multiplied by , , the left side has order at least and the right side degree at most , so both vanish, as is transcendental. Hence and , so , and as ; with the Plücker identities give and , so and . Conversely has ; with , , one has and , and the determinant of this change of basis gives .
Novelty. Not found in the sources read; routine.
Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate
namespace DiazModulus
theorem cubic_window_hull_real_pencil_class_iff
(v : ℂ) (hv : v ∉ Qbar) (hv1 : v * conj v = 1)
(z a b c d : ℂ) (ha : a ∈ Qbar) (hb : b ∈ Qbar) (hc : c ∈ Qbar) (hd : d ∈ Qbar)
(hz : z - (a * conj v ^ 3 + b * conj v ^ 2 + c * v ^ 2 + d * v ^ 3) ∈ Submodule.span Qbar ({1, v, conj v} : Set ℂ)) :
(∃ κ : ℂ, κ ∈ Qbar ∧ κ * conj κ = 1 ∧ ∃ G : Polynomial ↥Qbar, G.coeff 0 = 0 ∧ 2 ≤ G.natDegree ∧
Submodule.span Qbar ({1, v, conj v, z, conj z} : Set ℂ) =
Submodule.span Qbar ({1, v, conj v, Polynomial.aeval v G + κ * conj (v * Polynomial.aeval v G), conj (Polynomial.aeval v G + κ * conj (v * Polynomial.aeval v G))} : Set ℂ)) ↔
((a * conj c - b * conj d) * conj (a * conj c - b * conj d) = (a * conj a - d * conj d) ^ 2 ∧ (a * conj a - d * conj d) ≠ 0) := by
sorry
end DiazModulus
Source
Not found in the sources read. R18 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 18 October 2026 (C. Perassi).