The full standard-monomial prefix produces a proper integer auxiliary on the entire bounded surface congruence class, with the sharp weighted degree in the sole remaining numerical gap.

noncomputable def CCDN.affineCongruencePoints {n : ℕ} (f : MvPolynomial (Fin n) ℤ) (B : ℝ) (P : Finset ℕ) (a : ℕ → IntPoint n) : Finset (IntPoint n)

The integer zeros of f in the box of radius B that are congruent to a p modulo p, coordinatewise, for every p ∈ P.

Equations

• CCDN.affineCongruencePoints f B P a = {x ∈ CCDN.integerBox n B | (MvPolynomial.eval x) f = 0 ∧ ∀ p ∈ P, ∀ (j : Fin n), ↑p ∣ x j - a p j}

theorem CCDN.mem_affineCongruencePoints {n : ℕ} {f : MvPolynomial (Fin n) ℤ} {B : ℝ} {P : Finset ℕ} {a : ℕ → IntPoint n} {x : IntPoint n} : x ∈ affineCongruencePoints f B P a ↔ InBox x B ∧ (MvPolynomial.eval x) f = 0 ∧ ∀ p ∈ P, ∀ (j : Fin n), ↑p ∣ x j - a p j

A point lies in affineCongruencePoints f B P a exactly when it lies in the box of radius B, is a zero of f and is congruent to a p modulo every p ∈ P.

noncomputable def CCDN.surfaceCongruenceRank (f : MvPolynomial (Fin 3) ℤ) (M : ℕ) : ℕ

The number of standard monomials of degree at most M, for the degree-lexicographic order, of the principal ideal generated by the surface equation f over ℚ: the dimension of the space of polynomials of degree at most M modulo f.

Equations

• CCDN.surfaceCongruenceRank f M = (CCDN.standardMonomialPrefix (Ideal.span {(MvPolynomial.map (Int.castRingHom ℚ)) f}) MonomialOrder.degLex M).card

noncomputable def CCDN.surfaceWeightedDeterminantUpper (d s : ℕ) (B : ℝ) : ℝ

The bound log s! + ((2/3) s √(2s/d) + (2d + 2) s) log B for the logarithm of the absolute value of a determinant formed by evaluating s standard monomials of a surface of degree d at s integer points of the box of radius B.

Equations

• CCDN.surfaceWeightedDeterminantUpper d s B = Real.log ↑s.factorial + (2 / 3 * ↑s * √(2 * ↑s / ↑d) + (2 * ↑d + 2) * ↑s) * Real.log B

theorem CCDN.surface_congruence_rank_power_bounds (f : MvPolynomial (Fin 3) ℤ) (hf : f ≠ 0) {M : ℕ} (hM : f.totalDegree ≤ M) : ↑f.totalDegree * (↑M - ↑f.totalDegree + 1) ^ 2 / 2 ≤ ↑(surfaceCongruenceRank f M) ∧ ↑(surfaceCongruenceRank f M) ≤ ↑f.totalDegree * (↑M + 2) ^ 2 / 2

For a nonzero surface equation f of degree d ≤ M, the standard-monomial rank surfaceCongruenceRank f M lies between d (M - d + 1)² / 2 and d (M + 2)² / 2.

theorem CCDN.exists_surface_congruence_auxiliary_of_gap (f : MvPolynomial (Fin 3) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) {M : ℕ} (hM : f.totalDegree ≤ M) {B : ℝ} (hB : 1 ≤ B) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (a : ℕ → IntPoint 3) (ha : ∀ p ∈ P, MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin 3) => ↑(a p j)) f = 0) (hsmooth : ∀ p ∈ P, ∃ (j : Fin 3), (MvPolynomial.eval fun (i : Fin 3) => ↑(a p i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0) (hgap : surfaceWeightedDeterminantUpper f.totalDegree (surfaceCongruenceRank f M) B < affineCongruenceDeterminantLower 1 f.totalDegree (surfaceCongruenceRank f M) H (∑ p ∈ P, Real.log ↑p)) : ∃ (g : MvPolynomial (Fin 3) ℤ), g ≠ 0 ∧ ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ∧ g.totalDegree ≤ M ∧ ∀ x ∈ affineCongruencePoints f B P a, (MvPolynomial.eval x) g = 0

All bounded integer zeros in specified smooth residue classes lie on a proper auxiliary. The degree criterion is entirely numerical.