The restricted discriminant after progression substitution

theorem NairTenenbaum.PolynomialSystem.affine_discriminant {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) : (P.affine q a hq hqa).discriminant = q ^ (P.radical.natDegree * (P.radical.natDegree - 1)) * P.discriminant

Absolute-value form of equation (38).

theorem NairTenenbaum.PolynomialSystem.affine_badDiscriminant_factorization {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) (p : ℕ) : (P.affine q a hq hqa).badDiscriminant.factorization p = if p ∣ q then 0 else P.badDiscriminant.factorization p

The new powers of primes dividing q do not enter the restricted bad discriminant, since the transformed polynomial has no roots there.

theorem NairTenenbaum.PolynomialSystem.affine_badDiscriminant_dvd {k r : ℕ} (P : PolynomialSystem k r) (q : ℕ) (a : ℤ) (hq : q ≠ 0) (hqa : q.Coprime (Polynomial.eval a P.total).natAbs) : (P.affine q a hq hqa).badDiscriminant ∣ P.badDiscriminant

The transformed restricted discriminant divides the original one. Thus a finite divisor envelope of the Theorem 1 constants is uniform in q and a.