Uniform local-scale payment for the resonance divisor count

The proven pointwise divisor estimate pays both finite divisor choices. The bounds are uniform in the common first beta index and signed product. A bounds |P|, and B bounds d₁*n + |P|; no dyadic parameters are confused with the original, unextracted beta coordinates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_divisor_sum_le_local_scales {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (d₁ n : ℕ) (P : ℤ) (A B : ℝ), 0 ≤ A → 0 ≤ B → ↑P.natAbs ≤ A → ↑(d₁ * n + P.natAbs) ≤ B → ∑ j ∈ P.natAbs.divisors, ↑((fouvryTau 2) (P * (↑d₁ * ↑n - ↑j)).natAbs) ≤ C * A ^ (2 * ε) * B ^ ε

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_card_le_local_scales {ε : ℝ} (hε : 0 < ε) : ∃ (C : ℝ), 0 < C ∧ ∀ (d₁ n n₂' s' : ℕ) (a h : ℤ) (A B : ℝ), a ≠ 0 → h * ↑n₂' * ↑s' ≠ 0 → ↑d₁ * ↑n - ↑n₂' ≠ 0 → 0 ≤ A → 0 ≤ B → ↑(h * ↑n₂' * ↑s').natAbs ≤ A → ↑(d₁ * n + (h * ↑n₂' * ↑s').natAbs) ≤ B → ∀ (F : Finset (ℕ × ℕ × ℤ)), (∀ t ∈ F, 0 < t.1 ∧ 0 < t.2.1 ∧ (d₁ * n).Coprime t.1 ∧ ↑d₁ * ↑n - ↑t.1 ≠ 0 ∧ iv3CorrelationNumerator d₁ n t.1 n₂' t.2.1 s' a h t.2.2 = 0) → ↑F.card ≤ C * A ^ (2 * ε) * B ^ ε

The local-scale estimate applies to the entire resonant carrier, including all signed frequencies and every non-diagonal label pair.