A small-curve and residual cover for a surface of controlled coefficient height. Both the auxiliaries and the initial prime components are constructed.
theorem
CCDN.exists_surface_initial_curve_components
(f : MvPolynomial (Fin 3) ℤ)
(hirQ : Irreducible ((MvPolynomial.map (Int.castRingHom ℚ)) f))
{A B : ℝ}
(F : SurfaceCongruenceFamily f B A)
:
∃ (S : Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ),
(∀ I ∈ S,
IsSectionCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) ((MvPolynomial.map (Int.castRingHom ℚ)) F.initial) I
(δ I)) ∧ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f) ∩ zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) F.initial) = ⋃ I ∈ S, idealZeroLocus I ∧ ∑ I ∈ S, ↑(δ I) ≤ ↑f.totalDegree * A * (B ^ (1 / √↑f.totalDegree) + 1) * (1 + Real.log B)
The curve components cut out on the surface f = 0 by the initial auxiliary of a
congruence family: height-two primes containing f and the auxiliary, whose zero loci cover
the common zero locus and whose total degree is at most d A (B^(1/√d) + 1)(1 + log B).
theorem
CCDN.exists_surface_small_curve_residual_cover
(f : MvPolynomial (Fin 3) ℤ)
(hir : AbsolutelyIrreducible f)
(hd : 0 < f.totalDegree)
{K H B L X : ℝ}
(hK : 0 ≤ K)
(hheight : Real.log H ≤ K * (Real.log B + 1))
(hW : IsSurfaceResidueWindow f B H L X)
:
∃ (F : SurfaceCongruenceFamily f B (surfaceCongruenceDegreeConstant f.totalDegree K)) (S :
Finset (Ideal (CoordinatePolynomial 3))) (δ : Ideal (CoordinatePolynomial 3) → ℕ),
(∀ I ∈ S,
IsSectionCurve ((MvPolynomial.map (Int.castRingHom ℚ)) f) ((MvPolynomial.map (Int.castRingHom ℚ)) F.initial) I
(δ I)) ∧ ∑ I ∈ S, ↑(δ I) ≤ ↑f.totalDegree * surfaceCongruenceDegreeConstant f.totalDegree K * (B ^ (1 / √↑f.totalDegree) + 1) * (1 + Real.log B) ∧ count (zeroLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B ≤ count (singularHypersurfaceLocus ((MvPolynomial.map (Int.castRingHom ℚ)) f)) B + count
(⋃
I ∈
{I ∈ S |
↑(δ I) ≤ 2 * ↑f.totalDegree * surfaceCongruenceDegreeConstant f.totalDegree K * surfaceResidueLogBudget B L},
idealZeroLocus I)
B + count (surfaceResidueResidualLocus F S L X ⋯) B
A small-curve and residual cover of the integral points of the surface f = 0: they are
singular, lie on a component of degree at most 2 d A Λ(B, L) of the curve cover cut out by the
initial auxiliary, or lie in the residual locus.