Counting the bounded square-norm integers in the absence of an index-two subfield. Ordinary norm curves and small-subfield exceptions are both counted by proved estimates.

Uniform counts for signed norm curves whose parameter generates a subfield of odd index. The ambient field degree may be even.

noncomputable def CCDN.oddIndexNormCurveCountConstant : ℝ

The absolute constant in the count of integral points on signed norm curves whose parameter generates a subfield of odd index.

Equations

• CCDN.oddIndexNormCurveCountConstant = 2 * Real.exp 1 * CCDN.affineNonzeroConstantBound CCDN.planeResidueConstant

theorem CCDN.signed_norm_curve_count_of_odd_subfield_index (K : Type u_1) [Field K] [NumberField K] (β : NumberField.RingOfIntegers K) {ε : ℤ} (hε : ε ≠ 0) (hn : 2 ≤ Module.finrank ℚ K) (hindex : Odd (Module.finrank (↥ℚ⟮↑β⟯) K)) {B : ℝ} (hB : 1 ≤ B) : ↑(count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) (signedNormCurvePolynomial K β ε))) B) ≤ oddIndexNormCurveCountConstant * ↑(Module.finrank ℚ K) ^ 3 * B ^ (1 / ↑(Module.finrank ℚ K)) * (Real.log B + ↑(Module.finrank ℚ K))

If [K : ℚ(β)] is odd, n = [K : ℚ] ≥ 2 and ε ≠ 0, then the signed norm curve y ^ 2 = ε * N(x - β) has at most C * n ^ 3 * B ^ (1 / n) * (log B + n) integral points of height at most B ≥ 1.

noncomputable def CCDN.noIndexTwoCurveContributionConstant (n : ℕ) : ℝ

The degree-dependent constant bounding the contribution of one integer-translation class to the bounded square-norm count for fields of degree n without an index-two subfield.

Equations

• CCDN.noIndexTwoCurveContributionConstant n = 8 * CCDN.oddIndexNormCurveCountConstant * ↑n ^ 4

theorem CCDN.noIndexTwoCurveContributionConstant_nonneg (n : ℕ) : 0 ≤ noIndexTwoCurveContributionConstant n

The constant noIndexTwoCurveContributionConstant n is nonnegative.

theorem CCDN.boundedSquareNormIntegers_no_index_two_count (K : Type u_1) [Field K] [NumberField K] (hnoTwo : ∀ (L : IntermediateField ℚ K), Module.finrank (↥L) K ≠ 2) (hn : 2 ≤ Module.finrank ℚ K) {B : ℝ} (hB : 1 ≤ B) : ↑(boundedSquareNormIntegers K B).ncard ≤ ↑(boundedSmallSubfieldIntegers K B).ncard + noIndexTwoCurveContributionConstant (Module.finrank ℚ K) * ↑(boundedSquareNormTranslationClasses K B).card * √B * (Real.log B + 1)

For a number field of degree n ≥ 2 without an intermediate field of index two and B ≥ 1, the number of bounded square-norm integers is at most the number of bounded integers in small subfields plus C(n) times the number of translation classes times √B * (log B + 1).