Removing the full discriminant-supported part

For divisors of distinct polynomial values, all common prime divisors belong to the radical discriminant. Removing their full prime powers produces a dagger tuple and a cross-coprime factorization. A single division by the gcd with the discriminant does not in general have these properties.

theorem NairTenenbaum.primeSelect_coordinate_dvd {r : ℕ} (n : Tuple r) (s : Finset ℕ) (i : Fin r) : ↑(primeSelect n s i) ∣ ↑(n i)

theorem NairTenenbaum.primeReject_coordinate_dvd {r : ℕ} (n : Tuple r) (s : Finset ℕ) (i : Fin r) : ↑(primeReject n s i) ∣ ↑(n i)

theorem NairTenenbaum.primeReject_coprime {r : ℕ} (n : Tuple r) {D : ℕ} (hD : D ≠ 0) (i : Fin r) : (↑(primeReject n D.primeFactors i)).Coprime D

Every coordinate remaining after full prime-power removal is coprime to D, even when the original valuation exceeds the valuation of D.

theorem NairTenenbaum.primeReject_dagger {r : ℕ} (n : Tuple r) {D : ℕ} (hD : D ≠ 0) (hcommon : ∀ (i j : Fin r), i ≠ j → (↑(n i)).gcd ↑(n j) ∣ D) : Dagger D (primeReject n D.primeFactors)

Common-divisor control suffices to make the remaining tuple dagger.

theorem NairTenenbaum.rootCount_pos_of_dvd_eval (Q : Polynomial ℤ) {q : ℕ} (hq : q ≠ 0) (a : ℤ) (ha : ↑q ∣ Polynomial.eval a Q) : 0 < rootCount Q q

An actual integral zero modulo a positive modulus witnesses a nonzero root count.

theorem NairTenenbaum.PolynomialSystem.divisor_primeReject_dagger {k r : ℕ} (P : PolynomialSystem k r) (a : ℤ) (m : Tuple r) (hm : ∀ (i : Fin r), ↑(m i) ∣ (Polynomial.eval a (P.R i)).natAbs) : Dagger P.discriminant (primeReject m P.discriminant.primeFactors)

Removing all discriminant primes from divisors of the irreducible values produces exactly the coprimality restrictions required by (16).

theorem NairTenenbaum.PolynomialSystem.divisor_primeSelect_bad_support {k r : ℕ} (P : PolynomialSystem k r) (a : ℤ) (m : Tuple r) (hm : ∀ (i : Fin r), ↑(m i) ∣ (Polynomial.eval a (P.R i)).natAbs) (i : Fin r) : ↑(primeSelect m P.discriminant.primeFactors i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors

For tuples dividing polynomial values, the removed part is supported only on the restricted bad discriminant, rather than all discriminant primes.

theorem NairTenenbaum.gcd_removal_not_coprime : ¬(8 / Nat.gcd 8 4).Coprime 4 ∧ ¬(8 / Nat.gcd 8 4).Coprime (Nat.gcd 8 4)

Dividing by one gcd can leave a discriminant prime in both factors. Thus that division cannot replace the full prime-power removal above.