Returning individual cancellation to the original weighted Gram section

The inner weights are fixed along the reconstructed section. The equality below retains both original tuple indices and the common-k condition until the exact reindexing; it does not identify repeated beta coordinates.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionSlice_weighted_pair_eq {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 (ℕ × ℕ)) (β ζ : ℕ → ℝ) : 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 ↑(wCorrelationInnerWeight K β ζ t) * star ↑(wCorrelationInnerWeight K β ζ u) * (wExtractedArithmeticPhase a t.2 t.1 * star (wExtractedArithmeticPhase a u.2 u.1)) else 0) = ↑(ζ (wKSectionDeltaPrime K * s) * β (K.1.1 * n₂)) * star ↑(ζ (wKSectionDeltaPrime K * s') * β (K.1.1 * n₂')) * wKSectionPairSum N a x η R S M Z K r n₁ n₂ n₂' s s' h h' b j cap positive c

One weighted section of the original separated Gram sum is exactly the proved cancellation sum times its two fixed signed coefficients.