Concrete integer-translation fibers of the bounded square-norm set inject into integral points on the two signed norm curves.

The first counting reduction for two-torsion ideal classes: inject them into the finite set of bounded algebraic integers whose absolute norm is a square. Both possible signs of the signed norm are retained.

def CCDN.boundedSquareNormIntegers (K : Type u_1) [Field K] (B : ℝ) : Set (NumberField.RingOfIntegers K)

The set of nonzero algebraic integers β ∈ 𝓞 K bounded by B at every infinite place whose absolute norm |N(β)| is a perfect square.

Equations

• CCDN.boundedSquareNormIntegers K B = {β : NumberField.RingOfIntegers K | β ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ↑β ≤ B) ∧ ∃ (m : ℕ), ((Algebra.norm ℤ) β).natAbs = m ^ 2}

theorem CCDN.boundedSquareNormIntegers_finite (K : Type u_1) [Field K] [NumberField K] (B : ℝ) : (boundedSquareNormIntegers K B).Finite

There are finitely many bounded square-norm integers boundedSquareNormIntegers K B.

theorem CCDN.classGroupTwoTorsionCard_le_boundedSquareNormIntegers (K : Type u_1) [Field K] [NumberField K] : classGroupTwoTorsionCard K ≤ (boundedSquareNormIntegers K (9 * |↑(NumberField.discr K)| ^ (1 / ↑(Module.finrank ℚ K)))).ncard

The two-torsion subgroup of the class group of K has at most as many elements as there are bounded square-norm integers at the balanced radius 9 * |discr K| ^ (1 / [K : ℚ]); the injection sends each class to a balanced generator of the square of a representative ideal.

def CCDN.squareNormTranslateFiber (K : Type u_1) [Field K] (β : NumberField.RingOfIntegers K) (B : ℝ) : Set (NumberField.RingOfIntegers K)

The bounded square-norm integers of the form x - β with x ∈ ℤ, that is, those in the integer-translation class of -β.

Equations

• CCDN.squareNormTranslateFiber K β B = {α : NumberField.RingOfIntegers K | α ∈ CCDN.boundedSquareNormIntegers K B ∧ ∃ (x : ℤ), α = (algebraMap ℤ (NumberField.RingOfIntegers K)) x - β}

theorem CCDN.squareNormTranslateFiber_finite (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) (B : ℝ) : (squareNormTranslateFiber K β B).Finite

Each square-norm translate fiber squareNormTranslateFiber K β B is finite.

def CCDN.signedNormCurveLocus (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) (ε : ℤ) : Set (RatPoint 2)

The rational plane curve y ^ 2 = ε * N(x - β) cut out by the signed norm-curve polynomial of β with sign ε.

Equations

• CCDN.signedNormCurveLocus K β ε = CCDN.zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) (CCDN.signedNormCurvePolynomial K β ε))

theorem CCDN.squareNormTranslateFiber_count_le (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) {B : ℝ} (hβ : ∀ (w : NumberField.InfinitePlace K), w ↑β ≤ B) : (squareNormTranslateFiber K β B).ncard ≤ count (signedNormCurveLocus K β 1) (max (2 * B) √(B ^ Module.finrank ℚ K)) + count (signedNormCurveLocus K β (-1)) (max (2 * B) √(B ^ Module.finrank ℚ K))

If β is bounded by B at every infinite place, then the square-norm translate fiber of β has at most as many elements as there are integral points of height at most max (2 * B) (√(B ^ n)) on the two signed norm curves y ^ 2 = ±N(x - β), where n = [K : ℚ].