The actual Chen--Richert consumer with its sieve inputs discharged

The Goldbach sources have density 1 / (p - 1), not the literal JR1965 density 1 / p. The connection here is analytic, not an identification of the two sieves: the constructed JR delay functions supply the concrete Section 13 majorants, and the existing modern Suzuki comparisons give the required lower and uniformly conditioned upper sieve estimates.

The lower route is already specialized to Chen's varying source family. The upper route uses the proved modern all-depth comparison internally; it is not attributed to the literal 1965 Theorem 5. The public endpoints below concern the actual Chen sources and carry no imported sieve or distribution premise.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenBaseLowerSieve : SwitchingPrinciple.ChenJurkatRichertBaseLowerSieveFundamentalLemma

The actual base Goldbach sieve, including its genuine finite remainder.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenBaseLowerAsymptotic : SwitchingPrinciple.ChenJurkatRichertBaseLowerSieveAsymptotic

The base lower asymptotic after the unconditional modern distribution producer pays the actual Goldbach remainder.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenVaryingQUpperDensity (ε : ℝ) (hε : 0 < ε) (hεSmall : ε < 1 / 60) (δ : ℝ) (hδ : 0 < δ) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → SwitchingPrinciple.jurkatRichertSourceVaryingQMainSum N ε ≤ SwitchingPrinciple.jurkatRichertSourceVaryingQDensityModel N ε + δ * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2

The exact varying-medium-prime density aggregate, with all medium primes paid under one eventual threshold.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenVaryingQUpperAsymptotic : SwitchingPrinciple.ChenJurkatRichertVaryingQUpperSieveAsymptotic

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenDistinctWeightedLowerBound : SwitchingPrinciple.ChenJurkatRichertDistinctWeightedLowerBound

The literal distinct-medium-prime weighted lower bound of Chen Lemma 9.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenWeightedLowerBound : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound

The production weighted lower bound, including the existing correction from the distinct source weight to its valuation-based consumer.

theorem MathlibNt.SieveTheory.JurkatRichert1965ChenRichertConsumer.chenFacingSourceChainCertificate : Richert1969.ChenFacingSourceChainCertificate

The actual Richert source chain with all sieve and distribution inputs discharged. The finite stages retain exactly their original quantifiers.