The finite residue-edge cover and its complete counting bound.

def CCDN.surfaceResidueSubsetLocus {f : MvPolynomial (Fin 3) ℤ} {A B : ℝ} (F : SurfaceCongruenceFamily f B A) (S : Finset (Ideal (CoordinatePolynomial 3))) (L X : ℝ) (hL : 1 ≤ L) (R : Finset ℕ) : Set (RatPoint 3)

For a subset R of the prime window of logarithmic size L whose product is at most c L X (with c the constant scalingPrimeRatio), the union over the primes p ∈ R and the smooth residue families r modulo R of the crossing sets of the deletion edge R.erase p ⊂ R; the empty set for every other R.

Equations

• One or more equations did not get rendered due to their size.

def CCDN.surfaceResidueResidualLocus {f : MvPolynomial (Fin 3) ℤ} {A B : ℝ} (F : SurfaceCongruenceFamily f B A) (S : Finset (Ideal (CoordinatePolynomial 3))) (L X : ℝ) (hL : 1 ≤ L) : Set (RatPoint 3)

The residual locus of the surface residue cover: the union of the edge crossing sets surfaceResidueSubsetLocus F S L X hL R over all subsets R of the prime window of logarithmic size L.

Equations

• CCDN.surfaceResidueResidualLocus F S L X hL = ⋃ R ∈ (CCDN.congruencePrimeWindow L).powerset, CCDN.surfaceResidueSubsetLocus F S L X hL R

theorem CCDN.surface_residue_residual_count_le {f : MvPolynomial (Fin 3) ℤ} {A B L X : ℝ} (F : SurfaceCongruenceFamily f B A) (hA : 0 ≤ A) (hB : 1 ≤ B) (hL : 1 ≤ L) (hd : 1 ≤ f.totalDegree) (hX0 : 0 ≤ X) (hX : B ^ (1 / √↑f.totalDegree) ≤ X) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ) (hS : ∀ I ∈ S, IsSurfaceCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) I (δ I)) : ↑(count (surfaceResidueResidualLocus F S L X hL) B) ≤ 2 * ↑f.totalDegree * A ^ 2 * surfaceResidueLogBudget B L ^ 2 * (scalingPrimeRatio * L + 1) ^ 2 * X ^ 2 * ↑(congruencePrimeWindow L).card * (2 * ↑f.totalDegree) ^ (congruencePrimeWindow L).card

For an irreducible surface f = 0 of degree d ≥ 1 with curves S, a congruence family F with constant A and a cutoff X ≥ B^(1/√d), the residual locus has at most 2 d A² b² (c L + 1)² X² #W (2d)^#W integral points of height at most B, where b is the logarithmic budget surfaceResidueLogBudget B L, c is scalingPrimeRatio and W is the prime window of logarithmic size L.

theorem CCDN.large_curve_point_mem_surfaceResidueResidualLocus (f : MvPolynomial (Fin 3) ℤ) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f)) {A B H L X : ℝ} (hA : 0 ≤ A) (hW : IsSurfaceResidueWindow f B H L X) (F : SurfaceCongruenceFamily f B A) (S : Finset (Ideal (CoordinatePolynomial 3))) (I : Ideal (CoordinatePolynomial 3)) (hIS : I ∈ S) {d : ℕ} (hI : IsSurfaceCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) I d) (hinitI : (MvPolynomial.map (Int.castRingHom ℚ)) F.initial ∈ I) (hlarge : 2 * ↑f.totalDegree * A * surfaceResidueLogBudget B L < ↑d) (x : IntPoint 3) (hx : InBox x B) (hxf : (MvPolynomial.eval x) f = 0) (hxI : rationalPoint x ∈ idealZeroLocus I) (hsmooth : ∃ (j : Fin 3), (MvPolynomial.eval x) ((MvPolynomial.pderiv j) f) ≠ 0) : rationalPoint x ∈ surfaceResidueResidualLocus F S L X ⋯

An integer point of the box at which the surface f = 0 is nonsingular, lying on a curve I ∈ S that contains the initial auxiliary and has degree greater than 2 d A times the logarithmic budget, belongs to the residual locus surfaceResidueResidualLocus F S L X.