A coherent choice of proper auxiliaries for every finite smooth residue family. The structure stores conclusions of the determinant theorem; its existence is proved from the equation.

def CCDN.SmoothAffineResidueFamily.restrict {n : ℕ} {f : MvPolynomial (Fin n) ℤ} {P Q : Finset ℕ} (r : SmoothAffineResidueFamily f P) (hQP : Q ⊆ P) : SmoothAffineResidueFamily f Q

The restriction of a family of smooth residues, indexed by the primes of P, to a subset Q ⊆ P.

Equations

• r.restrict hQP q = r ⟨↑q, ⋯⟩

def CCDN.emptySmoothAffineResidueFamily {n : ℕ} (f : MvPolynomial (Fin n) ℤ) : SmoothAffineResidueFamily f ∅

The unique family of smooth residues indexed by the empty set of primes.

Equations

• CCDN.emptySmoothAffineResidueFamily f p = ⋯.elim

structure CCDN.SurfaceCongruenceFamily (f : MvPolynomial (Fin 3) ℤ) (B A : ℝ) : Type

A choice, for every finite set P of primes and every family r of smooth residues of f modulo the primes of P, of a nonzero integer polynomial that is not divisible by f over ℚ, has degree at most A (B^(1/√d) / ∏ p + 1)(1 + log B + ∑ log p) (with d the degree of f and p ranging over P) and vanishes at every integer zero of f in the box of radius B lying in the residue classes r.

• auxiliary (P : Finset ℕ) : (∀ p ∈ P, Nat.Prime p) → SmoothAffineResidueFamily f P → MvPolynomial (Fin 3) ℤ

  The auxiliary polynomial attached to a set P of primes and smooth residues modulo P.

• nonzero (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (r : SmoothAffineResidueFamily f P) : self.auxiliary P hP r ≠ 0

  Every auxiliary is nonzero.

• proper (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (r : SmoothAffineResidueFamily f P) : ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) (self.auxiliary P hP r)

  No auxiliary is divisible by f over ℚ.

• degree_le (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (r : SmoothAffineResidueFamily f P) : ↑(self.auxiliary P hP r).totalDegree ≤ A * (B ^ (1 / √↑f.totalDegree) / Real.exp (∑ p ∈ P, Real.log ↑p) + 1) * (1 + Real.log B + ∑ p ∈ P, Real.log ↑p)

  The degree of the auxiliary attached to P is at most A (B^(1/√d) / ∏ p + 1)(1 + log B + ∑ log p).

• vanishes (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (r : SmoothAffineResidueFamily f P) (x : IntPoint 3) : x ∈ affineCongruencePoints f B P (smoothResidueIntegerLift r) → (MvPolynomial.eval x) (self.auxiliary P hP r) = 0

  The auxiliary attached to P and r vanishes at the integer zeros of f in the box that lie in the residue classes r.

theorem CCDN.exists_surface_congruence_family (f : MvPolynomial (Fin 3) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) {K H B : ℝ} (hK : 0 ≤ K) (hH : 1 ≤ H) (hB : 1 ≤ B) (hcoeff : CoefficientHeightLE f H) (hheight : Real.log H ≤ K * (Real.log B + 1)) : Nonempty (SurfaceCongruenceFamily f B (surfaceCongruenceDegreeConstant f.totalDegree K))

An absolutely irreducible integer surface equation f of positive degree, whose coefficient height H satisfies log H ≤ K (log B + 1), admits a congruence family of auxiliaries with degree constant surfaceCongruenceDegreeConstant d K, where d is the degree of f.

def CCDN.SurfaceCongruenceFamily.initial {f : MvPolynomial (Fin 3) ℤ} {B A : ℝ} (F : SurfaceCongruenceFamily f B A) : MvPolynomial (Fin 3) ℤ

The auxiliary polynomial of a congruence family attached to the empty set of primes: it vanishes at every integer zero of f in the box.

Equations

• F.initial = F.auxiliary ∅ CCDN.SurfaceCongruenceFamily.initial._proof_1 (CCDN.emptySmoothAffineResidueFamily f)

theorem CCDN.SurfaceCongruenceFamily.initial_eq {f : MvPolynomial (Fin 3) ℤ} {B A : ℝ} (F : SurfaceCongruenceFamily f B A) (r : SmoothAffineResidueFamily f ∅) (hP : ∀ p ∈ ∅, Nat.Prime p) : F.auxiliary ∅ hP r = F.initial

The auxiliary attached to the empty set of primes is F.initial, whatever the (unique) residue family and primality proof.

theorem CCDN.SurfaceCongruenceFamily.initial_vanishes {f : MvPolynomial (Fin 3) ℤ} {B A : ℝ} (F : SurfaceCongruenceFamily f B A) (x : IntPoint 3) (hx : InBox x B) (hxf : (MvPolynomial.eval x) f = 0) : (MvPolynomial.eval x) F.initial = 0

The initial auxiliary F.initial vanishes at every integer zero of f in the box of radius B.

theorem CCDN.SurfaceCongruenceFamily.point_vanishes {f : MvPolynomial (Fin 3) ℤ} {B A : ℝ} (F : SurfaceCongruenceFamily f B A) (x : IntPoint 3) (hx : InBox x B) (hxf : (MvPolynomial.eval x) f = 0) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (hs : ∀ p ∈ P, ∃ (j : Fin 3), (MvPolynomial.eval fun (i : Fin 3) => ↑(x i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0) : (MvPolynomial.eval x) (F.auxiliary P hP (smoothResidueFamilyOfPoint x hxf P hs)) = 0

If an integer zero x of f in the box is a smooth point of f modulo every prime of P, then the auxiliary attached to P and to the residues of x vanishes at x.