Excluding the degenerate beta diagonal on the retained IV.3 carrier

Primitivity forces d₁*n = n₂ to have n₂ = 1. The original second beta coordinate would then be d ≤ x^η, contradicting its lower support. The nonzero differences below are derived from the actual support and mask, not imposed on the final original carrier.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_difference_ne_zero_of_support {d d₁ n n₂ : ℕ} {T Y : ℝ} (hc : (d₁ * n).Coprime n₂) (hd : ↑d ≤ Y) (hN₂ : T ≤ ↑(d * n₂)) (hYT : Y < T) : ↑d₁ * ↑n - ↑n₂ ≠ 0

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wFactorExtractionTuples_resonance_difference_ne_zero {N Q : Finset ℕ} (hN : ∀ m ∈ N, 0 < m) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S ξ T : ℝ} (hNT : ∀ m ∈ N, T ≤ ↑m) (hT : x ^ η < T) {z : WExtractedTuple} (hz : z ∈ wFactorExtractionTuples N Q a (c2FiveSmallMask x η) R S ξ) : have v := wGCDTuple (wExtractedOriginal z); ↑v.d₁ * ↑v.n₁ - ↑v.n₂ ≠ 0

Applies already to the original extracted carrier, before any section or Gram reindexing. Only the first component of the five-small mask is needed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedSupport_resonance_difference_ne_zero {N : Finset ℕ} {a : ℤ} {x η R S T : ℝ} (hNT : ∀ m ∈ N, T ≤ ↑m) (hT : x ^ η < T) {K : WExtractedKey} {r n n₂ s : ℕ} (hf : wKSectionFixedCanonical K r n n₂ s) (hsup : wKSectionFixedSupport N a x η R S K r n n₂ s) : ↑K.1.2.1 * ↑n - ↑n₂ ≠ 0

The same exclusion in the reconstructed fixed support interface.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_resonance_difference_ne_zero {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ m ∈ N, 0 < m) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S ξ T : ℝ} {b : ℕ} {K : WExtractedKey} (hNT : ∀ m ∈ N, T ≤ ↑m) (hT : x ^ η < T) {t : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S ξ b K) : have v := wGCDTuple (wExtractedOriginal t.1); ↑K.1.2.1 * ↑v.n₁ - ↑v.n₂ ≠ 0

Membership in an occupied key fiber supplies its own nonzero difference, with the fixed key's d₁.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wExtractedKeyFiber_resonance_differences_ne_zero {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ m ∈ N, 0 < m) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S ξ T : ℝ} {b : ℕ} {K : WExtractedKey} (hNT : ∀ m ∈ N, T ≤ ↑m) (hT : x ^ η < T) {t u : WExtractedTuple × ℤ} (ht : t ∈ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S ξ b K) (hu : u ∈ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S ξ b K) (hn : (wGCDTuple (wExtractedOriginal t.1)).n₁ = (wGCDTuple (wExtractedOriginal u.1)).n₁) : have v := wGCDTuple (wExtractedOriginal t.1); have v' := wGCDTuple (wExtractedOriginal u.1); ↑K.1.2.1 * ↑v.n₁ - ↑v.n₂ ≠ 0 ∧ ↑K.1.2.1 * ↑v.n₁ - ↑v'.n₂ ≠ 0

Both exclusions for a pair with the same first beta index follow from original membership. This does not assert any small-root cancellation.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_support_gap {x η ε T : ℝ} (hx : 1 < x) (hη : η < ε) (hT : x ^ ε ≤ T) : x ^ η < T

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.iv3_resonance_sum_le_const_mul_of_fixedSupport {N : Finset ℕ} {a h : ℤ} {x η R S T : ℝ} (ha : a ≠ 0) (hh : h ≠ 0) (hNT : ∀ m ∈ N, T ≤ ↑m) (hT : x ^ η < T) {K : WExtractedKey} {r n n₂' s' : ℕ} (hf' : wKSectionFixedCanonical K r n n₂' s') (hsup' : wKSectionFixedSupport N a x η R S K r n n₂' s') (F : Finset (ℕ × ℕ × ℤ)) (hF : ∀ t ∈ F, wKSectionFixedCanonical K r n t.1 t.2.1 ∧ wKSectionFixedSupport N a x η R S K r n t.1 t.2.1 ∧ iv3CorrelationNumerator K.1.2.1 n t.1 n₂' t.2.1 s' a h t.2.2 = 0) (w : ℕ × ℕ × ℤ → ℝ) {B : ℝ} (hB : 0 ≤ B) (hw : ∀ t ∈ F, w t ≤ B) : ∑ t ∈ F, w t ≤ B * ∑ n₂ ∈ (h * ↑n₂' * ↑s').natAbs.divisors, ↑((fouvryTau 2) (h * ↑n₂' * ↑s' * (↑K.1.2.1 * ↑n - ↑n₂)).natAbs)

A finite weighted count using only canonicality, retained fixed support, and zero resonance. In particular neither difference is a free hypothesis. These support predicates are the ones reconstructed from actual membership.