A level-supported upper sieve for the q¹ count

This file keeps the level restriction in the finite object that is estimated: we first majorize each corrected candidate fibre by a Selberg square, and only then expand it into reduced-residue progressions. Thus the distribution input below is a cutoff-supported signed aggregate, not the obsolete full positive sum q1ErrorTermSum.

The analytic shape is the one used in Liu 2022, th-mvt, lines 137--151, with the Bombieri--Vinogradov input in lines 81--86: a level-supported Selberg square is expanded before a signed reduced-residue mean-value estimate is applied. The producer contract at the end deliberately separates the sieve fundamental lemma from the ∀ A ∃ B(A) weighted Pan/BV theorem; the non-reduced correction and the floor-safe admissible level are proved unconditionally in this file.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1TrueLiAPError (κ : ℝ) (N m : ℕ) : ℝ

The q¹ progression discrepancy with a genuine logarithmic integral. The parameter κ records the additive normalization left implicit by Liu's notation.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1TrueLiAPError κ N m = ↑(MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount N m) - MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ (↑N - 2) / ↑m.totient

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1TrueLiAPError_eq_primesInAPBelow (κ : ℝ) (N m : ℕ) (hN : 2 ≤ N) : q1TrueLiAPError κ N m = ↑(AnalyticNumberTheory.Sieve.primesInAPBelow (N - 2) 1 m (N % m)) - LiuWeight.liuLogarithmicIntegral κ (↑N - 2) / ↑m.totient

The new discrepancy is literally the a = 1 prime-progression error with the genuine li main term.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelModulusCutoff (N B : ℕ) : ℕ

The natural distribution cutoff ⌊N^(1/2) / log(N)^B⌋. Keeping this as a natural number makes every later modulus restriction a finite predicate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelModulusCutoff N B = ⌊↑N ^ (1 / 2) / Real.log ↑N ^ B⌋₊

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1PanSelbergLevel (B N : ℕ) : ℕ

The selected fixed q¹ Selberg level. Taking the natural square root after dividing the Pan cutoff by the switching range makes the cutoff inequality floor-safe at the level of natural numbers.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1PanSelbergLevel B N = (MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelModulusCutoff N B / MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N).sqrt

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier (N L : ℕ) : Finset ℕ

Divisors of the corrected sifting product which survive the explicit Selberg level L.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L = {d ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors | d ≤ L}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_q1LevelCarrier {N L d : ℕ} : d ∈ q1LevelCarrier N L ↔ d ∣ correctedChenSiftingProduct N ∧ d ≤ L

Membership in the finite level carrier exposes both its sieve support and its numerical level.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelBoundingSieve (N : ℕ) : BoundingSieve

The reciprocal-totient bounding sieve on the corrected Chen sifting product. Unlike Liu's source sieve, its prime support is exactly the corrected product used by the q¹ candidate condition.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelBoundingSieve N = { support := ∅, prodPrimes := MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N, prodPrimes_squarefree := ⋯, weights := fun (x : ℕ) => 0, weights_nonneg := MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelBoundingSieve._proof_2, totalMass := 0, nu := MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient, nu_mult := MathlibNt.SieveTheory.LiuWeight.liuSelbergReciprocalTotient_isMultiplicative, nu_pos_of_prime := ⋯, nu_lt_one_of_prime := ⋯ }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier_lcm_le_square {N L d1 d2 : ℕ} (hd1 : d1 ∈ q1LevelCarrier N L) (hd2 : d2 ∈ q1LevelCarrier N L) : d1.lcm d2 ≤ L ^ 2

The lcm of two level divisors remains below the square level.

structure MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedSelbergWeight (N L : ℕ) : Type

A raw Selberg weight supported on q1LevelCarrier. The upper-sieve majorization itself is supplied below as an analytic input; this structure records precisely its finite support, normalization, and boundedness.

• lambda : ℕ → ℝ
• lambda_one : self.lambda 1 = 1
• support (d : ℕ) : self.lambda d ≠ 0 → d ∈ q1LevelCarrier N L
• abs_le_one (d : ℕ) : |self.lambda d| ≤ 1

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelOptimalSelbergWeight (N L : ℕ) (hL : 1 ≤ L) : Q1LevelSupportedSelbergWeight N L

The cutoff-parameterized optimal Selberg weight on the corrected Chen sifting product.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelOptimalSelbergWeight N L hL = { lambda := MathlibNt.SieveTheory.LiuWeight.truncatedSelbergOptimalLambda (MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelBoundingSieve N) L, lambda_one := ⋯, support := ⋯, abs_le_one := ⋯ }

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergDenominator (N L : ℕ) : ℝ

The exact denominator attached to the corrected q¹ level.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergDenominator N L = MathlibNt.SieveTheory.LiuWeight.truncatedSelbergDenominator (MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelBoundingSieve N) L

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergDenominator_eq_sum_Icc {N L : ℕ} (hNeven : Even N) (hLz : L < correctedChenZ N) : q1LevelSelbergDenominator N L = ∑ d ∈ Finset.Icc 1 L, LiuWeight.liuSelbergArithmetic N d

Once the cutoff lies below the corrected prime threshold, the q¹ denominator is exactly the established squarefree-coprime arithmetic sum. This is the bridge to the uniform convolution and Euler-error estimates.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_q1LevelSelbergDenominator_sub_log_main_le {N L : ℕ} (hNeven : Even N) (hN : 0 < N) (hL : 2 ≤ L) (hLz : L < correctedChenZ N) : |q1LevelSelbergDenominator N L - Real.log ↑L / (2 * SingularSeries.liuSingularSeries N)| ≤ 2 * LiuWeight.liuSelbergAbsoluteLogMoment N + LiuWeight.liuSelbergAbsoluteMass N

Uniform denominator reduction at the corrected q¹ level. The main term retains the genuine Liu singular series; conversion to the finite truncated normalization is intentionally deferred.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelDivisorSum (N L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) (n : ℕ) : ℝ

The finite divisor sum whose square is the upper-sieve majorant.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelDivisorSum N L W n = ∑ d ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, if d ∣ n then W.lambda d else 0

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1PreSieveFibre (N q : ℕ) : Finset ℕ

The pre-sieving fibre for one switching modulus. It contains all base primes, before the corrected small-prime sieve is imposed.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1PreSieveFibre N q = {p ∈ Finset.range N | Nat.Prime p ∧ 2 ≤ N - p ∧ q ∣ N - p}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSquareMajorant (N L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) (q : ℕ) : ℝ

The Selberg square over the complete pre-sieving q-fibre.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSquareMajorant N L W q = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1PreSieveFibre N q, MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelDivisorSum N L W (N - p) ^ 2

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSquareExpanded (N L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) (q : ℕ) : ℝ

The double-sum expansion of q1LevelSquareMajorant. The following theorem proves that this is the literal finite expansion, with no asymptotic or discarded terms.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSquareExpanded N L W q = ∑ d1 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, ∑ d2 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, W.lambda d1 * W.lambda d2 * ↑(MathlibNt.SieveTheory.SwitchingPrinciple.q1APBaseCount N (q.lcm (d1.lcm d2)))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount_le_levelSquareMajorant {N L q : ℕ} (W : Q1LevelSupportedSelbergWeight N L) (_hq : q ∈ q1SwitchingPrimes N) : q1CandidateAPCount N q ≤ q1LevelSquareMajorant N L W q

Each corrected candidate in a switching fibre contributes one to the level-supported Selberg square, while all other pre-sieving points contribute a nonnegative square.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSquareMajorant_eq_expanded (N L q : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : q1LevelSquareMajorant N L W q = q1LevelSquareExpanded N L W q

The finite level-supported square expansion.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes (N B L : ℕ) : Finset ℕ

Reduced switching moduli whose full Selberg square remains inside the explicit Pan/Bombieri--Vinogradov cutoff.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L = {q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1SwitchingPrimes N | ¬q ∣ N ∧ q * L ^ 2 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelModulusCutoff N B}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedSwitchingPrimes (N _B _L : ℕ) : Finset ℕ

The non-reduced switching moduli. They are separated rather than assigned a fictitious reduced-residue Pan error.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedSwitchingPrimes N _B _L = {q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1SwitchingPrimes N | q ∣ N}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffFailureSwitchingPrimes (N B L : ℕ) : Finset ℕ

Reduced switching moduli for which the selected level would exceed the distribution cutoff.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffFailureSwitchingPrimes N B L = {q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1SwitchingPrimes N | ¬q ∣ N ∧ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelModulusCutoff N B < q * L ^ 2}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_q1LevelGoodSwitchingPrimes {N B L q : ℕ} : q ∈ q1LevelGoodSwitchingPrimes N B L ↔ q ∈ q1SwitchingPrimes N ∧ ¬q ∣ N ∧ q * L ^ 2 ≤ q1LevelModulusCutoff N B

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_q1LevelNonreducedSwitchingPrimes {N B L q : ℕ} : q ∈ q1LevelNonreducedSwitchingPrimes N B L ↔ q ∈ q1SwitchingPrimes N ∧ q ∣ N

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_q1LevelCutoffFailureSwitchingPrimes {N B L q : ℕ} : q ∈ q1LevelCutoffFailureSwitchingPrimes N B L ↔ q ∈ q1SwitchingPrimes N ∧ ¬q ∣ N ∧ q1LevelModulusCutoff N B < q * L ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1PanSelbergLevel_modulus_le_cutoff (N B q : ℕ) (hq : q ∈ q1SwitchingPrimes N) : q * q1PanSelbergLevel B N ^ 2 ≤ q1LevelModulusCutoff N B

Every switching modulus is cutoff-safe at the canonical Selberg level. This exact natural-number inequality needs no asymptotic threshold.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_floor_rpow_one_thirteenth_le_q1PanSelbergLevel (B : ℕ) : ∀ᶠ (N : ℕ) in Filter.atTop, ⌊↑N ^ (1 / 13)⌋₊ ≤ q1PanSelbergLevel B N

The canonical level retains a genuine Selberg scale: for each fixed Pan exponent it eventually dominates ⌊N^(1/13)⌋. The exponent 1/13 is chosen strictly below the limiting 1/12 supplied by cutoff / Y.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffFailureSwitchingPrimes_panSelbergLevel_eq_empty (N B : ℕ) : q1LevelCutoffFailureSwitchingPrimes N B (q1PanSelbergLevel B N) = ∅

The cutoff-failure carrier is identically empty at the canonical level.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSwitchingPrimes_partition (N B L : ℕ) : q1LevelGoodSwitchingPrimes N B L ∪ q1LevelNonreducedSwitchingPrimes N B L ∪ q1LevelCutoffFailureSwitchingPrimes N B L = q1SwitchingPrimes N

The three switching carriers form an exact finite partition.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSwitchingCarriers_pairwise_disjoint (N B L : ℕ) : Disjoint (q1LevelGoodSwitchingPrimes N B L) (q1LevelNonreducedSwitchingPrimes N B L) ∧ Disjoint (q1LevelGoodSwitchingPrimes N B L) (q1LevelCutoffFailureSwitchingPrimes N B L) ∧ Disjoint (q1LevelNonreducedSwitchingPrimes N B L) (q1LevelCutoffFailureSwitchingPrimes N B L)

The three finite switching carriers are pairwise disjoint.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGood_modulus_le_cutoff {N B L q d1 d2 : ℕ} (hq : Nat.Prime q) (hgood : q ∈ q1LevelGoodSwitchingPrimes N B L) (hd1 : d1 ∈ q1LevelCarrier N L) (hd2 : d2 ∈ q1LevelCarrier N L) : q.lcm (d1.lcm d2) ≤ q1LevelModulusCutoff N B

Every progression modulus in the good square lies below the explicit cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGood_residue_coprime {N B L q d1 d2 : ℕ} (hq : Nat.Prime q) (hqz : correctedChenZ N ≤ q) (hgood : q ∈ q1LevelGoodSwitchingPrimes N B L) (hd1 : d1 ∈ q1LevelCarrier N L) (hd2 : d2 ∈ q1LevelCarrier N L) : (N % q.lcm (d1.lcm d2)).Coprime (q.lcm (d1.lcm d2))

Every good progression has the reduced residue N mod m required by the Pan distribution error.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGood_modulus_admissible {N B L q d1 d2 : ℕ} (hgood : q ∈ q1LevelGoodSwitchingPrimes N B L) (hd1 : d1 ∈ q1LevelCarrier N L) (hd2 : d2 ∈ q1LevelCarrier N L) : q.lcm (d1.lcm d2) ≤ q1LevelModulusCutoff N B ∧ (N % q.lcm (d1.lcm d2)).Coprime (q.lcm (d1.lcm d2))

Good switching moduli are exactly the moduli to which the reduced-residue cutoff-supported Pan aggregate applies.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelWeightedBV_modulus_admissible {N B L q m : ℕ} (hgood : q ∈ q1LevelGoodSwitchingPrimes N B L) (hm : m ∈ (correctedChenSiftingProduct N).divisors) (hmL : m ≤ L ^ 2) : q.lcm m ≤ q1LevelModulusCutoff N B ∧ (N % q.lcm m).Coprime (q.lcm m)

Every nonzero term in the divisor-weighted Pan majorant has a reduced residue and final modulus below the advertised cutoff.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSquareAggregate (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : ℝ

The good portion of the q¹ count is bounded by the corresponding level-supported squares.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSquareAggregate N B L W = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L, MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSquareMajorant N L W q

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSignedPanAggregate (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : ℝ

The signed reduced-residue Pan aggregate. Absolute value is intentionally outside the complete weighted aggregate in the analytic input below.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSignedPanAggregate κ N B L W = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L, ∑ d1 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, ∑ d2 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, W.lambda d1 * W.lambda d2 * MathlibNt.SieveTheory.SwitchingPrinciple.q1TrueLiAPError κ N (q.lcm (d1.lcm d2))

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelWeightedPanMajorant (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : ℝ

The source-shaped weighted Pan/BV majorant: absolute values are taken after the complete lambda-pair sum for each switching prime, and only then summed. In particular, the analytic input cannot use cancellation between distinct switching fibres.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelWeightedPanMajorant κ N B L W = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L, |∑ d1 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, ∑ d2 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, W.lambda d1 * W.lambda d2 * MathlibNt.SieveTheory.SwitchingPrinciple.q1TrueLiAPError κ N (q.lcm (d1.lcm d2))|

theorem MathlibNt.SieveTheory.SwitchingPrinciple.abs_q1LevelSignedPanAggregate_le_weightedPanMajorant (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : |q1LevelSignedPanAggregate κ N B L W| ≤ q1LevelWeightedPanMajorant κ N B L W

The source-shaped majorant controls the absolute value of the total signed Pan contribution without assuming cancellation between switching primes.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelReducedResiduePanMajorant (κ : ℝ) (N B L : ℕ) : ℝ

The cutoff-supported divisor-weighted Pan majorant. The factor 3 ^ ω(m) is exactly the lcm-fibre multiplicity for two divisors of the squarefree sifting product. This is the standard weighted form supplied by Pan's weighted mean-value theorem; unlike the old diagnostic sum, every final modulus is level-supported.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelReducedResiduePanMajorant κ N B L = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L, ∑ m ∈ (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenSiftingProduct N).divisors, 3 ^ m.primeFactors.card * if m ≤ L ^ 2 then |MathlibNt.SieveTheory.SwitchingPrinciple.q1TrueLiAPError κ N (q.lcm m)| else 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelWeightedPanMajorant_le_reducedResiduePanMajorant (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : q1LevelWeightedPanMajorant κ N B L W ≤ q1LevelReducedResiduePanMajorant κ N B L

Bounded level weights reduce the source-shaped lambda-pair error to the canonical 3 ^ ω(m) divisor-weighted Pan majorant.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelMainAggregate (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : ℝ

The genuine li(N-2)/φ(m) main term paired with the good level-supported square.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelMainAggregate κ N B L W = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L, ∑ d1 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, ∑ d2 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, W.lambda d1 * W.lambda d2 * (MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ (↑N - 2) / ↑(q.lcm (d1.lcm d2)).totient)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergQuadratic (N L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : ℝ

The level-truncated Selberg quadratic form occurring after the switching prime is split from the Euler totient.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergQuadratic N L W = ∑ d1 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, ∑ d2 ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCarrier N L, W.lambda d1 * W.lambda d2 / ↑(d1.lcm d2).totient

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergQuadratic_eq_mainSum (N L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : q1LevelSelbergQuadratic N L W = BoundingSieve.mainSum (BoundingSieve.lambdaSquared W.lambda)

The q¹ quadratic is exactly the abstract Selberg main sum, with no change of carrier or local normalization.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergQuadratic_optimal (N L : ℕ) (hL : 1 ≤ L) : q1LevelSelbergQuadratic N L (q1LevelOptimalSelbergWeight N L hL) = 1 / q1LevelSelbergDenominator N L

The corrected-product optimal weight attains the reciprocal of the exact truncated denominator.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSwitchingReciprocalSum (N B L : ℕ) : ℝ

The exact reciprocal switching-prime factor in the q¹ main term.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSwitchingReciprocalSum N B L = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSwitchingPrimes N B L, 1 / (↑q - 1)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelMainAggregate_eq_li_mul_reciprocalSum_mul_quadratic (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : q1LevelMainAggregate κ N B L W = LiuWeight.liuLogarithmicIntegral κ (↑N - 2) * q1LevelSwitchingReciprocalSum N B L * q1LevelSelbergQuadratic N L W

Exact main-factor algebra. No asymptotic replacement is made: the genuine li_kappa(N - 2), the finite switching-prime reciprocal sum, and the truncated Selberg quadratic remain separate factors.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelMainAggregate_optimal (κ : ℝ) (N B L : ℕ) (hL : 1 ≤ L) : q1LevelMainAggregate κ N B L (q1LevelOptimalSelbergWeight N L hL) = LiuWeight.liuLogarithmicIntegral κ (↑N - 2) * q1LevelSwitchingReciprocalSum N B L / q1LevelSelbergDenominator N L

For the explicit corrected-product optimizer, the q¹ main aggregate is the exact switching-prime factor divided by the truncated Selberg denominator.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelGoodSquare_eq_main_add_signedPan (κ : ℝ) (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) (_hN : 2 ≤ N) : q1LevelGoodSquareAggregate N B L W = q1LevelMainAggregate κ N B L W + q1LevelSignedPanAggregate κ N B L W

The good square is exactly its li(N-2)/φ(m) aggregate plus the signed Pan aggregate.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedResidual (N B L : ℕ) : ℝ

The non-reduced residual is a sum of the actual candidate AP counts, not a truncation obtained by deleting terms from q1ErrorTermSum.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedResidual N B L = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedSwitchingPrimes N B L, MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount N q

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount_le_one_of_prime_dvd {N q : ℕ} (hqprime : Nat.Prime q) (hqN : q ∣ N) : q1CandidateAPCount N q ≤ 1

A non-reduced switching fibre contains at most the single prime p = q: from q ∣ N and q ∣ N - p one gets q ∣ p, and both are prime.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedResidual_le_card (N B L : ℕ) : q1LevelNonreducedResidual N B L ≤ ↑(q1LevelNonreducedSwitchingPrimes N B L).card

The complete non-reduced residual is bounded by the number of non-reduced switching primes. This records the exact elementary correction before any asymptotic estimate of that cardinality.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedResidual_le_two_mul_rpow_one_third (N B L : ℕ) (hN : 1 ≤ N) : q1LevelNonreducedResidual N B L ≤ 2 * ↑N ^ (1 / 3)

The non-reduced residual is already power-saving: it has at most as many terms as the switching range, and Y ≤ 2 N^(1/3).

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffResidual (N B L : ℕ) : ℝ

The cutoff-failure residual is likewise an actual q¹ candidate count.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffResidual N B L = ∑ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffFailureSwitchingPrimes N B L, MathlibNt.SieveTheory.SwitchingPrinciple.q1CandidateAPCount N q

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenQ1Count_le_levelSquare_add_residuals (N B L : ℕ) (W : Q1LevelSupportedSelbergWeight N L) : correctedChenQ1Count N ≤ q1LevelGoodSquareAggregate N B L W + q1LevelNonreducedResidual N B L + q1LevelCutoffResidual N B L

The corrected q¹ count is bounded by the good Selberg square plus the two honest residual count sums.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1FinalSelbergMainCoefficientBudget : ℝ

The exact final-margin budget for the q¹ Selberg main coefficient after the printed 3.94033 / 2 contribution and the two half-unit residual allowances are reserved.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1FinalSelbergMainCoefficientBudget = 20 / 3 - 3.94033 / 2 - 1

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1FinalSelbergMainCoefficientBudget_pos : 0 < q1FinalSelbergMainCoefficientBudget

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1TargetSelbergMainCoefficient : ℝ

A concrete sharp coefficient strictly inside the final numerical budget.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1TargetSelbergMainCoefficient = 3.69

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1TargetSelbergMainCoefficient_pos : 0 < q1TargetSelbergMainCoefficient

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1TargetSelbergMainCoefficient_lt_budget : q1TargetSelbergMainCoefficient < q1FinalSelbergMainCoefficientBudget

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1PanFixedLevelAsymptoticCoefficient : ℝ

The coefficient forced by the fixed Pan level after normalizing by the truncated singular series. Indeed, log (q1PanSelbergLevel B N) / log N tends to 1 / 12, while the switching-prime reciprocal sum tends to log (10 / 3); the exact optimal denominator therefore contributes their ratio.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1PanFixedLevelAsymptoticCoefficient = 12 * Real.log (10 / 3)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1FinalSelbergMainCoefficientBudget_lt_panFixedLevel : q1FinalSelbergMainCoefficientBudget < q1PanFixedLevelAsymptoticCoefficient

The coefficient forced by the fixed Pan level is already larger than the entire final main-term budget. Consequently the 3.69 target cannot be proved for q1PanSelbergLevel; a different level or switching architecture is required.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1TargetSelbergMainCoefficient_lt_panFixedLevel : q1TargetSelbergMainCoefficient < q1PanFixedLevelAsymptoticCoefficient

In particular, the explicit sharp target is smaller than the coefficient forced by the fixed Pan level.

def MathlibNt.SieveTheory.SwitchingPrinciple.Q1SharpLevelSelbergMainBound (κ : ℝ) (B : ℕ) (level : ℕ → ℕ) (cMain : ℝ) : Prop

The sole scalar estimate still required after the explicit optimal weight construction. It keeps li_kappa, the exact finite reciprocal prime sum, the corrected denominator, and the truncated singular-series normalization in their native forms.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1SharpLevelSelbergMainBound κ B level cMain = ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (_ : 1 ≤ level N), MathlibNt.SieveTheory.LiuWeight.liuLogarithmicIntegral κ (↑N - 2) * MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSwitchingReciprocalSum N B (level N) / MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSelbergDenominator N (level N) ≤ cMain * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

def MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedUpperSieveInput (κ : ℝ) (B : ℕ) (level : ℕ → ℕ) : Prop

The finite upper-sieve input: after selecting a level-supported Selberg weight, its main aggregate has the expected q¹-scale upper bound. The theorem above shows that only the named scalar estimate remains; weight existence and finite minimization are unconditional.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedUpperSieveInput κ B level = ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (W : MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedSelbergWeight N (level N)), MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelMainAggregate κ N B (level N) W ≤ C * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Q1SharpLevelSelbergMainBound.to_upperSieveInput {κ cMain : ℝ} {B : ℕ} {level : ℕ → ℕ} (hcMain : 0 < cMain) (hMain : Q1SharpLevelSelbergMainBound κ B level cMain) : Q1LevelSupportedUpperSieveInput κ B level

The scalar sharp bound supplies the original upper-sieve producer with the canonical corrected-product optimizer and the same named coefficient.

def MathlibNt.SieveTheory.SwitchingPrinciple.Q1ReducedResidueWeightedPanInput (κ : ℝ) : Prop

The sole published distributional input in this reduction: the a = 1 specialization of Pan's 3 ^ ω mean-value theorem, with reduced residues and cutoff-supported final moduli. Its quantifiers have the published order ∀ A > 0, ∃ B = B(A) (Liu 2022, th-mvt, lines 137--151). The finite theorem above proves that this is exactly the weight needed for the Selberg lambda-pair expansion; no unrestricted positive error sum is truncated.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1ReducedResidueWeightedPanInput κ = ∀ (A : ℝ), 0 < A → ∃ (B : ℕ) (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ (L : ℕ), MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelReducedResiduePanMajorant κ N B L ≤ C * ↑N / Real.log ↑N ^ A

def MathlibNt.SieveTheory.SwitchingPrinciple.Q1NonreducedResidualInput (B : ℕ) (level : ℕ → ℕ) : Prop

The separate non-reduced correction required because a switching prime may divide N; it is deliberately not set to zero in the Pan aggregate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1NonreducedResidualInput B level = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelNonreducedResidual N B (level N) ≤ C * ↑N / Real.log ↑N ^ A

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1NonreducedResidualInput (B : ℕ) (level : ℕ → ℕ) : Q1NonreducedResidualInput B level

The non-reduced input is unconditional, uniformly in the chosen level: the elementary N^(1/3) bound is smaller than every N / log(N)^A scale.

def MathlibNt.SieveTheory.SwitchingPrinciple.Q1CutoffAdmissibleLevel (B : ℕ) (level : ℕ → ℕ) : Prop

A valid level selection keeps every reduced switching fibre inside the distribution range. Thus the cutoff-failure residual is eventually empty, rather than assumed small after discarding whole fibres.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1CutoffAdmissibleLevel B level = ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∀ q ∈ MathlibNt.SieveTheory.SwitchingPrinciple.q1SwitchingPrimes N, ¬q ∣ N → q * level N ^ 2 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelModulusCutoff N B

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1PanSelbergLevel_cutoffAdmissible (B : ℕ) : Q1CutoffAdmissibleLevel B (q1PanSelbergLevel B)

The selected fixed q¹ Selberg level is Pan-admissible for every exponent B.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelCutoffResidual_eq_zero_of_admissible {B : ℕ} {level : ℕ → ℕ} (hlevel : Q1CutoffAdmissibleLevel B level) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → q1LevelCutoffResidual N B (level N) = 0

An admissible level makes the actual cutoff-failure count vanish.

def MathlibNt.SieveTheory.SwitchingPrinciple.Q1WeightedAggregateTheorem : Prop

The level-supported weighted q¹ aggregate theorem contains exactly the two genuine analytic inputs. The explicit level is cutoff-admissible and its non-reduced residual is power-saving by the unconditional theorems above.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1WeightedAggregateTheorem = ∃ (κ : ℝ), (∀ (B : ℕ), MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedUpperSieveInput κ B (MathlibNt.SieveTheory.SwitchingPrinciple.q1PanSelbergLevel B)) ∧ MathlibNt.SieveTheory.SwitchingPrinciple.Q1ReducedResidueWeightedPanInput κ

@[reducible, inline]

abbrev MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedWeightedAggregateTheorem : Prop

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.Q1LevelSupportedWeightedAggregateTheorem = MathlibNt.SieveTheory.SwitchingPrinciple.Q1WeightedAggregateTheorem

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSupportedWeightedAggregate_of_inputs (κ : ℝ) (hSieve : ∀ (B : ℕ), Q1LevelSupportedUpperSieveInput κ B (q1PanSelbergLevel B)) (hPan : Q1ReducedResidueWeightedPanInput κ) : Q1WeightedAggregateTheorem

Package the two genuine analytic producer inputs.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.hq1_of_weightedAggregate (hAggregate : Q1WeightedAggregateTheorem) : ∃ (Cq : ℝ), 0 < Cq ∧ ∃ (Nq : ℕ), ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

The source-faithful producer contract implies exactly the q¹ count estimate used downstream. The proof uses the finite square expansion, the ∀ A ∃ B(A) reduced-residue majorant, the exact non-reduced count, and an eventually empty cutoff-failure carrier.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1LevelSupportedWeightedAggregate_consumer (h : Q1LevelSupportedWeightedAggregateTheorem) : ∃ (Cq : ℝ), 0 < Cq ∧ ∃ (Nq : ℕ), ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

The strongest honest downstream consumer.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.q1WeightedAggregateConstant (hAggregate : Q1WeightedAggregateTheorem) : ℝ

A designated q¹ constant extracted from the level-supported route.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.q1WeightedAggregateConstant hAggregate = Classical.choose ⋯

theorem MathlibNt.SieveTheory.SwitchingPrinciple.q1WeightedAggregateConstant_spec (hAggregate : Q1WeightedAggregateTheorem) : 0 < q1WeightedAggregateConstant hAggregate ∧ ∃ (Nq : ℕ), ∀ (N : ℕ), Nq ≤ N → Even N → correctedChenQ1Count N ≤ q1WeightedAggregateConstant hAggregate * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

Positivity and the eventual q¹ estimate for the designated constant.