A single logarithmic-height witness bounds the combined charge of geometric bad primes and prescribed congruence primes.

theorem CCDN.hypersurface_and_congruence_prime_charge {L : Type u_1} [Field L] [CharZero L] [IsAlgClosed L] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : Irreducible ((MvPolynomial.map (Int.castRingHom L)) f)) (hd : 0 < f.totalDegree) (H : ℝ) (hH : 1 ≤ H) (hcoeff : CoefficientHeightLE f H) (bad P : Finset ℕ) (hbad : ∀ p ∈ bad, stepanovThreshold f.totalDegree < p ∧ HypersurfaceBadReduction f p) (hP : ∀ p ∈ P, Nat.Prime p) : ∑ p ∈ bad ∪ P, Real.log ↑p / ↑p ≤ Real.log (1 + 27 * ↑f.totalDegree ^ 4 * (hypersurfaceHeightConstant (n + 1) * (1 + Real.log H / ↑f.totalDegree ^ 2)) + ∑ p ∈ P, Real.log ↑p) + 2 * mertensError + 1

Multiplying a constructed bad-prime witness by the congruence modulus keeps the combined prime charge within one logarithm of their log heights.