Congruence-refined determinant estimates for affine zeros and arbitrary bounded-degree polynomial evaluation columns.

theorem CCDN.primitive_affine_integer_coordinates {n : ℕ} (x : Fin n → ℤ) : Finset.univ.gcd (Fin.cons 1 x) = 1

The homogeneous coordinates (1, x) of an integer point x are primitive: their gcd is 1.

theorem CCDN.exists_affine_congruence_determinant_log_lower {n s N M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin (n + 2)) ℤ) (hir : AbsolutelyIrreducible f) (hd : 0 < f.totalDegree) (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) : ∃ (bad : Finset ℕ), (∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold f.totalDegree < p ∧ HypersurfaceBadReduction (scaledHomogenize f.totalDegree 1 f) p) ∧ hypersurfaceRankLowerBound n s f.totalDegree (∑ p ∈ bad ∪ P, Real.log ↑p / ↑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)))

Homogenization transfers the proved global-plus-congruence estimate without changing a single affine evaluation.