Richert 1969, Theorem 1: finite weighted-sieve chain

Frozen source:

• references/richert-1969/richert-1969.pdf, PDF pages 8--11, equations (3.1)--(3.11);
• references/richert-1969/VISION_TRANSCRIPTION.md, sections 5 and 9.

The paper's Theorem A is quoted rather than proved. This file therefore proves only the finite implication that consumes a lower S(A,z), every conditioned upper S(A,p,z), and the squareful exclusion. It does not introduce an axiom, and it does not assume the weighted conclusion.

def MathlibNt.SieveTheory.Richert1969.lowerCarrier (A : Finset ℕ) (P : ℕ) : Finset ℕ

The finite carrier counted by the lower object S(A,z).

Equations

• MathlibNt.SieveTheory.Richert1969.lowerCarrier A P = {a ∈ A | P.Coprime a}

def MathlibNt.SieveTheory.Richert1969.squarefreeWeightedCarrier (A Q : Finset ℕ) (P : ℕ) : Finset ℕ

The primed carrier in (3.1): square divisibility by a weighted prime is excluded before the Richert weight is summed.

Equations

• MathlibNt.SieveTheory.Richert1969.squarefreeWeightedCarrier A Q P = {a ∈ MathlibNt.SieveTheory.Richert1969.lowerCarrier A P | ∀ p ∈ Q, ¬p ^ 2 ∣ a}

def MathlibNt.SieveTheory.Richert1969.squarefulCorrection (A Q : Finset ℕ) (P : ℕ) : ℝ

The exact finite squareful correction removed from the lower carrier.

Equations

• MathlibNt.SieveTheory.Richert1969.squarefulCorrection A Q P = ↑(MathlibNt.SieveTheory.Richert1969.lowerCarrier A P).card - ↑(MathlibNt.SieveTheory.Richert1969.squarefreeWeightedCarrier A Q P).card

def MathlibNt.SieveTheory.Richert1969.primeConditionedCarrier (A : Finset ℕ) (P p : ℕ) : Finset ℕ

The prime-conditioned upper object S(A,p,z).

Equations

• MathlibNt.SieveTheory.Richert1969.primeConditionedCarrier A P p = {a ∈ MathlibNt.SieveTheory.Richert1969.lowerCarrier A P | p ∣ a}

def MathlibNt.SieveTheory.Richert1969.weightedLowerObject (A Q : Finset ℕ) (P : ℕ) (lambda : ℝ) (w : ℕ → ℝ) : ℝ

The finite weighted lower object in (3.1), with the source prime interval encoded by Q and the source factor 1 - u log p / log X encoded by w.

Equations

• MathlibNt.SieveTheory.Richert1969.weightedLowerObject A Q P lambda w = ∑ a ∈ MathlibNt.SieveTheory.Richert1969.squarefreeWeightedCarrier A Q P, (1 - lambda * ∑ p ∈ Q, if p ∣ a then w p else 0)

def MathlibNt.SieveTheory.Richert1969.primeConditionedUpperAggregate (A Q : Finset ℕ) (P : ℕ) (w : ℕ → ℝ) : ℝ

The weighted sum of all prime-conditioned upper objects.

Equations

• MathlibNt.SieveTheory.Richert1969.primeConditionedUpperAggregate A Q P w = ∑ p ∈ Q, w p * ↑(MathlibNt.SieveTheory.Richert1969.primeConditionedCarrier A P p).card

noncomputable def MathlibNt.SieveTheory.Richert1969.theoremOneWeightedPrimes (X : ℝ) (K : ℕ) (u v : ℝ) : Finset ℕ

The exact prime interval in (3.1), including the restriction p ∤ K.

Equations

• MathlibNt.SieveTheory.Richert1969.theoremOneWeightedPrimes X K u v = {p ∈ Finset.range ⌈X ^ (1 / u)⌉₊ | Nat.Prime p ∧ X ^ (1 / v) ≤ ↑p ∧ ↑p < X ^ (1 / u) ∧ ¬p ∣ K}

noncomputable def MathlibNt.SieveTheory.Richert1969.theoremOneSiftingProduct (X : ℝ) (K : ℕ) (v : ℝ) : ℕ

The finite product P_K(X^(1/v)) defining the lower sifted carrier.

Equations

• MathlibNt.SieveTheory.Richert1969.theoremOneSiftingProduct X K v = {p ∈ Finset.range ⌈X ^ (1 / v)⌉₊ | Nat.Prime p ∧ ↑p < X ^ (1 / v) ∧ ¬p ∣ K}.prod id

noncomputable def MathlibNt.SieveTheory.Richert1969.theoremOnePrimeWeight (X u : ℝ) (p : ℕ) : ℝ

Richert's logarithmic prime weight 1 - u log p / log X in (3.1).

Equations

• MathlibNt.SieveTheory.Richert1969.theoremOnePrimeWeight X u p = 1 - u * Real.log ↑p / Real.log X

noncomputable def MathlibNt.SieveTheory.Richert1969.theoremOneWeightedLowerObject (A : Finset ℕ) (X : ℝ) (K : ℕ) (v u lambda : ℝ) : ℝ

The literal finite object W_K(A,v,u,lambda) from (3.1)--(3.2).

Equations

• MathlibNt.SieveTheory.Richert1969.theoremOneWeightedLowerObject A X K v u lambda = MathlibNt.SieveTheory.Richert1969.weightedLowerObject A (MathlibNt.SieveTheory.Richert1969.theoremOneWeightedPrimes X K u v) (MathlibNt.SieveTheory.Richert1969.theoremOneSiftingProduct X K v) lambda (MathlibNt.SieveTheory.Richert1969.theoremOnePrimeWeight X u)

theorem MathlibNt.SieveTheory.Richert1969.lower_sub_squareful_sub_conditioned_le_weightedLowerObject (A Q : Finset ℕ) (P : ℕ) (lambda : ℝ) (w : ℕ → ℝ) (hlambda : 0 ≤ lambda) (hw : ∀ p ∈ Q, 0 ≤ w p) : ↑(lowerCarrier A P).card - squarefulCorrection A Q P - lambda * primeConditionedUpperAggregate A Q P w ≤ weightedLowerObject A Q P lambda w

Equations (3.5)--(3.8), before any analytic estimate: the weighted lower object is bounded below by the lower sieve, minus the exact squareful correction, minus the weighted sum of the prime-conditioned upper sieves.

theorem MathlibNt.SieveTheory.Richert1969.theoremOneFiniteLowerBound (A : Finset ℕ) (X : ℝ) (K : ℕ) (v u lambda : ℝ) (hlambda : 0 ≤ lambda) (hweight : ∀ p ∈ theoremOneWeightedPrimes X K u v, 0 ≤ theoremOnePrimeWeight X u p) : ↑(lowerCarrier A (theoremOneSiftingProduct X K v)).card - squarefulCorrection A (theoremOneWeightedPrimes X K u v) (theoremOneSiftingProduct X K v) - lambda * primeConditionedUpperAggregate A (theoremOneWeightedPrimes X K u v) (theoremOneSiftingProduct X K v) (theoremOnePrimeWeight X u) ≤ theoremOneWeightedLowerObject A X K v u lambda

Equation (3.5) for the literal interval and logarithmic weight of Theorem 1. The later analytic estimates (3.6)--(3.11) are separate inputs.

theorem MathlibNt.SieveTheory.Richert1969.Chen.lowerS_eq_candidateCard (N : ℕ) : BoundingSieve.siftedSum = ↑(SwitchingPrinciple.jurkatRichertSourceCandidates N).card

The lower S(A,z) in the Chen specialization is exactly the source Goldbach candidate count.

theorem MathlibNt.SieveTheory.Richert1969.Chen.primeConditionedUpperS_eq_candidateCard (N p : ℕ) : BoundingSieve.siftedSum = ↑{q ∈ SwitchingPrinciple.jurkatRichertSourceCandidates N | p ∣ N - q}.card

Every S(A,p,z) in the Chen specialization is the literal conditioned candidate count, including the nonreduced p ∣ N lanes.

theorem MathlibNt.SieveTheory.Richert1969.Chen.weightedLowerObject_eq_lower_sub_half_conditioned (N : ℕ) : SwitchingPrinciple.jurkatRichertSourceWeightedCount N = ↑(SwitchingPrinciple.jurkatRichertSourceCandidates N).card - SwitchingPrinciple.jurkatRichertSourceMediumPrimeAggregate N / 2

Chen's displayed weighted object is the lower sieve minus one half of the sum of its prime-conditioned upper sieves.

theorem MathlibNt.SieveTheory.Richert1969.Chen.stieltjesPrimeIntegral : SwitchingPrinciple.ChenJurkatRichertVaryingQPrimeSumAsymptotic

The prime sum is paid by the Stieltjes/partial-summation integral, with the exact coefficient 8 * (log 8 + K / 2).

theorem MathlibNt.SieveTheory.Richert1969.Chen.squarefulCorrection_le (N : ℕ) (hN : 2 ^ 110 < N) (hEven : Even N) : SwitchingPrinciple.jurkatRichertDistinctWeightedCount N - 30 * ↑N ^ (9 / 10) ≤ SwitchingPrinciple.jurkatRichertWeightedCount N

The downstream Chen proper-prime-power correction. This is distinct from Richert's direct (A4) payment for the removed p^2 ∣ a carrier in (3.7).

theorem MathlibNt.SieveTheory.Richert1969.Chen.weightedLowerBound_of_importedTheoremA (hLowerTheoremA : SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hOrdinaryBombieri : BombieriVinogradov.StandardBombieriVinogradov) (hUpperTheoremA : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBombieri : SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound

The Chen-facing conclusion from the two quoted lower/upper Theorem A coefficient dependencies and the two distribution inputs. Theorem A remains an explicit imported dependency; Richert 1969 does not prove it.