Finite bridge from Liu's Selberg square to corrected Chen triples #
This module isolates the exact overlap between Liu's source-pair Selberg square and the corrected Chen triple count. A candidate residual prime contributes unit Selberg weight unless it divides Liu's paper modulus; those exceptional primes remain as an explicit finite residual.
Corrected Chen triples whose first two primes are one fixed Liu source pair.
The ordering p₂ ≤ p₃ and the corrected candidate residual are retained.
Equations
Instances For
The exact exceptional part of a corrected triple slice: the candidate
residual prime divides Liu's paper modulus, so its optimal Selberg packet need
not reduce to the coefficient at 1.
Equations
- MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleQResidual N epsilon p₁ p₂ = ∑ p₃ ∈ Finset.range (N + 1) with Nat.Prime p₃ ∧ p₂ ≤ p₃ ∧ p₁ * p₂ * p₃ ≤ N, if N - p₁ * p₂ * p₃ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N ∧ N - p₁ * p₂ * p₃ ∣ MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus N epsilon then 1 else 0
Instances For
The source pairs common to Liu's characteristic weight and the corrected Chen rectangular switching range.
Equations
- MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourcePairs N = {p ∈ MathlibNt.SieveTheory.LiuWeight.liuWeightPairs N (MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N) (MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N) | MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N ≤ p.1 ∧ p.1 < MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N ≤ p.2}
Instances For
The corrected triple count on the exact common source-pair region.
Equations
Instances For
The modulus-dividing residual summed over the exact common source-pair region.
Equations
Instances For
The two possible source-pair contributions of a strict ordered triple to the historical switched sum.
Equations
Instances For
The historical chenF fibre has the same exact one-or-two multiplicity as
Liu's source weight: the smaller large prime always contributes, while the
larger contributes exactly on the additional square-cutoff subregion.
On common integer and real cutoffs, historical chenOmega source fibres
and the source-pair carrier underlying Liu's square count have exactly the same
local multiplicity. The square count additionally weights each carrier element
by its squared divisor packet.
A product of three primes has exactly three prime factors with
multiplicity, so it is not a P₂.
A historical W-candidate with a strict three-prime complement belongs to the bad fibre.
On a strict ordered squarefree triple, the corrected penalty is exactly two: one unit from the medium-prime multiplicity and one from the canonical ordered-triple witness.
The exact strict-triple value of the corrected candidate penalty.
The honest finite carrier behind the corrected triple-factor sum. Its
elements are candidate residuals together with the first prime factor; the
larger two prime factors remain existential, exactly as in
tripleFactorCount.
Equations
- MathlibNt.SieveTheory.LiuWeight.correctedChenFirstFactorCarrier N = (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N).sigma fun (p : ℕ) => {p₁ ∈ Finset.range (N - p + 1) | Nat.Prime p₁ ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N ≤ p₁ ∧ p₁ < MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N ∧ ∃ (p₂ : ℕ) (p₃ : ℕ), Nat.Prime p₂ ∧ Nat.Prime p₃ ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N ≤ p₂ ∧ p₂ ≤ p₃ ∧ p₁ * p₂ * p₃ = N - p ∧ p₁ < p₂ ∧ p₂ ≤ p₃}
Instances For
The finite ordered-triple carrier counted by the common Liu source region.
Equations
- MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCarrier N = (MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourcePairs N).sigma fun (p : ℕ × ℕ) => {p₃ ∈ {p₃ ∈ Finset.range (N + 1) | Nat.Prime p₃ ∧ p.2 ≤ p₃ ∧ p.1 * p.2 * p₃ ≤ N} | N - p.1 * p.2 * p₃ ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N}
Instances For
The lower-cutoff endpoint fibre, represented by its candidate residual. Divisibility by the fixed first factor is all that is needed for the ensuing cardinality bound.
Equations
Instances For
The upper-cutoff endpoint fibre, represented by the candidate residual and the first prime factor.
Equations
- MathlibNt.SieveTheory.LiuWeight.correctedChenUpperEndpointCarrier N = (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N).sigma fun (p : ℕ) => {p₁ ∈ Finset.range (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) | Nat.Prime p₁ ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N ≤ p₁ ∧ p₁ * MathlibNt.SieveTheory.LiuWeight.liuSourceY3 N ∣ N - p}
Instances For
Conditions on the ordered pair of larger factors selected from one first-factor witness.
Equations
Instances For
A fixed ordered pair of larger factors for a member of the honest first-factor carrier. It is used only to inject that carrier into the source and endpoint fibres; no multiplicity assertion is made.
Equations
- MathlibNt.SieveTheory.LiuWeight.correctedChenSelectedLargeFactors N p p₁ = if h : ∃ (q : ℕ × ℕ), MathlibNt.SieveTheory.LiuWeight.correctedChenLargeFactorConditions N p p₁ q then Classical.choose h else (0, 0)
Instances For
The selected larger factors satisfy all the ordered-factor conditions for members of the first-factor carrier.
The selected-factor map sends a first-factor witness either to the common source triple, to the lower endpoint, or to the upper endpoint.
Equations
- MathlibNt.SieveTheory.LiuWeight.correctedChenSourceEndpointMap N x = if x.snd = MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N then Sum.inr (Sum.inl x.fst) else have q := MathlibNt.SieveTheory.LiuWeight.correctedChenSelectedLargeFactors N x.fst x.snd; if (x.snd, q.1) ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourcePairs N then Sum.inl ⟨(x.snd, q.1), q.2⟩ else Sum.inr (Sum.inr x)
Instances For
The corrected triple-factor sum is exactly the cardinality of its first-factor carrier. In particular, this does not identify the summand with the multiplicity of ordered triples.
The common Liu source count is exactly the cardinality of its ordered triple carrier.
Once Liu's lower cutoff has reached 2, it is exactly the corrected Chen
lower cutoff; the latter differs only by its small-N guard.
The floor source split never exceeds the corrected ceiling split.
The corrected ceiling split is at most one beyond Liu's floor split.
Thus the only upper-cutoff mismatch is the single integer endpoint.
A corrected ordered triple lies in Liu's source carrier unless one of the two integer cutoff endpoints is attained.
Away from the two displayed endpoints, corrected ordered triples are
literally Liu source pairs; the product-square condition follows from
p₂ ≤ p₃.
The selected-factor map lands in the disjoint union of the common source carrier and the two endpoint fibres.
The selected-factor map is injective on the honest first-factor carrier.
In the source branch the candidate residual is recovered from
p = N - p₁p₂p₃; the endpoint branches retain enough coordinates directly.
Exact finite-carrier accounting gives the corrected first-factor carrier as a subcardinal of the common source triples plus the two endpoint fibres.
The aggregate corrected triple-factor sum is bounded by the exact common source count plus the two explicit endpoint-cardinality fibres.
The lower endpoint candidates inject into the quotient interval modulo the fixed lower cutoff.
The upper endpoint pairs inject into a quotient interval times the first-factor interval.
Together the two cutoff fibres have the unconditional
13 * N^(9/10) power-saving bound once the lower floor cutoff has reached
2.
The complete corrected triple-factor sum differs from the common Liu
source count by at most 13 * N^(9/10).
Hence the endpoint complement is smaller than every fixed inverse-log scale.
Each fixed source-pair residual injects into the prime factors of Liu's
paper modulus via the candidate residual N - p₁p₂p₃.
Reindex an arbitrary sum against Liu's characteristic source by its unique admissible ordered prime pair.
The unique product map identifies Liu's pair carrier with the supported source integers.
Every prime factor of Liu's paper modulus lies below its defining cutoff.
Summing the fixed-pair injection bounds the complete source residual by the source-pair cardinality times the number of prime factors of the paper modulus.
A completely finite envelope for the modulus-dividing source residual.
The source support and the paper-modulus cutoff give an unconditional
N^(11/12) power saving for the exceptional residual.
Consequently the modulus-dividing source residual is smaller than every fixed inverse logarithmic scale.
Liu's square count is exactly the sum of its Selberg packets over the admissible source pairs and third primes.
Away from candidate residual primes dividing Liu's paper modulus, one corrected triple slice is bounded by the corresponding optimal Selberg square slice. The exceptional primes are retained exactly in the final summand.
On the exact common source-pair region, the corrected triple count is bounded by Liu's optimal square count plus only the explicit modulus-dividing candidate-prime residual.
The inverse-log residual contract between the corrected ordered-triple sum and Liu's exact source-pair count.
Equations
- MathlibNt.SieveTheory.LiuWeight.LiuSelbergCorrectedSourceComplementResidualBound = ∀ (A : ℝ), 0 < A → ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, Even N → ∑ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N, MathlibNt.SieveTheory.SwitchingPrinciple.tripleFactorCount (N - p) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenZ N) (MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N) ≤ MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCount N + C * ↑N / Real.log ↑N ^ A
Instances For
The explicit endpoint-fibre power saving unconditionally inhabits the source-complement residual contract.
The canonical Pan--Wang--Ding square estimate controls the complete
corrected Chen triple term unconditionally at the endpoint seam. The
paper-modulus residual is discharged by the unconditional N^(11/12) estimate
above.
The canonical Liu--Pan coprime theorem produces the strict ordered-triple upper-bound contract consumed by the generic Jurkat--Richert endpoint. This is a producer of the remaining penalty input, not another Chen endpoint consumer.
Backward-compatible wrapper for the stronger canonical source contract.
An inverse-log remainder is absorbed into an arbitrary positive multiple of the genuine Liu singular-series scale. The uniform lower bound is the positive universal Euler product, since every divisor correction factor is at least one.
The final Chen theorem from the derived Jurkat--Richert weighted lower API and the Liu--Pan--Wang--Ding aggregate theorem. This broad intermediate interface is retained for downstream compatibility.
Backward wrapper from the stronger canonical source contract.
Source-faithful wrapper from literal Corollary (2.30).
The canonical internal Chen endpoint from the five remaining literature
interfaces: generic lower Rosser density, standard Bombieri--Vinogradov, upper
Rosser density, varying-q weighted Bombieri--Vinogradov, and
Liu--Pan--Wang--Ding.
Backward wrapper for the former stronger Pan hypothesis.
Source-faithful literature endpoint from literal Corollary (2.30).
An inverse-log remainder is absorbed into an arbitrary positive multiple of
the truncated main scale. The uniform lower bound 𝔖_trunc ≥ 1/2 is used
explicitly here.
The canonical corrected-triple estimate in the analytic truncation units.
The Euler-tail margin ηs and inverse-log absorption margin ηr remain
separate in the coefficient.
The existing q1/proper-power reduction with its two contributions kept
visible: Cq from q1 and 1/2 from proper prime powers.
Diagnostic corrected-penalty assembly. Besides the Pan--Wang--Ding contract, the only analytic input is the q¹ bound. The fixed Pan level cannot meet the displayed final numerical inequality, even with optimal weights, so this theorem records the obstruction rather than a canonical final route.
Diagnostic Liu--Pan--Wang--Ding Omega assembly with the q¹ bound supplied by the direct weighted aggregate theorem. Its fixed-level coefficient is larger than the available final budget.
Diagnostic corrected-Chen endpoint whose q¹ input is exactly the weighted aggregate theorem consumed by the finite q¹ reduction. The numerical hypothesis is incompatible with the fixed Pan level.
Source-faithful W-side specialization of the diagnostic weighted-aggregate q¹ endpoint.
Diagnostic Liu--Pan--Wang--Ding Omega assembly from the stronger cutoff-free full-divisor-lane delta-one predicates.
Diagnostic corrected-Chen endpoint retaining the stronger full-lane delta-one assumptions for audit compatibility.
Source-faithful W-side specialization of the diagnostic full-lane q¹ endpoint.
Public Chen theorem from the derived Jurkat--Richert weighted lower API. This broad intermediate interface is retained for downstream compatibility.
Backward public wrapper from the stronger canonical source contract.
Public source-faithful wrapper from literal Corollary (2.30).
Canonical public form of Chen's theorem, conditional exactly on the generic
dimension-one lower Rosser density fundamental lemma, standard
Bombieri--Vinogradov, the upper Rosser density fundamental lemma, varying-q
weighted Bombieri--Vinogradov, and the Liu--Pan--Wang--Ding theorem.
Backward public endpoint from the stronger canonical source contract.
Public source-faithful endpoint from literal Corollary (2.30).