A nonsingular point on a large-degree initial curve must cross a proper auxiliary section along a one-prime deletion edge. This constructs the residual cover from smooth reductions and auxiliaries.

noncomputable def CCDN.surfaceResidueLogBudget (B L : ℝ) : ℝ

The quantity 1 + log B + (log 4 + 4) c L, with c the constant scalingPrimeRatio, which bounds 1 + log B + ∑ p ∈ R, log p for every set R of primes in the prime window of logarithmic size L.

Equations

• CCDN.surfaceResidueLogBudget B L = 1 + Real.log B + (Real.log 4 + 4) * CCDN.scalingPrimeRatio * L

structure CCDN.IsSurfaceResidueWindow (f : MvPolynomial (Fin 3) ℤ) (B H L X : ℝ) : Prop

The parameters of the residue cover of the surface f = 0 in the box of radius B ≥ 1: the coefficients of f are bounded by H ≥ 1; the logarithmic prime window L ≥ 1 dominates 4 log(d + 1) + log H + d log B, which bounds the logarithm of a partial derivative of f at a point of the box, where d is the degree of f; and the residue-modulus cutoff X satisfies 1 < X, B^(1/√d) ≤ X and X ≤ e^L.

• one_le_radius : 1 ≤ B

  The box radius is at least one.

• one_le_height : 1 ≤ H

  The height bound is at least one.

• one_le_window : 1 ≤ L

  The logarithmic size of the prime window is at least one.

• coeff_le : CoefficientHeightLE f H

  The coefficients of f are bounded by H in absolute value.

• log_le_window : 4 * Real.log (↑f.totalDegree + 1) + Real.log H + ↑f.totalDegree * Real.log B ≤ L

  The window dominates the logarithmic size of a partial derivative of f on the box.

• one_lt_cutoff : 1 < X

  The modulus cutoff exceeds one.

• root_le_cutoff : B ^ (1 / √↑f.totalDegree) ≤ X

  The modulus cutoff is at least B^(1/√d).

• cutoff_le_exp : X ≤ Real.exp L

  The modulus cutoff is at most exp L.

theorem CCDN.exp_sum_log_primes (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) : Real.exp (∑ p ∈ P, Real.log ↑p) = ∏ p ∈ P, ↑p

For a finite set P of primes, the exponential of ∑ p ∈ P, log p is ∏ p ∈ P, p.

structure CCDN.IsSurfaceResidueEdge {f : MvPolynomial (Fin 3) ℤ} {A B : ℝ} (F : SurfaceCongruenceFamily f B A) (I : Ideal (CoordinatePolynomial 3)) (L X : ℝ) (x : IntPoint 3) (R : Finset ℕ) (hR : ∀ p ∈ R, Nat.Prime p) (p : ℕ) (r : SmoothAffineResidueFamily f R) : Prop

A one-prime deletion edge R.erase p ⊂ R of the congruence family F, at the smooth residues r, crossing the curve I near the point x: the primes of R lie in the window of log-size L, the modulus of R is less than c L X and that of R.erase p is less than X (where c is scalingPrimeRatio), the parent auxiliary lies in I, the child auxiliary does not, and the child vanishes at x.

• subset_window : R ⊆ congruencePrimeWindow L

  The primes of R lie in the prime window of logarithmic size L.

• prod_lt : ∏ q ∈ R, ↑q < scalingPrimeRatio * L * X

  The product of the primes of R is less than c L X, with c the constant scalingPrimeRatio.

• erase_prod_lt : ∏ q ∈ R.erase p, ↑q < X

  The product of the primes of R.erase p is less than X.

• parent_mem : (MvPolynomial.map (Int.castRingHom ℚ)) (F.auxiliary (R.erase p) ⋯ (r.restrict ⋯)) ∈ I

  The auxiliary attached to R.erase p, over ℚ, lies in the ideal I of the curve.

• child_not_mem : (MvPolynomial.map (Int.castRingHom ℚ)) (F.auxiliary R hR r) ∉ I

  The auxiliary attached to R, over ℚ, does not lie in the ideal I.

• child_vanishes : (MvPolynomial.eval x) (F.auxiliary R hR r) = 0

  The auxiliary attached to R vanishes at x.

theorem CCDN.surface_residue_boundary_of_large_curve (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) (I : Ideal (CoordinatePolynomial 3)) {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) (hsmooth : ∃ (j : Fin 3), (MvPolynomial.eval x) ((MvPolynomial.pderiv j) f) ≠ 0) : ∃ (R : Finset ℕ) (hR : ∀ p ∈ R, Nat.Prime p), ∃ p ∈ R, ∃ (r : SmoothAffineResidueFamily f R), IsSurfaceResidueEdge F I L X x R hR p r

A point on an initial prime curve above the terminal degree cutoff lies in a proper section across a bounded-modulus residue edge.