The affine congruence determinant bound with all bad-prime charges controlled by the equation's coefficient height and congruence modulus.

noncomputable def CCDN.congruenceHeightCharge (m d : ℕ) (H Q : ℝ) : ℝ

The logarithmic bad-prime charge in the affine congruence determinant estimate for a form of degree d in m variables with coefficient height at most H, where Q is the sum of the logarithms of the congruence primes.

Equations

• CCDN.congruenceHeightCharge m d H Q = Real.log (1 + 27 * ↑d ^ 4 * (CCDN.hypersurfaceHeightConstant m * (1 + Real.log H / ↑d ^ 2)) + Q) + 2 * CCDN.mertensError + 1

theorem CCDN.affine_congruence_determinant_log_lower_height {n s N M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin (n + 2)) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) (G : Fin N → MvPolynomial (Fin (n + 2)) ℤ) (hG : ∀ (j : Fin N), (G j).totalDegree ≤ M) (x : Fin s → IntPoint (n + 2)) (hx : ∀ (i : Fin s), (MvPolynomial.eval (x i)) f = 0) (hrows : LinearIndependent ℚ ((Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (x i)) (G j)).map Int.cast).row) (P : Finset ℕ) (a : ℕ → IntPoint (n + 2)) (hres : IsSmoothResidueFamily f P a x) : hypersurfaceRankLowerBound n s f.totalDegree (congruenceHeightCharge (n + 3) f.totalDegree H (∑ p ∈ P, Real.log ↑p)) + (hypersurfaceDeterminantMain n s - (↑n + 2) * ↑s) * ∑ p ∈ P, Real.log ↑p ≤ Real.log ↑(Int.Matrix.minorGcd (Matrix.of fun (i : Fin s) (j : Fin N) => (MvPolynomial.eval (x i)) (G j)))

The logarithmic height and modulus are the only equation-dependent errors in the affine smooth-congruence determinant estimate.