Prove2Me
Navigate
DiscoverCollectionsFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

For u ∉ Q̄ and the pencil of any Möbius involution, the space Q̄ + Q̄u + Q̄u⁻¹ + Σ Q̄ q₁(u)ⁱq₂(u)³⁻ⁱ/(u l₁(u)l₂(u)) carries a 2×3 configuration

Proved
DiazModulus.involution_pencil_space_carries_two_by_three_configuration

by carlok · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

diaz-modulus-leannumber-theorytranscendence

Let u∈C∖Q‾u \in \mathbb{C} \setminus \overline{\mathbb{Q}}u∈C∖Q​. Let q1,q2∈Q‾[X]q_1, q_2 \in \overline{\mathbb{Q}}[X]q1​,q2​∈Q​[X] be coprime of degree at most 222, one of them of degree exactly 222, so that Λ=Q‾q1+Q‾q2\Lambda = \overline{\mathbb{Q}}q_1 + \overline{\mathbb{Q}}q_2Λ=Q​q1​+Q​q2​ is the pencil of quadratics of a Möbius involution τ\tauτ of the uuu-line (its members vanish on the τ\tauτ-orbits). Let l1,l2∈Λl_1, l_2 \in \Lambdal1​,l2​∈Λ be non-zero, and let WWW be the Q‾\overline{\mathbb{Q}}Q​-span of 1,u,u−11, u, u^{-1}1,u,u−1 and of q1(u)iq2(u)3−i/(u l1(u)l2(u))q_1(u)^iq_2(u)^{3-i}/(u\,l_1(u)l_2(u))q1​(u)iq2​(u)3−i/(ul1​(u)l2​(u)), i=0,…,3i = 0, \dots, 3i=0,…,3. Then there are x1,x2x_1, x_2x1​,x2​, free over Q‾\overline{\mathbb{Q}}Q​, and y1,y2,y3y_1, y_2, y_3y1​,y2​,y3​, free over Q‾\overline{\mathbb{Q}}Q​, with all six products xiyjx_iy_jxi​yj​ in WWW: WWW contains the progression c,cr,cr2,cr3c, cr, cr^2, cr^3c,cr,cr2,cr3 with ratio r=q1(u)/q2(u)r = q_1(u)/q_2(u)r=q1​(u)/q2​(u).

Proof. Put r=q1(u)/q2(u)r = q_1(u)/q_2(u)r=q1​(u)/q2​(u) and c=q2(u)3/(u l1(u)l2(u))c = q_2(u)^3/(u\,l_1(u)l_2(u))c=q2​(u)3/(ul1​(u)l2​(u)); then c rkc\,r^kcrk, k=0,…,3k = 0, \dots, 3k=0,…,3, are the four extra spanning elements, so x=(1,r)x = (1, r)x=(1,r), y=(c,cr,cr2)y = (c, cr, cr^2)y=(c,cr,cr2) has all six products in WWW. Since uuu is transcendental, q2(u)q_2(u)q2​(u), li(u)l_i(u)li​(u) and uuu are non-zero, and r∉Q‾r \notin \overline{\mathbb{Q}}r∈/Q​: otherwise q1=rq2q_1 = r q_2q1​=rq2​ as polynomials, against coprimality and the degree condition. So rrr is transcendental, and 1,r,r21, r, r^21,r,r2 are free.

Novelty. Not asserted for the shape: it is the progression of Fischler (2001, Lemma 6.1) and Diaz (2007, Th. 7(2)); that a configuration whose products span four dimensions is a progression is Bachoc–Serra–Zémor (2017, Lemma 4).

Preamble
import Definitions.Def_DiazModulus
Formal statement
open Complex ComplexConjugate

namespace DiazModulus

theorem involution_pencil_space_carries_two_by_three_configuration
    (u : ℂ) (hu : u ∉ Qbar) (q₁ q₂ l₁ l₂ : Polynomial ↥Qbar)
    (hq₁ : q₁.natDegree ≤ 2) (hq₂ : q₂.natDegree ≤ 2) (hdeg : q₁.natDegree = 2 ∨ q₂.natDegree = 2)
    (hcop : IsCoprime q₁ q₂)
    (hl₁ : l₁ ∈ Submodule.span ↥Qbar ({q₁, q₂} : Set (Polynomial ↥Qbar))) (hl₁0 : l₁ ≠ 0)
    (hl₂ : l₂ ∈ Submodule.span ↥Qbar ({q₁, q₂} : Set (Polynomial ↥Qbar))) (hl₂0 : l₂ ≠ 0) :
    ∃ (x : Fin 2 → ℂ) (y : Fin 3 → ℂ), LinearIndependent (↥Qbar) x ∧ LinearIndependent (↥Qbar) y ∧
      ∀ i j, x i * y j ∈ Submodule.span Qbar (({1, u, u⁻¹} : Set ℂ) ∪ Set.range (fun i : Fin 4 =>
        Polynomial.aeval u q₁ ^ (i : ℕ) * Polynomial.aeval u q₂ ^ (3 - (i : ℕ)) /
          (u * Polynomial.aeval u l₁ * Polynomial.aeval u l₂))) := by
  sorry

end DiazModulus
Source
The configuration is the progression of S. Fischler, Orbits under algebraic groups and logarithms of algebraic numbers, Acta Arith. 100 (2001), 167–187, Lemma 6.1 (p. 184), and G. Diaz, Produits et quotients de combinaisons linéaires de logarithmes de nombres algébriques : conjectures et résultats partiels, J. Théor. Nombres Bordeaux 19 (2007), 373–391, Th. 7(2) (p. 390). R9 of the Diaz modulus mission. Formal proof: Diaz modulus mission, 10 October 2026 (C. Perassi).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me