Exceptional mass and finite remainder transport for the actual external family

All coefficients below are the original full-integer externalTerm weights. The upper edge uses a smaller prime carrier only in the existing family definition; exceptional moduli are still measured against the original primorial. The generic finite remainder budget does not assume injectivity of any underlying sequence.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalUpperTerm_exceptional_mass_le (P : Finset ℕ) {D η : ℝ} (z : ℝ) (t : List ℕ) (hD : 2 ≤ D) (hη : 0 < η) (hηsmall : η < 1 / 8) (ht : t ∈ externalTags true P D η z) (T : ℕ) : ∑ d ∈ Finset.Icc 1 T with ¬d ∣ P.prod id, |(externalTerm true P D η z t) d| * (↑d.totient)⁻¹ ≤ 4 / D ^ η ^ 2 * (1 + Real.log ↑T) ^ 2

Uniform exceptional mass for each actual upper external member, including z > sqrt D. No primality or cutoff assumption on P is needed for this bound.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalUpperTerm_exceptional_remainder_le (P : Finset ℕ) {D η : ℝ} (z : ℝ) (t : List ℕ) (hD : 2 ≤ D) (hη : 0 < η) (hηsmall : η < 1 / 8) (ht : t ∈ externalTags true P D η z) (T : ℕ) (r : ℕ → ℝ) (H : ℝ) (hH : 0 ≤ H) (hr : ∀ d ∈ Finset.Icc 1 T, |r d| ≤ H / ↑d.totient) : |∑ d ∈ Finset.Icc 1 T with ¬d ∣ P.prod id, (externalTerm true P D η z t) d * r d| ≤ H * (4 / D ^ η ^ 2 * (1 + Real.log ↑T) ^ 2)

A per-member finite budget for arbitrary real remainders. The majorant is required only on the finite interval actually used in the sum.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalUpperFamily_exceptional_remainder_budget (P : Finset ℕ) {D η : ℝ} (z : ℝ) (hD : 2 ≤ D) (hη : 0 < η) (hηsmall : η < 1 / 8) (T : ℕ) (r : ℕ → ℝ) (H : ℝ) (hH : 0 ≤ H) (hr : ∀ d ∈ Finset.Icc 1 T, |r d| ≤ H / ↑d.totient) : ∑ t ∈ externalTags true P D η z, |∑ d ∈ Finset.Icc 1 T with ¬d ∣ P.prod id, (externalTerm true P D η z t) d * r d| ≤ ↑(externalTags true P D η z).card * H * (4 / D ^ η ^ 2) * (1 + Real.log ↑T) ^ 2

The sum of absolute per-tag exceptional remainders, with the actual tag cardinality. This is a finite transport layer, not a G9 endpoint hypothesis.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalTerm_full_sum_split (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D η : ℝ} (z : ℝ) (hD : 2 ≤ D) (hη : 0 < η) (hηsmall : η < 1 / 8) (t : List ℕ) (ht : t ∈ externalTags upper P D η z) (r : ℕ → ℝ) : ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + η + η ^ 9)⌋₊, (externalTerm upper P D η z t) d * r d = ∑ d ∈ (P.prod id).divisors, (externalTerm upper P D η z t) d * r d + ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + η + η ^ 9)⌋₊ with ¬d ∣ P.prod id, (externalTerm upper P D η z t) d * r d

Exact primorial-to-full splitting for the same actual member and arbitrary remainders. Only the summation carrier changes, never the weight.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalFamily_full_sum_split (upper : Bool) (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D η : ℝ} (z : ℝ) (hD : 2 ≤ D) (hη : 0 < η) (hηsmall : η < 1 / 8) (r : ℕ → ℝ) : ∑ t ∈ externalTags upper P D η z, ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + η + η ^ 9)⌋₊, (externalTerm upper P D η z t) d * r d = ∑ t ∈ externalTags upper P D η z, ∑ d ∈ (P.prod id).divisors, (externalTerm upper P D η z t) d * r d + ∑ t ∈ externalTags upper P D η z, ∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + η + η ^ 9)⌋₊ with ¬d ∣ P.prod id, (externalTerm upper P D η z t) d * r d

The exact family identity is obtained by summing memberwise identities; it makes no well-factorability assertion about an aggregate.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.externalUpperFamily_full_transport_budget (P : Finset ℕ) (hP : ∀ p ∈ P, Nat.Prime p) {D η : ℝ} (z : ℝ) (hD : 2 ≤ D) (hη : 0 < η) (hηsmall : η < 1 / 8) (r : ℕ → ℝ) (H : ℝ) (hH : 0 ≤ H) (hr : ∀ d ∈ Finset.Icc 1 ⌊D ^ (1 + η + η ^ 9)⌋₊, |r d| ≤ H / ↑d.totient) : ∑ t ∈ externalTags true P D η z, |∑ d ∈ Finset.Icc 1 ⌊D ^ (1 + η + η ^ 9)⌋₊, (externalTerm true P D η z t) d * r d - ∑ d ∈ (P.prod id).divisors, (externalTerm true P D η z t) d * r d| ≤ ↑(externalTags true P D η z).card * H * (4 / D ^ η ^ 2) * (1 + Real.log ↑⌊D ^ (1 + η + η ^ 9)⌋₊) ^ 2

Quantitative primorial-to-full transport, retaining absolute values memberwise. The generic remainder majorant is local to Icc 1 (floor Q).