The full-level, paid-floor IV.3 k₁ carrier

After reconstruction, both original factor supports and all beta masks are constant along the section. Canonical extraction and compatibility leave explicit coprimalities in k₁; the floor frequency bound is an interval. This is an exact carrier identity, not a bound for an arbitrary masked sum.

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedSupport (N : Finset ℕ) (a : ℤ) (x η R S : ℝ) (K : WExtractedKey) (r n₁ n₂ s : ℕ) : Prop

Original support, compatibility and five-small/low-omega conditions which do not vary with k₁. The finite beta carrier may be arbitrary.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionFixedSupport N a x η R S K r n₁ n₂ s = (K.2 * r ≤ ⌊R⌋₊ ∧ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime K * s ≤ ⌊S⌋₊ ∧ K.1.1 * K.1.2.1 * n₁ ∈ N ∧ K.1.1 * n₂ ∈ N ∧ a.natAbs.Coprime (K.1.2.2.1 * K.1.2.2.2.1) ∧ a.natAbs.Coprime (K.1.2.2.1 * K.1.2.2.2.2 * (r * s)) ∧ (K.1.1 * K.1.2.1 * n₁).Coprime (K.1.2.2.1 * K.1.2.2.2.1) ∧ (K.1.1 * n₂).Coprime (K.1.2.2.1 * K.1.2.2.2.2 * (r * s)) ∧ K.1.1 * K.1.2.1 * n₁ ≡ K.1.1 * n₂ [MOD K.1.2.2.1] ∧ ↑K.1.1 ≤ x ^ η ∧ ↑K.1.2.1 ≤ x ^ η ∧ ↑K.1.2.2.1 ≤ x ^ η ∧ ↑K.1.2.2.2.1 ≤ x ^ η ∧ ↑K.1.2.2.2.2 ≤ x ^ η ∧ ↑(K.1.1 * K.1.2.1 * n₁).primeFactors.card ≤ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x ∧ ↑(K.1.1 * n₂).primeFactors.card ≤ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x ∧ ↑(MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionDeltaPrime K * s).primeFactors.card ≤ MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.highOmegaCutoff x ∧ s.Coprime K.2)

def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCoprime (K : WExtractedKey) (a : ℤ) (r n₁ s k : ℕ) : Prop

The complete varying arithmetic mask, not an unspecified predicate.

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionCoprime K a r n₁ s k = (k.Coprime K.1.2.2.1 ∧ k.Coprime (K.1.2.2.2.2 * (r * s)) ∧ a.natAbs.Coprime k ∧ (K.1.1 * K.1.2.1 * n₁).Coprime k)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_factor_iff {N : Finset ℕ} {a : ℤ} {x η R S : ℝ} (hR : 0 ≤ R) (hS : 0 ≤ S) {K : WExtractedKey} {r n₁ n₂ s k : ℕ} (h : ℤ) (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))) (hΔ : 0 < K.2) (hΔ' : 0 < wKSectionDeltaPrime K) (he : K.2 * wKSectionDeltaPrime K = K.1.2.2.1 * K.1.2.2.2.2) : (wKSectionTuple K r n₁ n₂ s h k).1 ∈ wFactorExtractionTuples N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) ↔ wKSectionFixedSupport N a x η R S K r n₁ n₂ s ∧ k ≤ ⌊R * S⌋₊ / (K.1.2.2.1 * K.1.2.2.2.1) ∧ a.natAbs.Coprime k ∧ (K.1.1 * K.1.2.1 * n₁).Coprime k

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionLower (M Z : ℝ) (K : WExtractedKey) (r s : ℕ) (h : ℤ) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionLower M Z K r s h = max 1 ⌈↑h.natAbs * M * ↑K.1.2.2.1 / (↑(K.1.2.2.1 * K.1.2.2.2.2 * (r * s)) * ↑(K.1.2.2.1 * K.1.2.2.2.1) * Z)⌉₊

noncomputable def MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionUpper (R S : ℝ) (K : WExtractedKey) : ℕ

Equations

• MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionUpper R S K = ⌊R * S⌋₊ / (K.1.2.2.1 * K.1.2.2.2.1)

theorem MathlibNt.AnalyticNumberTheory.LargeSieve.LiLiuPrereqFouvry.wKSectionTuple_mem_key_iff {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₂ s k : ℕ} {h : ℤ} {b : ℕ} (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) : wKSectionTuple K r n₁ n₂ s h k ∈ wExtractedKeyFiber (wFloorCutoff M Z) N (Finset.Ioc 0 ⌊R * S⌋₊) a (c2FiveSmallMask x η) R S (highOmegaCutoff x) b K ↔ wKSectionFixedSupport N a x η R S K r n₁ n₂ s ∧ 2 ^ b ≤ h.natAbs ∧ h.natAbs < 2 ^ (b + 1) ∧ k ∈ Finset.Icc (wKSectionLower M Z K r s h) (wKSectionUpper R S K) ∧ wKSectionCoprime K a r n₁ s k

Exact membership of a reconstructed original tuple. The extraction equation, both supports, the gcd key, the signed shell and the paid floor cutoff are all accounted for. No varying coefficient is discarded.