Uniqueness of divisor tuples at a fixed substituted mass

Outside the radical discriminant, a prime cannot divide the values of two distinct irreducible factors at the same integer. This makes the congruence sets for distinct tuples of the same weighted mass disjoint.

theorem NairTenenbaum.coordinate_dvd_of_weightedMass_dvd {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n m : Tuple r) (hcross : ∀ (i j : Fin r), i ≠ j → (↑(n i)).Coprime ↑(m j)) (hmass : weightedMass γ n ∣ weightedMass γ m) (i : Fin r) : ↑(n i) ∣ ↑(m i)

Cross-coprimality removes every other coordinate from a weighted product.

theorem NairTenenbaum.weightedMass_injective_of_cross_coprime {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (n m : Tuple r) (hcross : ∀ (i j : Fin r), i ≠ j → (↑(n i)).Coprime ↑(m j)) (hmass : weightedMass γ n = weightedMass γ m) : n = m

Equality of weighted masses determines cross-coprime tuples uniquely.

theorem NairTenenbaum.PolynomialSystem.divisor_tuple_cross_coprime {k r : ℕ} (P : PolynomialSystem k r) (t : ℤ) (n m : Tuple r) (hn : ∀ (i : Fin r), ↑↑(n i) ∣ Polynomial.eval t (P.R i)) (hm : ∀ (i : Fin r), ↑↑(m i) ∣ Polynomial.eval t (P.R i)) (hD : ∀ (i : Fin r), (↑(n i)).Coprime P.discriminant) (i j : Fin r) : i ≠ j → (↑(n i)).Coprime ↑(m j)

Actual value divisors avoiding the discriminant are coprime across unequal irreducible-factor coordinates.

theorem NairTenenbaum.PolynomialSystem.divisor_tuple_eq_of_weightedMass_eq {k r : ℕ} (P : PolynomialSystem k r) (t : ℤ) (n m : Tuple r) (hn : ∀ (i : Fin r), ↑↑(n i) ∣ Polynomial.eval t (P.R i)) (hm : ∀ (i : Fin r), ↑↑(m i) ∣ Polynomial.eval t (P.R i)) (hD : Dagger P.discriminant n) (hmass : weightedMass P.exponent n = weightedMass P.exponent m) : n = m

Distinct dagger tuples of the same weighted mass cannot hold at the same integer. This is the disjointness needed before summing their root densities.