Analytic control of bad-prime charges from an integer witness. The construction and coefficient bound for a Noether witness remain separate.

theorem CCDN.prime_divisor_log_sum_le (P : Finset ℕ) {D : ℤ} (hD : 0 < D) (hP : ∀ p ∈ P, Nat.Prime p) (hdiv : ∀ p ∈ P, ↑p ∣ D) : ∑ p ∈ P, Real.log ↑p ≤ Real.log ↑D

Distinct prime divisors of a positive integer have total logarithmic weight at most the logarithm of that integer.

theorem CCDN.prime_divisor_charge_le (P : Finset ℕ) {D : ℤ} (hD : 0 < D) (hP : ∀ p ∈ P, Nat.Prime p) (hdiv : ∀ p ∈ P, ↑p ∣ D) {T : ℝ} (hT : 0 < T) (hlo : ∀ p ∈ P, T ≤ ↑p) : ∑ p ∈ P, Real.log ↑p / ↑p ≤ Real.log ↑D / T

Above a cutoff T, the reciprocal-weighted charge costs at most log(D)/T.

theorem CCDN.bad_prime_charge_of_height (P : Finset ℕ) {D : ℤ} (hD : 0 < D) (hP : ∀ p ∈ P, Nat.Prime p) (hdiv : ∀ p ∈ P, ↑p ∣ D) {L H : ℝ} (hL : 1 ≤ L) (hH : 1 ≤ H) (hlo : ∀ p ∈ P, L < ↑p) (hheight : Real.log ↑D ≤ L * H) : ∑ p ∈ P, Real.log ↑p / ↑p ≤ Real.log H + 2 * mertensError + 1

A logarithmic-height bound for an integer witness controls the bad-prime charge at the scale of the cutoff. Constructing such a witness is algebraic.

theorem CCDN.bad_prime_factor_of_height (P : Finset ℕ) {D : ℤ} (hD : 0 < D) (hP : ∀ p ∈ P, Nat.Prime p) (hdiv : ∀ p ∈ P, ↑p ∣ D) {L H : ℝ} (hL : 1 ≤ L) (hH : 1 ≤ H) (hlo : ∀ p ∈ P, L < ↑p) (hheight : Real.log ↑D ≤ L * H) : primeSetFactor P ≤ Real.exp (2 * mertensError + 1) * H

The exponential bad-prime factor has linear dependence on the scaled logarithmic height of a nonzero integer witness.