Exact squarefree coefficients of the fixed divided-power box

The existing full-integer weight is not changed. On a squarefree integer with k prime factors in the box, the raw slot sum is exactly k! and its divided power is exactly one. This distinguishes a normalized aggregate from its factorial-copy expansion; it asserts no sieve-density estimate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.primeBox_pow_squarefree (B : Finset ℕ) (k : ℕ) {n : ℕ} (hn : Squarefree n) (hB : n.primeFactors ⊆ B) (hk : ArithmeticFunction.cardFactors n = k) : (primeBox B ^ k) n = k.factorial

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.boxWeight_squarefree_eq_one (B : Finset ℕ) (k : ℕ) {n : ℕ} (hn : Squarefree n) (hB : n.primeFactors ⊆ B) (hk : ArithmeticFunction.cardFactors n = k) : (boxWeight B k) n = 1

This is a theorem about the already fixed full-integer divided power, not a squarefree mask substituted into its definition.