The global determinant bound with simultaneous smooth congruence conditions. Bad reductions and local exponents are derived from the equation.

Congruence-refined global hypersurface determinant bounds.

theorem CCDN.exists_smooth_congruence_determinant_log_lower {K : Type u_1} [Field K] [CharZero K] [IsAlgClosed K] {n s N d M : ℕ} (hs : 0 < s) (f : MvPolynomial (Fin (n + 3)) ℤ) (hf : f.IsHomogeneous d) (hd : 0 < d) (hir : Irreducible ((MvPolynomial.map (Int.castRingHom K)) f)) {F : Fin N → MvPolynomial (Fin (n + 3)) ℤ} {z : Fin s → IntPoint (n + 3)} (hev : IsIndependentEvaluation f M F z) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) (k : ℕ → Fin (n + 3)) (a : ℕ → Fin (n + 2) → ℤ) (ha : ∀ p ∈ P, MvPolynomial.eval₂ (Int.castRingHom (ZMod p)) (fun (j : Fin (n + 2)) => ↑(a p j)) (projectiveHypersurfaceChart (k p) f) = 0) (hsmooth : ∀ p ∈ P, ∃ (j : Fin (n + 2)), (MvPolynomial.eval fun (i : Fin (n + 2)) => ↑(a p i)) ((MvPolynomial.pderiv j) ((MvPolynomial.map (Int.castRingHom (ZMod p))) (projectiveHypersurfaceChart (k p) f))) ≠ 0) (hunit : ∀ p ∈ P, ∀ (i : Fin s), IsCoprime (↑p) (z i (k p))) (hres : ∀ p ∈ P, ∀ (i : Fin s) (j : Fin (n + 2)), ↑p ∣ z i ((Equiv.swap 0 (k p)) j.succ) - a p j * z i (k p)) : ∃ (bad : Finset ℕ), (∀ (p : ℕ), p ∈ bad ↔ stepanovThreshold d < p ∧ HypersurfaceBadReduction f p) ∧ hypersurfaceRankLowerBound n s d (∑ 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 (z i)) (F j)))

The global determinant contribution and all prescribed smooth-prime contributions hold simultaneously.