Integral norm polynomials and the two signed plane equations needed to count square-norm generators. The norm polynomial retains the full number-field degree even when its parameter lies in a proper subfield.

noncomputable def CCDN.integerNormPolynomial (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) : Polynomial ℤ

The integer norm polynomial of β ∈ 𝓞 K: the characteristic polynomial of multiplication by β, whose value at x ∈ ℤ is the norm N(x - β).

Equations

• CCDN.integerNormPolynomial K β = LinearMap.charpoly ((Algebra.lmul ℤ (NumberField.RingOfIntegers K)) β)

theorem CCDN.integerNormPolynomial_monic (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) : (integerNormPolynomial K β).Monic

The integer norm polynomial of an algebraic integer is monic.

theorem CCDN.integerNormPolynomial_natDegree (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) : (integerNormPolynomial K β).natDegree = Module.finrank ℚ K

The integer norm polynomial of an algebraic integer of K has degree [K : ℚ].

theorem CCDN.integerNormPolynomial_eval (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) (x : ℤ) : Polynomial.eval x (integerNormPolynomial K β) = (Algebra.norm ℤ) ((algebraMap ℤ (NumberField.RingOfIntegers K)) x - β)

The integer norm polynomial of β evaluated at x ∈ ℤ is the norm N(x - β).

noncomputable def CCDN.signedNormCurvePolynomial (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) (ε : ℤ) : MvPolynomial (Fin 2) ℤ

The signed norm-curve polynomial y ^ 2 - ε * N(x - β) in the plane coordinates (y, x), where N(x - β) is the integer norm polynomial of β: on an integral point the first coordinate is a square root of the norm and the second is the integral translation parameter.

Equations

• CCDN.signedNormCurvePolynomial K β ε = (CCDN.bivariatePolynomialEquiv ℤ).symm (Polynomial.X ^ 2 - Polynomial.C (Polynomial.C ε * CCDN.integerNormPolynomial K β))

theorem CCDN.square_norm_yields_signedNormCurve_point (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) (x : ℤ) (m : ℕ) (h : ((Algebra.norm ℤ) ((algebraMap ℤ (NumberField.RingOfIntegers K)) x - β)).natAbs = m ^ 2) : (MvPolynomial.eval ![↑m, x]) (signedNormCurvePolynomial K β 1) = 0 ∨ (MvPolynomial.eval ![↑m, x]) (signedNormCurvePolynomial K β (-1)) = 0

If |N(x - β)| = m ^ 2, then (m, x) is an integral point on one of the two signed norm curves y ^ 2 = N(x - β) or y ^ 2 = -N(x - β).