theorem MathlibNt.SieveTheory.suzukiElementaryMass_le_pow_div_factorial (S : BoundingSieve) (n z : ℕ) : suzukiElementaryMass S n z ≤ (∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p) ^ n / ↑n.factorial

The elementary symmetric mass is bounded by the corresponding power sum, with the exact factorial denominator.

theorem MathlibNt.SieveTheory.suzukiSourceV_le_pow_div_factorial (S : BoundingSieve) (n D z : ℕ) : suzukiSourceV S n D z ≤ (∑ p ∈ SwitchingPrinciple.suzukiSupportedBelow S z, S.nu p) ^ n / ↑n.factorial

Lemma 14.1 factorial bound, combining source domination by the elementary symmetric mass with its ordered-tuple/factorial estimate.