$c_d\,N(a-b\theta) = b^d f(a/b)$

Proved

GNFS.leadingCoeff_mul_norm_eq_homogenize

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

algebraic-number-theoryinteger-factorizationnumber-theory

Let $f = \sum_{i=0}^d c_i x^i \in \mathbb{Z}[x]$ have degree $d$ and leading coefficient $c_d$ , and suppose $f$ is irreducible over $\mathbb{Q}$ . Let $\theta \in \mathbb{C}$ be a root of $f$ and write $N = N_{\mathbb{Q}(\theta)/\mathbb{Q}}$ for the field norm. Then for all integers $a, b$ ,

c_d \cdot N(a - b\theta) = \sum_{i=0}^{d} c_i a^i b^{d-i} = b^d f(a/b).

In particular, for monic $f$ the sieve value $r = b^d f(a/b)$ is exactly the norm of $a - b\theta$ . This is why smoothness of $r$ controls the factorization of $a - b\theta$ .

Formalization Note The source says " $r$ is a norm of $a-b\theta$ "; this holds exactly for monic $f$ . The statement records the general identity with the factor $c_d$ .

Preamble

import Mathlib
import Definitions.Def_GNFS_defs
open Polynomial IntermediateField

Formal statement

namespace GNFS
theorem leadingCoeff_mul_norm_eq_homogenize (f : ℤ[X])
    (hf : Irreducible (f.map (Int.castRingHom ℚ))) (θ : ℂ) (hθ : aeval θ f = 0) (a b : ℤ) :
    (f.leadingCoeff : ℚ) *
        Algebra.norm ℚ ((a : ℚ⟮θ⟯) - (b : ℚ⟮θ⟯) * AdjoinSimple.gen ℚ θ) =
      (homogenize f a b : ℚ) := 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 — Generation of relation pairs (sieving)'

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

cd N(a−bθ)=bdf(a/b)c_d\,N(a-b\theta) = b^d f(a/b)cd​N(a−bθ)=bdf(a/b)

$c_d\,N(a-b\theta) = b^d f(a/b)$