Counting the proper sections attached to one residue-subset edge, including the sum over all smooth residue tuples.

def CCDN.surfaceResidueCrossing {f : MvPolynomial (Fin 3) ℤ} {A B : ℝ} (F : SurfaceCongruenceFamily f B A) (S : Finset (Ideal (CoordinatePolynomial 3))) (R : Finset ℕ) (hR : ∀ p ∈ R, Nat.Prime p) (p : ℕ) (r : SmoothAffineResidueFamily f R) : Set (RatPoint 3)

For a congruence family F, a set R of primes, a prime p and smooth residues r modulo R, the rational points on curves I ∈ S whose ideal contains the auxiliary of R.erase p but not the one of R, and at which the latter auxiliary vanishes.

Equations

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

theorem CCDN.surface_residue_edge_count_le {f : MvPolynomial (Fin 3) ℤ} {A B L X : ℝ} (F : SurfaceCongruenceFamily f B A) (hA : 0 ≤ A) (hB : 1 ≤ B) (hL : 1 ≤ L) (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)) (R : Finset ℕ) (hRW : R ⊆ congruencePrimeWindow L) (hR : ∀ p ∈ R, Nat.Prime p) (p : ℕ) (hp : p ∈ R) (hq : ∏ q ∈ R, ↑q ≤ scalingPrimeRatio * L * X) : ↑(count (⋃ (r : SmoothAffineResidueFamily f R), surfaceResidueCrossing F S R hR p r) B) ≤ 2 * ↑f.totalDegree ^ (R.card + 1) * A ^ 2 * surfaceResidueLogBudget B L ^ 2 * (scalingPrimeRatio * L + 1) ^ 2 * X ^ 2

Summing all smooth residue tuples cancels the square of the modulus. Only d to the number of selected primes remains.