Freezing the actual small root and reducing the paired sieve

The residue modulus is the small key modulus D', not the reciprocal modulus. Its unit conditions are derived from original tuple membership. On a unit residue class, the only sieve cost not already supplied by reciprocal nonunit vanishing is the divisor cost of |a|.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSection_DPrime_pos {K : WExtractedKey} {r n₁ n₂ s : ℕ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) : 0 < K.D'

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_coprime_DPrime {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {r n₁ n₂ s k : ℕ} {h : ℤ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (ht : wKSectionTuple K r n₁ n₂ s h k ∈ wExtractedKeyFiber H N Q a P R S ξ b K) : k.Coprime K.D'

The original compatibility conditions force a unit residue modulo the small root modulus. This is not an additional input to the producer.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_smallRoot_congr {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {P : WOriginalTuple → Prop} {R S ξ : ℝ} {b : ℕ} {K : WExtractedKey} {r n₁ n₂ s k l : ℕ} {h : ℤ} (hf : wKSectionFixedCanonical K r n₁ n₂ s) (ht : wKSectionTuple K r n₁ n₂ s h k ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (hu : wKSectionTuple K r n₁ n₂ s h l ∈ wExtractedKeyFiber H N Q a P R S ξ b K) (hkl : k ≡ l [MOD K.D']) : wActualSmallRootFactor a (wKSectionTuple K r n₁ n₂ s h k) = wActualSmallRootFactor a (wKSectionTuple K r n₁ n₂ s h l)

Two real section members in the same D' residue have exactly the same small-root factor, for either sign of the frequency and residue.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCoprime_pair_iff_of_units (K : WExtractedKey) (a : ℤ) (r n₁ s s' k : ℕ) (hkD : k.Coprime K.D') (hkq : k.Coprime (n₁ * r * s * s')) : wKSectionCoprime K a r n₁ s k ∧ wKSectionCoprime K a r n₁ s' k ↔ k.Coprime a.natAbs

After the two inherent unit conditions, only |a| remains in the paired arithmetic sieve. No divisor cost of n₁*r*s*s' is introduced.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCoprime_pair_coprime_modulus {K : WExtractedKey} {a : ℤ} {r n₁ s s' k : ℕ} (hk : wKSectionCoprime K a r n₁ s k) (hk' : wKSectionCoprime K a r n₁ s' k) : k.Coprime (n₁ * r * s * s')

Conversely, the actual paired sieve itself supplies the phase unit condition, even before a residue class has been selected.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSection_sieved_phase_eq {K : WExtractedKey} {a : ℤ} {r n₁ s s' k : ℕ} [NeZero (n₁ * r * s * s')] (hkD : k.Coprime K.D') (d : ℤ) : (if wKSectionCoprime K a r n₁ s k ∧ wKSectionCoprime K a r n₁ s' k then reciprocalPhase (n₁ * r * s * s') d ↑k else 0) = if k.Coprime a.natAbs then reciprocalPhase (n₁ * r * s * s') d ↑k else 0

Exact sieve reduction with the nonunit-zero extension of the phase. Thus nonunit points can be added back before using the analytic theorem.

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionPair_phase_data {H : ℕ → ℕ → ℕ} {N Q : Finset ℕ} (hN : ∀ n ∈ N, 0 < n) (hQ : ∀ q ∈ Q, 0 < q) {a : ℤ} {x η R S : ℝ} {b : ℕ} {K : WExtractedKey} {U : Finset (WExtractedTuple × ℤ)} (hU : U ⊆ wExtractedKeyFiber H N Q a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K) {c : Finset (ℕ × ℕ)} {r n₁ n₂ n₂' s s' k : ℕ} {h h' : ℤ} [NeZero (n₁ * r * s * s')] (hf : wKSectionFixedCanonical K r n₁ n₂ s) (hf' : wKSectionFixedCanonical K r n₁ n₂' s') (ht : wKSectionTuple K r n₁ n₂ s h k ∈ wCoprimeFiber x N S U c) (hu : wKSectionTuple K r n₁ n₂' s' h' k ∈ wCoprimeFiber x N S U c) : (K.D' * n₂ * n₂').Coprime (n₁ * r * s * s') ∧ K.D'.Coprime (n₁ * r * s * s') ∧ k.Coprime K.D' ∧ wActualReciprocalCorrelation K a (wKSectionTuple K r n₁ n₂ s h k) (wKSectionTuple K r n₁ n₂' s' h' k) = reciprocalPhase (n₁ * r * s * s') (iv3CorrelationNumerator K.1.2.1 n₁ n₂ n₂' s s' a h h' * wPhaseInverse (K.D' * n₂ * n₂') (n₁ * r * s * s')) ↑k

The reciprocal twist and the small residue step are units on a real paired section. The displayed phase equality uses the zero-extended reciprocal function only at its legitimate unit points.