Numerical degree selection for the smooth-congruence auxiliary on a surface. All constants are independent of coefficients and box radius.

noncomputable def CCDN.surfaceCongruenceChargeConstant (d : ℕ) (K : ℝ) : ℝ

A constant, depending on the degree d and the logarithmic height constant K, bounding the height charge of the smooth-congruence determinant estimate for a surface of degree d whose coefficient height H satisfies log H ≤ K (log B + 1).

Equations

• CCDN.surfaceCongruenceChargeConstant d K = Real.log (2 + 27 * ↑d ^ 4 * CCDN.hypersurfaceHeightConstant 4 * (1 + K / ↑d ^ 2)) + 2 * CCDN.mertensError + 1

noncomputable def CCDN.surfaceCongruenceGapConstant (d : ℕ) (K : ℝ) : ℝ

The constant 8 log d + 2 surfaceCongruenceChargeConstant d K + E + 6d + 22, with E the determinant error in dimension one, controlling the numerical gap between the upper and lower bounds for surface congruence determinants.

Equations

• CCDN.surfaceCongruenceGapConstant d K = 8 * Real.log ↑d + 2 * CCDN.surfaceCongruenceChargeConstant d K + CCDN.hypersurfaceDeterminantError 1 + 6 * ↑d + 22

noncomputable def CCDN.surfaceCongruenceDegreeConstant (d : ℕ) (K : ℝ) : ℝ

The constant d + 2 (exp (G / 2) + 1) + 1, with G the gap constant surfaceCongruenceGapConstant d K, which scales the degree of the surface congruence auxiliaries.

Equations

• CCDN.surfaceCongruenceDegreeConstant d K = ↑d + 2 * (Real.exp (CCDN.surfaceCongruenceGapConstant d K / 2) + 1) + 1

theorem CCDN.surfaceCongruenceDegreeConstant_pos (d : ℕ) (K : ℝ) : 0 < surfaceCongruenceDegreeConstant d K

The auxiliary degree constant surfaceCongruenceDegreeConstant d K is positive.

theorem CCDN.exists_surface_congruence_auxiliary (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)) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (a : ℕ → IntPoint 3) (ha : ∀ p ∈ P, MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin 3) => ↑(a p j)) f = 0) (hsmooth : ∀ p ∈ P, ∃ (j : Fin 3), (MvPolynomial.eval fun (i : Fin 3) => ↑(a p i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) f)) ≠ 0) : ∃ (g : MvPolynomial (Fin 3) ℤ), g ≠ 0 ∧ ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ∧ ↑g.totalDegree ≤ surfaceCongruenceDegreeConstant f.totalDegree K * (B ^ (1 / √↑f.totalDegree) / Real.exp (∑ p ∈ P, Real.log ↑p) + 1) * (1 + Real.log B + ∑ p ∈ P, Real.log ↑p) ∧ ∀ x ∈ affineCongruencePoints f B P a, (MvPolynomial.eval x) g = 0

The smooth residue classes have a proper auxiliary of degree O_d,K((B^(1/√d)/exp Q + 1)(1 + log B + Q)).