Auxiliary polynomials from the competing congruence determinant lower bound and weighted archimedean upper bound.

noncomputable def CCDN.affineCongruenceDeterminantLower (n d s : ℕ) (H Q : ℝ) : ℝ

The lower bound for the logarithm of a nonzero s × s determinant of monomials evaluated at integral zeros of an absolutely irreducible affine equation of degree d in n + 2 variables with coefficient height at most H, when the zeros lie in smooth residue classes modulo primes whose logarithms sum to Q.

Equations

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

theorem CCDN.exists_affine_congruence_auxiliary_of_gap {n N t M : ℕ} (hN : 0 < N) (f : MvPolynomial (Fin (n + 2)) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) (mon : Fin N → Fin (n + 2) →₀ ℕ) (hmon : Function.Injective mon) (hstd : ∀ (j : Fin N), mon j ∈ (Ideal.span {(MvPolynomial.map (Int.castRingHom ℚ)) f}).standardExponents MonomialOrder.degLex) (hdegree : ∀ (j : Fin N), Finsupp.degree (mon j) ≤ M) {B : ℝ} {x : Fin t → IntPoint (n + 2)} (hxB : IsBoxZeroFamily f B x) (P : Finset ℕ) (a : ℕ → IntPoint (n + 2)) (hres : IsSmoothResidueFamily f P a x) (hgap : Real.log ↑N.factorial + (∑ j : Fin N, ↑(Finsupp.degree (mon j))) * Real.log B < affineCongruenceDeterminantLower n f.totalDegree N H (∑ p ∈ P, Real.log ↑p)) : ∃ (g : MvPolynomial (Fin (n + 2)) ℤ), g ≠ 0 ∧ ¬(MvPolynomial.map (Int.castRingHom ℚ)) f ∣ (MvPolynomial.map (Int.castRingHom ℚ)) g ∧ g.totalDegree ≤ M ∧ ∀ (i : Fin t), (MvPolynomial.eval (x i)) g = 0

The determinant gap yields an integer auxiliary, proper over the rationals, for every given finite family of points in the residue classes.