Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiChenVaryingFamilyLowerDensity

Uniform Suzuki lower density for Chen's varying source family #

This is the first production consumer of the uniform-in-sieve Lemma 14.7. Its constant is chosen before the varying family jurkatRichertSourceBoundingSieve N; the proof then uses the literal Chen floor level, adaptive supported-carrier depth, and the exact Euler/main-sum bridges. No conclusion-shaped comparison premise is used.

Increasing the displayed dimension-one constant preserves the local-product bound. This lets the source witness, which is stated with 1 < K, meet the literal all-depth consumer's harmless normalization 2 ≤ K.

theorem MathlibNt.SieveTheory.chen_le_tenth_rpow_imp_lt_chenZ {N p : } {ε : } (hN : 1 N) (_hε0 : 0 ε) ( : ε < 1 / 10) (hp : p N ^ (1 / 10)) :

The floor in Chen's level makes the Suzuki cutoff strictly larger even when a source prime lies exactly at the real tenth-power endpoint.

On Chen's interval, the natural Suzuki cutoff is no larger than the natural floor level. This is the missing finite-carrier bridge needed by the exact mainSum theorem.

Chen's varying source family satisfies the eventual lower-density estimate with one Suzuki constant selected before the family varies. The fixed source parameters are exactly (d, Δ, Θ) = (16, 1/2, 7).

The conclusion is at Chen's literal floor level and uses the production lower Rosser weight. The arbitrary positive ρ absorbs the complete adaptive-depth Suzuki error uniformly in the growing supported carrier.

The source-contract-relative Chen/Jurkat--Richert base lower-density fundamental lemma, obtained directly from the natural-ceiling varying-family producer rather than through the stronger generic real-parameter comparison.

The exact finite lower-Rosser expansion turns the density theorem above into Chen's base lower-sieve fundamental lemma, still retaining the genuine finite Goldbach remainder.

Chen's base lower asymptotic after the Suzuki source contract and the genuine standard Bombieri--Vinogradov input. The former now supplies the complete lower sieve; the only remaining premise here is the named distribution theorem.