GNFS congruence of squares: $\varphi_1(\gamma_1)^2 = \varphi_2(\gamma_2)^2$ in $\mathbb{Z}/n\mathbb{Z}$

Proved

GNFS.congruence_of_squares

by Lucas · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-number-theoryinteger-factorizationnumber-theory

Let $n \in \mathbb{N}$ , $m \in \mathbb{Z}$ , and let $f_1, f_2 \in \mathbb{Z}[x]$ be irreducible in $\mathbb{Z}[x]$ with complex roots $\theta_1, \theta_2$ and a common root $m$ modulo $n$ :

n \mid f_1(m), \qquad n \mid f_2(m).

Let $S$ be a finite set of pairs of integers $(a,b)$ , and suppose $\gamma_1 \in \mathbb{Z}[\theta_1]$ and $\gamma_2 \in \mathbb{Z}[\theta_2]$ satisfy

\gamma_1^2 = \prod_{(a,b)\in S} (a - b\theta_1), \qquad \gamma_2^2 = \prod_{(a,b)\in S} (a - b\theta_2).

Then

there is a ring homomorphism $\varphi_1 : \mathbb{Z}[\theta_1] \to \mathbb{Z}/n\mathbb{Z}$ with $\varphi_1(\theta_1) = m$ ;
there is a ring homomorphism $\varphi_2 : \mathbb{Z}[\theta_2] \to \mathbb{Z}/n\mathbb{Z}$ with $\varphi_2(\theta_2) = m$ ;
for all such homomorphisms, $\varphi_1(\gamma_1)^2 = \varphi_2(\gamma_2)^2$ in $\mathbb{Z}/n\mathbb{Z}$ .

So $x = \varphi_1(\gamma_1)$ and $y = \varphi_2(\gamma_2)$ satisfy $x^2 \equiv y^2 \pmod n$ . This is the congruence of squares produced by the postprocessing step of the general number field sieve.

Formalization Note $\mathbb{Z}[\theta_j]$ is the subring of $\mathbb{C}$ generated by $\theta_j$ . The rational side $g(x) = x - m$ is the case $\theta_2 = m$ , where $\mathbb{Z}[\theta_2] = \mathbb{Z}$ .

Preamble

import Mathlib
import Definitions.Def_GNFS_defs
open Polynomial IntermediateField

Formal statement

namespace GNFS
theorem congruence_of_squares (n : ℕ) (m : ℤ) (f₁ f₂ : ℤ[X])
    (hf₁ : Irreducible f₁) (hf₂ : Irreducible f₂) (θ₁ θ₂ : ℂ)
    (hθ₁ : aeval θ₁ f₁ = 0) (hθ₂ : aeval θ₂ f₂ = 0)
    (hm₁ : (n : ℤ) ∣ f₁.eval m) (hm₂ : (n : ℤ) ∣ f₂.eval m)
    (S : Finset (ℤ × ℤ))
    (γ₁ : Algebra.adjoin ℤ ({θ₁} : Set ℂ)) (γ₂ : Algebra.adjoin ℤ ({θ₂} : Set ℂ))
    (hγ₁ : (γ₁ : ℂ) ^ 2 = ∏ p ∈ S, ((p.1 : ℂ) - (p.2 : ℂ) * θ₁))
    (hγ₂ : (γ₂ : ℂ) ^ 2 = ∏ p ∈ S, ((p.1 : ℂ) - (p.2 : ℂ) * θ₂)) :
    (∃ φ₁ : Algebra.adjoin ℤ ({θ₁} : Set ℂ) →+* ZMod n,
        φ₁ ⟨θ₁, Algebra.self_mem_adjoin_singleton ℤ θ₁⟩ = (m : ZMod n)) ∧
      (∃ φ₂ : Algebra.adjoin ℤ ({θ₂} : Set ℂ) →+* ZMod n,
        φ₂ ⟨θ₂, Algebra.self_mem_adjoin_singleton ℤ θ₂⟩ = (m : ZMod n)) ∧
      ∀ (φ₁ : Algebra.adjoin ℤ ({θ₁} : Set ℂ) →+* ZMod n)
        (φ₂ : Algebra.adjoin ℤ ({θ₂} : Set ℂ) →+* ZMod n),
        φ₁ ⟨θ₁, Algebra.self_mem_adjoin_singleton ℤ θ₁⟩ = (m : ZMod n) →
        φ₂ ⟨θ₂, Algebra.self_mem_adjoin_singleton ℤ θ₂⟩ = (m : ZMod n) →
        φ₁ γ₁ ^ 2 = φ₂ γ₂ ^ 2 := by sorry
end GNFS

Source

Wikipedia, "General number field sieve" (revision oldid=1377718368, https://en.wikipedia.org/w/index.php?title=General_number_field_sieve&oldid=1377718368), section 'Method — Postprocessing'

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

GNFS congruence of squares: φ1(γ1)2=φ2(γ2)2\varphi_1(\gamma_1)^2 = \varphi_2(\gamma_2)^2φ1​(γ1​)2=φ2​(γ2​)2 in Z/nZ\mathbb{Z}/n\mathbb{Z}Z/nZ

GNFS congruence of squares: $\varphi_1(\gamma_1)^2 = \varphi_2(\gamma_2)^2$ in $\mathbb{Z}/n\mathbb{Z}$