Both cutoff intervals in an actual IV.3 pair

The common-k diagonal is reindexed without identifying distinct original tuples. Its interval is the intersection of the two separately reconstructed carriers, hence includes both paid floor cutoffs. No cancellation is claimed.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCoprime_iff (K : WExtractedKey) (a : ℤ) (r n₁ s k : ℕ) : wKSectionCoprime K a r n₁ s k ↔ k.Coprime (K.1.2.2.1 * (K.1.2.2.2.2 * (r * s)) * a.natAbs * (K.1.1 * K.1.2.1 * n₁))

A single, completely explicit coprimality obstruction. In particular it is not an arbitrary additional mask on an interval.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCarrier_inter (N : Finset ℕ) (a : ℤ) (x η R S M Z : ℝ) (K : WExtractedKey) (r n₁ n₂ n₂' s s' : ℕ) (h h' : ℤ) (b : ℕ) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) : wKSectionCarrier N a x η R S M Z K r n₁ n₂ s h b j cap positive c ∩ wKSectionCarrier N a x η R S M Z K r n₁ n₂' s' h' b j cap positive c = {k ∈ Finset.Icc (max (wKSectionGridLower M Z K r s h j) (wKSectionGridLower M Z K r s' h' j)) (wKSectionGridUpper R S K j cap) | (wKSectionFixedSupport N a x η R S K r n₁ n₂ s ∧ 2 ^ b ≤ h.natAbs ∧ h.natAbs < 2 ^ (b + 1) ∧ wKSectionFixedGrid x N S r n₁ n₂ s h j cap positive c ∧ wKSectionCoprime K a r n₁ s k) ∧ wKSectionFixedSupport N a x η R S K r n₁ n₂' s' ∧ 2 ^ b ≤ h'.natAbs ∧ h'.natAbs < 2 ^ (b + 1) ∧ wKSectionFixedGrid x N S r n₁ n₂' s' h' j cap positive c ∧ wKSectionCoprime K a r n₁ s' k}

The paired domain has the maximum of the two lower endpoints. All fixed tests and both explicit arithmetic masks remain visible.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_innerWeight {K : WExtractedKey} {r n₁ n₂ s k : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hk : 0 < k) (hkδ : k.Coprime K.1.2.2.1) (hkr : k.Coprime (K.1.2.2.2.2 * (r * s))) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (h : ℤ) (β ζ : ℕ → ℝ) : wCorrelationInnerWeight K β ζ (wKSectionTuple K r n₁ n₂ s h k) = ζ (wKSectionDeltaPrime K * s) * β (K.1.1 * n₂)

The inner weight, including any beta-clean mask, is constant along the section. The arbitrary first-modulus coefficient is not included.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.sum_wKSectionSlice_pair {A : Type u_1} [AddCommMonoid A] {N : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) {a : ℤ} {x η R S M Z : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) (hM : 0 < M) (hZ : 0 < Z) {K : WExtractedKey} {r n₁ n₂ n₂' s s' : ℕ} {h h' : ℤ} {b : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hf' : wKSectionFixedCanonical K r n₁ n₂' s') (hΔ : 0 < K.2) (hΔ' : 0 < wKSectionDeltaPrime K) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) (j cap : Fin 5 → ℕ) (positive : Bool) (c : Finset (ℕ × ℕ)) (F : WExtractedTuple × ℤ → WExtractedTuple × ℤ → A) : have U := wCoprimeFiber x N S (wAnalyticPrefix (wAnalyticDyadicBlock (wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) j positive) cap) c; (∑ t ∈ wKSectionSlice U r n₁ n₂ s h, ∑ u ∈ wKSectionSlice U r n₁ n₂' s' h', if (wGCDTuple (wExtractedOriginal t.1)).k₁ = (wGCDTuple (wExtractedOriginal u.1)).k₁ then F t u else 0) = ∑ k ∈ wKSectionCarrier N a x η R S M Z K r n₁ n₂ s h b j cap positive c ∩ wKSectionCarrier N a x η R S M Z K r n₁ n₂' s' h' b j cap positive c, F (wKSectionTuple K r n₁ n₂ s h k) (wKSectionTuple K r n₁ n₂' s' h' k)

Exact common-k paired sum on the real cell and prefix. The weight F can be the full IV.3 Gram kernel, with the small-root product intact.