Weighted counting bridges and prime-power penalties

Corrected good and bad candidates give an exact counting bridge. Explicit Mertens bounds, Jurkat--Richert integral coefficients, and proper-prime-power estimates reduce positivity to stated uniform analytic inputs.

All declarations retain the MathlibNt.SieveTheory.SwitchingPrinciple namespace.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidate_mem_corrected_of_two_le {N p : ℕ} (hp : p ∈ chenWCandidates N) (hcomp : 2 ≤ N - p) : p ∈ correctedChenCandidates N

The historical lower-sieve candidates transfer safely to the corrected candidate set once the unit boundary is removed. This is a finite inclusion: it carries no historical switching or Omega estimate.

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

Historical lower-sieve candidates away from the unit boundary.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.chenWNonUnitCandidates N = {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates N | 2 ≤ N - p}

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenWNonUnitCandidates_subset_correctedChenCandidates (N : ℕ) : chenWNonUnitCandidates N ⊆ correctedChenCandidates N

The non-unit historical lower-sieve fibre is contained in the corrected candidate set.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenWCandidates_card_le_correctedChenCandidates_card_add_one (N : ℕ) : (chenWCandidates N).card ≤ (correctedChenCandidates N).card + 1

The historical W-count differs from a corrected-candidate lower bound by at most its explicitly isolated unit fibre.

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

Corrected candidates that already give a prime-plus-at-most-two-almost- prime representation.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenGoodCandidates N = {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N | Nat.IsAtMostAlmostPrime 2 (N - p)}

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

The bad fibre of the corrected candidate set. The planned replacement Omega must supply a multiplicity-correct penalty for every member of this set.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBadCandidates N = {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N | ¬Nat.IsAtMostAlmostPrime 2 (N - p)}

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPenalty (N p : ℕ) : ℝ

The explicit penalty attached to a corrected candidate. It records both prime-factor multiplicities in the medium interval and canonical medium/large/large triple witnesses.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPenalty N p = MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum (N - p) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) + MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount (N - p) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N)

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

The replacement switching sum associated with the corrected candidates. Unlike the historical chenOmega, its factor multiplicity is explicit. No analytic upper bound or counting bridge is claimed for it yet.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenOmega N = (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N).sum (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPenalty N)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPositivity_of_mainTerm_beats_error (N : ℕ) (hV : (BoundingSieve.errSum fun (x : ℕ) => 1) + correctedChenOmega N / 2 < (correctedChenBoundingSieve N).totalMass * correctedChenSieveProduct N) : 0 < ↑(correctedChenCandidates N).card - correctedChenOmega N / 2

Final positivity reduction from the lower-bound identity: if the main term X·V(N) is strictly greater than errSum(1) + Ω/2, the corrected count is positive.

This is the complete lower-bound reduction for CorrectedChenAnalyticPositivity: the three analytic inputs (the Mertens lower bound for V(N), control of errSum, and the Ω upper bound) are ultimately used only to establish this explicit real inequality.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.chenWeight_eq_one_sub_correctedChenPenalty (N p : ℕ) : chenWeight (N - p) (correctedChenZ N) (correctedChenY N) = 1 - correctedChenPenalty N p / 2

The corrected penalty is exactly the amount subtracted by the existing Chen weight. This gives a concrete interpretation to the future / 2 in a switching bridge.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenBad_penalty_ge_two {N p : ℕ} (hp : p ∈ correctedChenBadCandidates N) (hzy : correctedChenZ N < correctedChenY N) (hcube : ↑N - ↑p < ↑(correctedChenY N) ^ 3) : 2 ≤ correctedChenPenalty N p

A bad corrected candidate has penalty at least two, provided the cutoff parameters cover its complementary number below the cube scale. This is the finite multiplicity fact that will justify / 2 in the replacement switching bridge.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_counting_bridge (N : ℕ) (hzy : correctedChenZ N < correctedChenY N) (hcube : ∀ p ∈ correctedChenCandidates N, ↑N - ↑p < ↑(correctedChenY N) ^ 3) : ↑(correctedChenCandidates N).card - correctedChenOmega N / 2 ≤ ↑(correctedChenGoodCandidates N).card

The corrected finite switching bridge, conditional only on the elementary cutoff facts needed by the weight lemma. Its / 2 is justified by the explicit bad-fibre penalty, not by the obsolete historical Omega count.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.mem_correctedChenGood_or_bad {N p : ℕ} (hp : p ∈ correctedChenCandidates N) : p ∈ correctedChenGoodCandidates N ∨ p ∈ correctedChenBadCandidates N

Every corrected candidate lies in exactly one of the good and bad fibres. This is the finite partition on which the replacement counting bridge will be built.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenGoodCandidates_subset_goodRepresentations (N : ℕ) : correctedChenGoodCandidates N ⊆ chenGoodRepresentations N

Corrected good candidates are genuine good representations in the public Chen statement.

def MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenCutoffValid (N : ℕ) : Prop

The two elementary scale facts required by the corrected finite switching bridge. Keeping them as a named predicate cleanly separates rounding/cutoff analysis from the purely finite multiplicity argument.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenCutoffValid N = (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N < MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N ∧ ↑N ≤ ↑(MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) ^ 3)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChen_cube_scale (N : ℕ) : ↑N ≤ ↑(correctedChenY N) ^ 3

Ceiling rounding alone supplies the cube-scale half of the corrected cutoff predicate, for every natural input.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChen_floorZ_lt_y {N : ℕ} (hN : 1 < ↑N) : ⌊↑N ^ (1 / 10)⌋₊ < correctedChenY N

Apart from the harmless max 2, the lower cutoff is strictly below the upper cutoff as soon as the base exceeds one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChen_cutoffValid_of_root_gt_two {N : ℕ} (hroot : 2 < ↑N ^ (1 / 3)) : CorrectedChenCutoffValid N

The corrected cutoff predicate follows from a single concrete lower-root condition. The remaining threshold task is therefore the elementary claim 2 < N^(1/3), rather than any switching-counting statement.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChen_cutoffValid_of_nine_le {N : ℕ} (hN : 9 ≤ N) : CorrectedChenCutoffValid N

The remaining lower-root condition is already valid from the concrete threshold N ≥ 9. Consequently the corrected finite counting bridge has no unproved cutoff side condition in the range relevant to Chen's theorem.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChen_candidate_complement_lt_cube {N p : ℕ} (hscale : ↑N ≤ ↑(correctedChenY N) ^ 3) (hp : p ∈ correctedChenCandidates N) : ↑N - ↑p < ↑(correctedChenY N) ^ 3

The global cube-scale part of CorrectedChenCutoffValid supplies the strict complementary bound for every corrected candidate, because its prime component is positive.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_counting_bridge_public {N : ℕ} (hcutoff : CorrectedChenCutoffValid N) : ↑(correctedChenCandidates N).card - correctedChenOmega N / 2 ≤ ↑(chenGoodRepresentations N).card

The corrected bridge in the public Chen representation space. It is a fully kernel-checked replacement for the refuted historical counting bridge, conditional only on the cutoff predicate whose eventual validity remains an explicit analytic/rounding task.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_counting_bridge_public_of_nine_le {N : ℕ} (hN : 9 ≤ N) : ↑(correctedChenCandidates N).card - correctedChenOmega N / 2 ≤ ↑(chenGoodRepresentations N).card

The corrected finite bridge in the public representation space, with its cutoffs discharged for every N ≥ 9.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_key_inequality_implies_chen_at {N : ℕ} (hN : 9 ≤ N) (hkey : 0 < ↑(correctedChenCandidates N).card - correctedChenOmega N / 2) : ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

A positive corrected sieve difference already yields a genuine Chen representation. All finite switching, rounding, and boundary-fibre work is internal to this theorem; the only future input is an analytic proof that its left-hand side is positive.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_key_inequality_implies_chen (hkey : ∀ (N : ℕ), Even N → 1000 ≤ N → 0 < ↑(correctedChenCandidates N).card - correctedChenOmega N / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

The corrected analytic target implies Chen's theorem at the conventional threshold. This replaces the historical ChenCountingBridge assumption by a single honest analytic positivity obligation for the new objects.

def MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenAnalyticPositivity : Prop

The sole active analytic obligation for the corrected Chen development. It deliberately speaks only about the new candidate and penalty objects; no constant or bound from the refuted historical switching model is imported.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenAnalyticPositivity = ∀ (N : ℕ), Even N → 1000 ≤ N → 0 < ↑(MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N).card - MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenOmega N / 2

Positivity from the uniform main-term lower bound

theorem MathlibNt.SieveTheory.SwitchingPrinciple.primeProduct_lower_explicit : ∃ (M₀ : ℕ), ∀ (m : ℕ), M₀ ≤ m → 2 ≤ m → 1 / 3 / Real.log ↑m ≤ MertensTheorem.primeProduct m

Mertens lower bound with explicit constant 1/3: ∃ M₀, ∀ m ≥ M₀, 2 ≤ m → (1/3)/log m ≤ primeProduct m`.

This follows from the precise Mertens estimate |pp - e^{-γ}/log m| ≤ C/log²m and e^{-γ} > 1/3, which follows from γ < 2/3 and e < 3.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_log_le_logN_div_ten {N : ℕ} (hN : 2 ≤ N) : Real.log ↑(correctedChenZ N - 1) ≤ 1 / 10 * Real.log ↑N

Sharp upper parameter estimate: log(z-1) ≤ (1/10)·log N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ_sub_one_ge_of_N_ge {k N : ℕ} (hk : 2 ≤ k) (hN : (k + 1) ^ 10 ≤ N) : k ≤ correctedChenZ N - 1

General parameter estimate: for N ≥ (k+1)^10, k ≤ z-1 (z = ⌈N^{1/10}⌉).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.tendsto_correctedChenZ_sub_one_atTop : Filter.Tendsto (fun (N : ℕ) => correctedChenZ N - 1) Filter.atTop Filter.atTop

theorem MathlibNt.SieveTheory.SwitchingPrinciple.tendsto_correctedChenSingularSeriesTailMajorant : Filter.Tendsto (fun (N : ℕ) => (1 + 1 / ↑(correctedChenZ N - 1)) ^ 10) Filter.atTop (nhds 1)

The explicit ten-factor majorant for the large-prime tail tends to one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_two_mul_liuSingularSeries_le_truncated (η : ℝ) (hη : 0 < η) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → 2 * SingularSeries.liuSingularSeries N ≤ (1 + η) * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1)

Uniform comparison at the varying corrected Chen cutoff. The genuine Liu series is bounded by half the sieve-normalized truncation, up to any prescribed multiplicative margin. No fixed-source convergence statement is used.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenMainTermLower_singularSeries_units : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → 10 / 3 * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2 ≤ (correctedChenBoundingSieve N).totalMass * correctedChenSieveProduct N

Uniform main-term lower bound in singular-series units: (10/3)·𝔖_trunc·N/log²N ≤ X·V(N).

Combine the exact identity X·V = X·𝔖·primeProduct(z-1), the Mertens lower bound primeProduct ≥ (1/3)/log(z-1), and the parameter upper bound log(z-1) ≤ (1/10)·log N.

def MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenOmegaUpperBound : Prop

Ω upper-bound target: uniformly, correctedChenOmega ≤ cΩ·𝔖_trunc·N/log²N, with (10/3) > cΩ/2, so the main-term coefficient strictly exceeds the Ω/2 coefficient.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenOmegaUpperBound = ∃ (cΩ : ℝ), 10 / 3 > cΩ / 2 ∧ ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenOmega N ≤ cΩ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

theorem MathlibNt.SieveTheory.SwitchingPrinciple.omega_upper_bound_compatible_with_39404 : 10 / 3 > 3.9404 / 2

Compatibility with the classical constant: the main-term coefficient 10/3 strictly exceeds half the classical Ω upper-bound coefficient, 3.9404/2. Thus the numerical condition in CorrectedChenOmegaUpperBound permits cΩ = 3.9404, the classical constant of Chen 1973.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenOmegaUpperBound_of_39404 (hbound : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → correctedChenOmega N ≤ 3.9404 * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) : CorrectedChenOmegaUpperBound

An Ω upper bound with the classical constant 3.9404, satisfying the main-term coefficient condition, can be used directly. This theorem makes the instantiation condition for CorrectedChenOmegaUpperBound explicit: it suffices to prove ∃ N₀, ∀ N ≥ N₀ Even, correctedChenOmega N ≤ 3.9404·𝔖_trunc·N/log²N.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.CorrectedChenPositivity_large_of_inputs (hPan : ChenWeightedPanInput) (hΩ : CorrectedChenOmegaUpperBound) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → 0 < ↑(correctedChenCandidates N).card - correctedChenOmega N / 2

Final assembly: the proved uniform main-term lower bound, an Ω upper-bound input, and weighted Pan control of errSum imply positivity of the corrected count for sufficiently large even numbers.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.corrected_chens_theorem_of_inputs (hPan : ChenWeightedPanInput) (hΩ : CorrectedChenOmegaUpperBound) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Chen's theorem conditional on two analytic inputs: pass from CorrectedChenPositivity_large_of_inputs through corrected_key_inequality_implies_chen_at to the final ∃ N₀ form.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum_eq_sum_factorization_of_dvd {n z y : ℕ} (hn : n ≠ 0) : primePowerSum n z y = ∑ q ∈ Finset.range y with Nat.Prime q ∧ z ≤ q ∧ q ∣ n, ↑(n.factorization q)

Prime-power part: primePowerSum n z y equals the sum of the multiplicities of primes in [z, y) dividing n; the filter condition ∃ k ≥ 1, exactDiv q k n is equivalent to q ∣ n.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.factorization_le_card_pow_dvd {n q : ℕ} (hq : Nat.Prime q) (hn : n ≠ 0) : n.factorization q ≤ {k ∈ Finset.range (n + 1) | q ^ (k + 1) ∣ n}.card

Multiplicity is at most the number of prime powers: n.factorization q ≤ #{k : q^(k+1) ∣ n}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum_le_powerCount (n z y : ℕ) : primePowerSum n z y ≤ ∑ q ∈ Finset.range y with Nat.Prime q ∧ z ≤ q, ∑ k ∈ Finset.range (n + 1), if q ^ (k + 1) ∣ n then 1 else 0

Uniform finite upper bound for the prime-power part: primePowerSum n z y ≤ Σ_{q ∈ [z,y)} Σ_k [q^(k+1) | n].

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

The prime-power part of the corrected Chen penalty.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPrimePowerPenalty N = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N, MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum (N - p) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N)

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

The strict ordered-triple part of the corrected Chen penalty.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenTriplePenalty N = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N, MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount (N - p) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral (u : ℝ) : ℝ

The inner Buchstab integral occurring in both terms of Chen's equations (26)--(27).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral u = ∫ (t : ℝ) in 2..u - 1, Real.log (t - 1) / t

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertJ : ℝ

Chen's exact integral J from equation (26): ∫₃⁴ du/u ∫₂ᵘ⁻¹ log(t-1)/t dt.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertJ = ∫ (u : ℝ) in 3..4, MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral u / u

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral_nonneg {u : ℝ} (hu3 : 3 ≤ u) : 0 ≤ jurkatRichertInnerIntegral u

The inner Buchstab integral is nonnegative on the range used by Chen.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertJ_nonneg : 0 ≤ jurkatRichertJ

Chen's base Buchstab integral is nonnegative.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertK : ℝ

Chen's exact integral K from equations (26)--(27), after the paper's change of variables u = 5 - 10α: ∫₃⁴ 10/[u(5-u)] du ∫₂ᵘ⁻¹ log(t-1)/t dt.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertK = ∫ (u : ℝ) in 3..4, 10 / (u * (5 - u)) * MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertInnerIntegral u

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertK_nonneg : 0 ≤ jurkatRichertK

Chen's varying-level Buchstab integral is nonnegative.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.Internal.continuousOn_jurkatRichertInnerIntegral : ContinuousOn jurkatRichertInnerIntegral (Set.Icc 3 4)

The exact inner Buchstab integral is continuous on the range needed for Chen's outer integral.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichert_integralEstimate : -164725e-7 ≤ jurkatRichertJ - jurkatRichertK / 4

Chen's numerical estimate for the exact integrals in equations (26)--(27). The small cubic saving in jurkatRichert_innerIntegral_le makes the displayed decimal bound valid despite the rounding in the printed elementary majorant.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseMainCoefficient (J : ℝ) : ℝ

The base lower-sieve coefficient in Chen's equation (26).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseMainCoefficient J = 8 * (Real.log 4 + J)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseSieveFactor (J : ℝ) : ℝ

The dimensionless source lower-sieve factor before equation (25)'s Mertens normalization is applied.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseSieveFactor J = 2 * Real.exp Real.eulerMascheroniConstant / 5 * (Real.log 4 + J)

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertMertensFactor : ℝ

The factor in Chen's equation (25): Γ_N(N^(1/10)) ~ 20 exp(-γ) C_N / log N.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertMertensFactor = 20 * Real.exp (-Real.eulerMascheroniConstant)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertBaseSieveFactor_pos : 0 < jurkatRichertBaseSieveFactor jurkatRichertJ

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertMertensFactor_pos : 0 < jurkatRichertMertensFactor

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichert_sieveFactor_mul_mertensFactor : jurkatRichertBaseSieveFactor jurkatRichertJ * jurkatRichertMertensFactor = jurkatRichertBaseMainCoefficient jurkatRichertJ

Equation (25)'s Mertens factor and equation (26)'s lower-sieve factor multiply to the exact base coefficient, with no opaque constant.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertQ1MainCoefficient (K : ℝ) : ℝ

The varying-level medium-prime upper-sieve coefficient in Chen's equations (26)--(27).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertQ1MainCoefficient K = 8 * (Real.log 8 + K / 2)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichert_mainCoefficient_decomposition (J K : ℝ) : jurkatRichertBaseMainCoefficient J - jurkatRichertQ1MainCoefficient K / 2 = 8 * (Real.log 4 - Real.log 8 / 2 + (J - K / 4))

The exact algebraic split behind Chen's 2.6408: the base lower-sieve coefficient minus half the distinct-q upper-sieve coefficient.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichert_mainCoefficient_ge_twoPoint6408 (J K : ℝ) (hJK : -164725e-7 ≤ J - K / 4) : 2.6408 ≤ jurkatRichertBaseMainCoefficient J - jurkatRichertQ1MainCoefficient K / 2

Chen's numerical integral input J - K/4 ≥ -0.0164725 yields the published coefficient 2.6408. The remaining decimal step is certified from Mathlib's explicit lower bound for log 2.

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

The valuation-weighted count used by the corrected finite Chen decomposition. It is not the direct literature object: repeated powers of one medium prime are charged with their full valuation.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertWeightedCount N = ↑(MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N).card - MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPrimePowerPenalty N / 2

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound : Prop

The canonical corrected endpoint. For every positive coefficient margin, the valuation-weighted count is eventually bounded below by (2.6408 - η) 𝔖(N) N / log² N along the even integers, in Liu's genuine singular-series normalization. It is produced from the source-faithful distinct-q theorem below, after a separate proper-prime-power correction.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound = ∀ (η : ℝ), 0 < η → ∀ᶠ (N : ℕ) in Filter.atTop, Even N → (2.6408 - η) * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 ≤ MathlibNt.SieveTheory.SwitchingPrinciple.jurkatRichertWeightedCount N

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenOmega_eq_primePower_add_triple (N : ℕ) : correctedChenOmega N = ∑ p ∈ correctedChenCandidates N, primePowerSum (N - p) (correctedChenZ N) (correctedChenY N) + ∑ p ∈ correctedChenCandidates N, tripleFactorCount (N - p) (correctedChenZ N) (correctedChenY N)

correctedChenOmega splits into its prime-power and triple parts.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenKeyCount_eq_jurkatRichertWeightedCount_sub_triple (N : ℕ) : ↑(correctedChenCandidates N).card - correctedChenOmega N / 2 = jurkatRichertWeightedCount N - correctedChenTriplePenalty N / 2

Exact finite bookkeeping: the Jurkat--Richert weighted count has already paid the prime-power part of the corrected penalty, leaving only half of the strict ordered-triple penalty.

def MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertTriplePenaltyUpperBound : Prop

Source-scale upper input for the genuine strict ordered-triple penalty. It is independent of the JR weighted lower conclusion and keeps the inverse-log remainder visible.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.ChenJurkatRichertTriplePenaltyUpperBound = ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, Even N → MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenTriplePenalty N ≤ 3.94033 * MathlibNt.SieveTheory.SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ 3

Uniform prime-power bound

theorem MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenPrimePowerProperCountBound (N : ℕ) (hNbig : 2 ^ 110 < N) (_hEven : Even N) : ↑(∑ p ∈ correctedChenCandidates N, {q ∈ Finset.range (correctedChenY N) | Nat.Prime q ∧ correctedChenZ N ≤ q ∧ q ^ 2 ∣ N - p}.card) ≤ 6 * ↑N ^ (9 / 10)

Uniform bound for proper prime powers: the number of pairs (p,q) with p a corrected candidate, q a prime in [z,y), and q² | N-p is uniformly bounded by 6·N^{9/10}.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.primePowerSum_le_factorCount_add_powerSum (n z y : ℕ) (hn : n ≠ 0) : primePowerSum n z y ≤ ↑{q ∈ Finset.range y | Nat.Prime q ∧ z ≤ q ∧ q ∣ n}.card + ∑ q ∈ Finset.range y with Nat.Prime q ∧ z ≤ q ∧ q ^ 2 ∣ n, ↑(n.factorization q)

Structural decomposition of the prime-power sum: primePowerSum(n) ≤ #{q ∈ [z,y) : q | n} + Σ_{q ∈ [z,y), q²|n} v_q(n). Thus the prime-power penalty is at most the k=1 prime-divisor count plus the proper-power part, whose N^{9/10} bound is supplied by correctedChenPrimePowerProperCountBound.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.errLogCube_negligible (Cerr : ℝ) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → Cerr * ↑N / Real.log ↑N ^ 3 ≤ 1 / 4 * ↑N / Real.log ↑N ^ 2

Negligibility threshold: for any Cerr, there exists N₀ such that Cerr·N/log³N ≤ (1/4)·N/log²N for even N ≥ N₀. It suffices to have log N ≥ 4·Cerr, so take N₀ = ⌈exp(4·Cerr)⌉ + 1.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.eventually_jr_inverseLogRemainder_le_scale (C ρ : ℝ) (hC : 0 < C) (hρ : 0 < ρ) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → C * ↑N / Real.log ↑N ^ 3 ≤ ρ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

Any inverse-log-cube remainder is eventually absorbed by an arbitrary positive fraction of the Liu singular-series N/log² N scale.

The q¹ distribution input

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

q¹ distribution input: the aggregate count of prime factors in [z,y) over candidates, Σ_{p ∈ candidates} #{q ∈ [z,y) : q | N−p}.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenQ1Count N = ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N, ↑{q ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) | Nat.Prime q ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N ≤ q ∧ q ∣ N - p}.card