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.

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleSlice (N p₁ p₂ : ℕ) : ℝ

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

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleSlice N 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 then 1 else 0

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleQResidual (N : ℕ) (epsilon : ℝ) (p₁ p₂ : ℕ) : ℝ

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

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourcePairs (N : ℕ) : Finset (ℕ × ℕ)

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}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCount (N : ℕ) : ℝ

The corrected triple count on the exact common source-pair region.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCount N = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourcePairs N, MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleSlice N p.1 p.2

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleQResidual (N : ℕ) (epsilon : ℝ) : ℝ

The modulus-dividing residual summed over the exact common source-pair region.

Equations

• MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleQResidual N epsilon = ∑ p ∈ MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourcePairs N, MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleQResidual N epsilon p.1 p.2

noncomputable def MathlibNt.SieveTheory.LiuWeight.historicalChenOrderedTripleMultiplicity (N p₁ p₂ p₃ : ℕ) : ℝ

The two possible source-pair contributions of a strict ordered triple to the historical switched sum.

Equations

• MathlibNt.SieveTheory.LiuWeight.historicalChenOrderedTripleMultiplicity N p₁ p₂ p₃ = MathlibNt.SieveTheory.SwitchingPrinciple.chenF N (p₁ * p₂) + MathlibNt.SieveTheory.SwitchingPrinciple.chenF N (p₁ * p₃)

theorem MathlibNt.SieveTheory.LiuWeight.historicalChenOrderedTripleMultiplicity_eq_one_add_indicator {N p₁ p₂ p₃ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hroot₁ : ↑N ^ (1 / 10) < ↑p₁) (hp₁root : ↑p₁ ≤ ↑N ^ (1 / 3)) (hroot₂ : ↑N ^ (1 / 3) < ↑p₂) (hp₂p₃ : p₂ < p₃) (hprod : p₁ * p₂ * p₃ ≤ N) : historicalChenOrderedTripleMultiplicity N p₁ p₂ p₃ = 1 + if p₁ * p₃ ^ 2 ≤ N then 1 else 0

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.

theorem MathlibNt.SieveTheory.LiuWeight.historicalChenOrderedTripleMultiplicity_eq_liu {N z y p₁ p₂ p₃ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hzp₁ : z < p₁) (hp₁y : p₁ ≤ y) (hyp₂ : y < p₂) (hroot₁ : ↑N ^ (1 / 10) < ↑p₁) (hp₁root : ↑p₁ ≤ ↑N ^ (1 / 3)) (hroot₂ : ↑N ^ (1 / 3) < ↑p₂) (hp₂p₃ : p₂ < p₃) (hprod : p₁ * p₂ * p₃ ≤ N) : historicalChenOrderedTripleMultiplicity N p₁ p₂ p₃ = liuOrderedTriplePairMultiplicity N z y p₁ p₂ p₃

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.

theorem MathlibNt.SieveTheory.LiuWeight.strict_ordered_triple_not_isAtMostAlmostPrime_two {p₁ p₂ p₃ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) : ¬Nat.IsAtMostAlmostPrime 2 (p₁ * p₂ * p₃)

A product of three primes has exactly three prime factors with multiplicity, so it is not a P₂.

theorem MathlibNt.SieveTheory.LiuWeight.strict_ordered_triple_mem_chenWBadCandidates {N p p₁ p₂ p₃ : ℕ} (hp : p ∈ SwitchingPrinciple.chenWCandidates N) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hcomplement : N - p = p₁ * p₂ * p₃) : p ∈ SwitchingPrinciple.chenWBadCandidates N

A historical W-candidate with a strict three-prime complement belongs to the bad fibre.

theorem MathlibNt.SieveTheory.LiuWeight.correctedPenalty_of_strict_ordered_triple_eq_two {z y p₁ p₂ p₃ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hzp₁ : z ≤ p₁) (hp₁y : p₁ < y) (hyp₂ : y ≤ p₂) (hp₂p₃ : p₂ < p₃) : SwitchingPrinciple.primePowerSum (p₁ * p₂ * p₃) z y + SwitchingPrinciple.tripleFactorCount (p₁ * p₂ * p₃) z y = 2

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.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenPenalty_eq_two_of_strict_ordered_triple {N p p₁ p₂ p₃ : ℕ} (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hzp₁ : SwitchingPrinciple.correctedChenZ N ≤ p₁) (hp₁y : p₁ < SwitchingPrinciple.correctedChenY N) (hyp₂ : SwitchingPrinciple.correctedChenY N ≤ p₂) (hp₂p₃ : p₂ < p₃) (hcomplement : N - p = p₁ * p₂ * p₃) : SwitchingPrinciple.correctedChenPenalty N p = 2

The exact strict-triple value of the corrected candidate penalty.

noncomputable def MathlibNt.SieveTheory.LiuWeight.correctedChenFirstFactorCarrier (N : ℕ) : Finset ((_ : ℕ) × ℕ)

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₃}

noncomputable def MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCarrier (N : ℕ) : Finset ((_ : ℕ × ℕ) × ℕ)

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}

noncomputable def MathlibNt.SieveTheory.LiuWeight.correctedChenLowerEndpointCarrier (N : ℕ) : Finset ℕ

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

• MathlibNt.SieveTheory.LiuWeight.correctedChenLowerEndpointCarrier N = {p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenCandidates N | MathlibNt.SieveTheory.LiuWeight.liuSourceZ10 N ∣ N - p}

noncomputable def MathlibNt.SieveTheory.LiuWeight.correctedChenUpperEndpointCarrier (N : ℕ) : Finset ((_ : ℕ) × ℕ)

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}

def MathlibNt.SieveTheory.LiuWeight.correctedChenLargeFactorConditions (N p p₁ : ℕ) (q : ℕ × ℕ) : Prop

Conditions on the ordered pair of larger factors selected from one first-factor witness.

Equations

• MathlibNt.SieveTheory.LiuWeight.correctedChenLargeFactorConditions N p p₁ q = (Nat.Prime q.1 ∧ Nat.Prime q.2 ∧ MathlibNt.SieveTheory.SwitchingPrinciple.correctedChenY N ≤ q.1 ∧ q.1 ≤ q.2 ∧ p₁ * q.1 * q.2 = N - p ∧ p₁ < q.1 ∧ q.1 ≤ q.2)

noncomputable def MathlibNt.SieveTheory.LiuWeight.correctedChenSelectedLargeFactors (N p p₁ : ℕ) : ℕ × ℕ

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)

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenSelectedLargeFactors_spec {N : ℕ} {x : (_ : ℕ) × ℕ} (hx : x ∈ correctedChenFirstFactorCarrier N) : correctedChenLargeFactorConditions N x.fst x.snd (correctedChenSelectedLargeFactors N x.fst x.snd)

The selected larger factors satisfy all the ordered-factor conditions for members of the first-factor carrier.

noncomputable def MathlibNt.SieveTheory.LiuWeight.correctedChenSourceEndpointMap (N : ℕ) (x : (_ : ℕ) × ℕ) : (_ : ℕ × ℕ) × ℕ ⊕ ℕ ⊕ (_ : ℕ) × ℕ

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)

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenTripleFactorSum_eq_firstFactorCarrier_card (N : ℕ) : ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) = ↑(correctedChenFirstFactorCarrier N).card

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.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCount_eq_carrier_card (N : ℕ) : liuSelbergCorrectedSourceTripleCount N = ↑(liuSelbergCorrectedSourceTripleCarrier N).card

The common Liu source count is exactly the cardinality of its ordered triple carrier.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenZ_eq_liuSourceZ10_of_two_le {N : ℕ} (hZ : 2 ≤ liuSourceZ10 N) : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N

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.

theorem MathlibNt.SieveTheory.LiuWeight.liuSourceY3_le_correctedChenY (N : ℕ) : liuSourceY3 N ≤ SwitchingPrinciple.correctedChenY N

The floor source split never exceeds the corrected ceiling split.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenY_le_liuSourceY3_add_one (N : ℕ) : SwitchingPrinciple.correctedChenY N ≤ liuSourceY3 N + 1

The corrected ceiling split is at most one beyond Liu's floor split.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenY_eq_liuSourceY3_or_add_one (N : ℕ) : SwitchingPrinciple.correctedChenY N = liuSourceY3 N ∨ SwitchingPrinciple.correctedChenY N = liuSourceY3 N + 1

Thus the only upper-cutoff mismatch is the single integer endpoint.

theorem MathlibNt.SieveTheory.LiuWeight.correctedOrderedTriple_mem_liuWeightPairs_or_cutoff_endpoint {N p₁ p₂ p₃ : ℕ} (hZ : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (_hp₃ : Nat.Prime p₃) (hZp₁ : SwitchingPrinciple.correctedChenZ N ≤ p₁) (hp₁Y : p₁ < SwitchingPrinciple.correctedChenY N) (hYp₂ : SwitchingPrinciple.correctedChenY N ≤ p₂) (hp₂p₃ : p₂ ≤ p₃) (hprod : p₁ * p₂ * p₃ ≤ N) : (p₁, p₂) ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N) ∨ p₁ = liuSourceZ10 N ∨ p₂ = liuSourceY3 N

A corrected ordered triple lies in Liu's source carrier unless one of the two integer cutoff endpoints is attained.

theorem MathlibNt.SieveTheory.LiuWeight.correctedOrderedTriple_mem_liuWeightPairs {N p₁ p₂ p₃ : ℕ} (hZ : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) (hp₃ : Nat.Prime p₃) (hZp₁ : SwitchingPrinciple.correctedChenZ N ≤ p₁) (hp₁Y : p₁ < SwitchingPrinciple.correctedChenY N) (hYp₂ : SwitchingPrinciple.correctedChenY N ≤ p₂) (hp₂p₃ : p₂ ≤ p₃) (hprod : p₁ * p₂ * p₃ ≤ N) (hp₁ne : p₁ ≠ liuSourceZ10 N) (hp₂ne : p₂ ≠ liuSourceY3 N) : (p₁, p₂) ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)

Away from the two displayed endpoints, corrected ordered triples are literally Liu source pairs; the product-square condition follows from p₂ ≤ p₃.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenSourceEndpointMap_mem {N : ℕ} (hZ : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N) {x : (_ : ℕ) × ℕ} (hx : x ∈ correctedChenFirstFactorCarrier N) : correctedChenSourceEndpointMap N x ∈ (liuSelbergCorrectedSourceTripleCarrier N).disjSum ((correctedChenLowerEndpointCarrier N).disjSum (correctedChenUpperEndpointCarrier N))

The selected-factor map lands in the disjoint union of the common source carrier and the two endpoint fibres.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenSourceEndpointMap_injOn (N : ℕ) : Set.InjOn (correctedChenSourceEndpointMap N) ↑(correctedChenFirstFactorCarrier N)

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.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenFirstFactorCarrier_card_le_source_add_endpoints {N : ℕ} (hZ : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N) : (correctedChenFirstFactorCarrier N).card ≤ (liuSelbergCorrectedSourceTripleCarrier N).card + (correctedChenLowerEndpointCarrier N).card + (correctedChenUpperEndpointCarrier N).card

Exact finite-carrier accounting gives the corrected first-factor carrier as a subcardinal of the common source triples plus the two endpoint fibres.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenTripleFactorSum_le_source_add_endpoint_cards {N : ℕ} (hZ : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N) : ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ liuSelbergCorrectedSourceTripleCount N + ↑(correctedChenLowerEndpointCarrier N).card + ↑(correctedChenUpperEndpointCarrier N).card

The aggregate corrected triple-factor sum is bounded by the exact common source count plus the two explicit endpoint-cardinality fibres.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenLowerEndpointCarrier_card_le_div_add_one (N : ℕ) : (correctedChenLowerEndpointCarrier N).card ≤ N / liuSourceZ10 N + 1

The lower endpoint candidates inject into the quotient interval modulo the fixed lower cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenUpperEndpointCarrier_card_le_product (N : ℕ) (hcut : SwitchingPrinciple.correctedChenZ N = liuSourceZ10 N) (hZ : 1 ≤ liuSourceZ10 N) (hY : 1 ≤ liuSourceY3 N) : (correctedChenUpperEndpointCarrier N).card ≤ (N / (liuSourceZ10 N * liuSourceY3 N) + 1) * SwitchingPrinciple.correctedChenY N

The upper endpoint pairs inject into a quotient interval times the first-factor interval.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenEndpointCards_le_thirteen_mul_rpow_nine_tenths (N : ℕ) (hN : 1 ≤ N) (hZ2 : 2 ≤ liuSourceZ10 N) : ↑(correctedChenLowerEndpointCarrier N).card + ↑(correctedChenUpperEndpointCarrier N).card ≤ 13 * ↑N ^ (9 / 10)

Together the two cutoff fibres have the unconditional 13 * N^(9/10) power-saving bound once the lower floor cutoff has reached 2.

theorem MathlibNt.SieveTheory.LiuWeight.correctedChenTripleFactorSum_le_source_add_thirteen_mul_rpow_nine_tenths (N : ℕ) (hN : 1 ≤ N) (hZ2 : 2 ≤ liuSourceZ10 N) : ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ liuSelbergCorrectedSourceTripleCount N + 13 * ↑N ^ (9 / 10)

The complete corrected triple-factor sum differs from the common Liu source count by at most 13 * N^(9/10).

theorem MathlibNt.SieveTheory.LiuWeight.eventually_correctedChenTripleFactorSum_le_source_add_div_log_rpow (A : ℝ) (_hA : 0 < A) : ∀ᶠ (N : ℕ) in Filter.atTop, ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ liuSelbergCorrectedSourceTripleCount N + 13 * ↑N / Real.log ↑N ^ A

Hence the endpoint complement is smaller than every fixed inverse-log scale.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleQResidual_le_primeFactors_card (N : ℕ) (epsilon : ℝ) (p₁ p₂ : ℕ) (hp₁ : Nat.Prime p₁) (hp₂ : Nat.Prime p₂) : liuSelbergCorrectedTripleQResidual N epsilon p₁ p₂ ≤ ↑(liuPaperQModulus N epsilon).primeFactors.card

Each fixed source-pair residual injects into the prime factors of Liu's paper modulus via the candidate residual N - p₁p₂p₃.

theorem MathlibNt.SieveTheory.LiuWeight.sum_liuWeight_mul_eq_sum_pairs (N z y : ℕ) (F : ℕ → ℝ) : ∑ a ∈ Finset.range (N + 1), liuWeight N z y a * F a = ∑ p ∈ liuWeightPairs N z y, F (p.1 * p.2)

Reindex an arbitrary sum against Liu's characteristic source by its unique admissible ordered prime pair.

theorem MathlibNt.SieveTheory.LiuWeight.liuWeightPairs_card_eq_support_card (N z y : ℕ) : (liuWeightPairs N z y).card = (Finset.filter (LiuWeightSupport N z y) (Finset.Icc 1 N)).card

The unique product map identifies Liu's pair carrier with the supported source integers.

theorem MathlibNt.SieveTheory.LiuWeight.liuPaperQModulus_primeFactors_card_le_cutoff_add_one (N : ℕ) (epsilon : ℝ) : (liuPaperQModulus N epsilon).primeFactors.card ≤ paperQSourceCutoff N epsilon + 1

Every prime factor of Liu's paper modulus lies below its defining cutoff.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleQResidual_le_pair_card_mul_primeFactors_card (N : ℕ) (epsilon : ℝ) : liuSelbergCorrectedSourceTripleQResidual N epsilon ≤ ↑(liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N)).card * ↑(liuPaperQModulus N epsilon).primeFactors.card

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.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleQResidual_le_source_cutoff_envelope (N : ℕ) (epsilon : ℝ) : liuSelbergCorrectedSourceTripleQResidual N epsilon ≤ ↑(⌈↑N ^ (2 / 3)⌉₊ + 1) * ↑(paperQSourceCutoff N epsilon + 1)

A completely finite envelope for the modulus-dividing source residual.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleQResidual_le_six_mul_rpow_eleven_twelfths (N : ℕ) (epsilon : ℝ) (hN : 1 ≤ N) (hepsilon : 0 ≤ epsilon) : liuSelbergCorrectedSourceTripleQResidual N epsilon ≤ 6 * ↑N ^ (11 / 12)

The source support and the paper-modulus cutoff give an unconditional N^(11/12) power saving for the exceptional residual.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_liuSelbergCorrectedSourceTripleQResidual_le_div_log_rpow (epsilon A : ℝ) (hepsilon : 0 ≤ epsilon) (_hA : 0 < A) : ∀ᶠ (N : ℕ) in Filter.atTop, liuSelbergCorrectedSourceTripleQResidual N epsilon ≤ 6 * ↑N / Real.log ↑N ^ A

Consequently the modulus-dividing source residual is smaller than every fixed inverse logarithmic scale.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergSquareCount_eq_sum_pairs (N : ℕ) (epsilon : ℝ) (lambda : ℕ → ℝ) : liuSelbergSquareCount N epsilon lambda = ∑ p ∈ liuWeightPairs N (liuSourceZ10 N) (liuSourceY3 N), ∑ p₃ ∈ Finset.range (N + 1) with Nat.Prime p₃ ∧ p.1 * p.2 * p₃ ≤ N, (∑ d ∈ liuSelbergLambdaSourceCarrier N epsilon with d ∣ N - p.1 * p.2 * p₃, lambda d) ^ 2

Liu's square count is exactly the sum of its Selberg packets over the admissible source pairs and third primes.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedTripleSlice_le_square_add_QResidual {N p₁ p₂ : ℕ} {epsilon : ℝ} (hEven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) : liuSelbergCorrectedTripleSlice N p₁ p₂ ≤ ∑ p₃ ∈ Finset.range (N + 1) with Nat.Prime p₃ ∧ p₁ * p₂ * p₃ ≤ N, (∑ d ∈ liuSelbergLambdaSourceCarrier N epsilon with d ∣ N - p₁ * p₂ * p₃, liuSelbergOptimalLambda N epsilon d) ^ 2 + liuSelbergCorrectedTripleQResidual N epsilon p₁ p₂

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.

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceTripleCount_le_square_add_QResidual {N : ℕ} {epsilon : ℝ} (hEven : Even N) (hR : 1 ≤ paperQSourceCutoff N epsilon) : liuSelbergCorrectedSourceTripleCount N ≤ liuSelbergSquareCount N epsilon (liuSelbergOptimalLambda N epsilon) + liuSelbergCorrectedSourceTripleQResidual N epsilon

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.

def MathlibNt.SieveTheory.LiuWeight.LiuSelbergCorrectedSourceComplementResidualBound : Prop

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

theorem MathlibNt.SieveTheory.LiuWeight.liuSelbergCorrectedSourceComplementResidualBound : LiuSelbergCorrectedSourceComplementResidualBound

The explicit endpoint-fibre power saving unconditionally inhabits the source-complement residual contract.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem.eventually_correctedChenOmegaTriple_le (hPan : LiuPanCanonicalCoprimeTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, Even N → ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

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.

theorem MathlibNt.SieveTheory.LiuWeight.liu_pan_wang_ding_strictTriple_upper (hPan : LiuPanCanonicalCoprimeTheorem) : SwitchingPrinciple.ChenJurkatRichertTriplePenaltyUpperBound

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.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_correctedChenOmegaTriple_le (hPan : LiuPanWangDingTheorem) (epsilon A : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hA : 0 < A) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (N : ℕ) in Filter.atTop, Even N → ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ 3.94033 * SingularSeries.liuSingularSeries N * ↑N / Real.log ↑N ^ 2 + C * ↑N / Real.log ↑N ^ A

Backward-compatible wrapper for the stronger canonical source contract.

theorem MathlibNt.SieveTheory.LiuWeight.chens_theorem_of_jurkat_richert_weighted_lower_bound (hJR : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound) (hLiu : LiuPanCanonicalCoprimeTheorem) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

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.

theorem MathlibNt.SieveTheory.LiuWeight.chens_theorem_of_jurkat_richert_weighted_lower_bound_of_liuPanWangDing (hJR : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound) (hLiu : LiuPanWangDingTheorem) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Backward wrapper from the stronger canonical source contract.

theorem MathlibNt.SieveTheory.LiuWeight.chens_theorem_of_jurkat_richert_weighted_lower_bound_of_corollary230 (hJR : SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound) (hLiu : LiuPanWangDingCorollary230) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Source-faithful wrapper from literal Corollary (2.30).

theorem MathlibNt.SieveTheory.LiuWeight.chens_theorem_of_literature_inputs (hLowerDensity : SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hBV : BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) (hLiu : LiuPanCanonicalCoprimeTheorem) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

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.

theorem MathlibNt.SieveTheory.LiuWeight.chens_theorem_of_literature_inputs_of_liuPanWangDing (hLowerDensity : SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hBV : BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) (hLiu : LiuPanWangDingTheorem) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Backward wrapper for the former stronger Pan hypothesis.

theorem MathlibNt.SieveTheory.LiuWeight.chens_theorem_of_literature_inputs_of_corollary230 (hLowerDensity : SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hBV : BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) (hLiu : LiuPanWangDingCorollary230) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Source-faithful literature endpoint from literal Corollary (2.30).

theorem MathlibNt.SieveTheory.LiuWeight.eventually_inverse_log_remainder_le_truncated (C ρ : ℝ) (hρ : 0 < ρ) : ∀ᶠ (N : ℕ) in Filter.atTop, C * ↑N / Real.log ↑N ^ 3 ≤ ρ * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

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.

theorem MathlibNt.SieveTheory.LiuWeight.LiuPanWangDingTheorem.eventually_correctedChenOmegaTriple_le_truncated (hPan : LiuPanWangDingTheorem) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.tripleFactorCount (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ (3.94033 / 2 * (1 + ηs) + ηr) * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

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.

theorem MathlibNt.SieveTheory.LiuWeight.eventually_correctedChenPrimePowerSum_le_of_q1 (Cq : ℝ) (hq1 : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → SwitchingPrinciple.correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → ∑ p ∈ SwitchingPrinciple.correctedChenCandidates N, SwitchingPrinciple.primePowerSum (N - p) (SwitchingPrinciple.correctedChenZ N) (SwitchingPrinciple.correctedChenY N) ≤ (Cq + 1 / 2) * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2

The existing q1/proper-power reduction with its two contributions kept visible: Cq from q1 and 1/2 from proper prime powers.

theorem MathlibNt.SieveTheory.LiuWeight.CorrectedChenOmegaUpperBound_of_liuPanWangDing_q1 (hPan : LiuPanWangDingTheorem) (epsilon ηs ηr Cq : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hq1 : ∀ᶠ (N : ℕ) in Filter.atTop, Even N → SwitchingPrinciple.correctedChenQ1Count N ≤ Cq * AnalyticNumberTheory.Sieve.singularSeriesTruncated N (SwitchingPrinciple.correctedChenZ N - 1) * ↑N / Real.log ↑N ^ 2) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (Cq + 1 / 2)) / 2) : SwitchingPrinciple.CorrectedChenOmegaUpperBound

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.

theorem MathlibNt.SieveTheory.LiuWeight.CorrectedChenOmegaUpperBound_of_liuPanWangDing_q1WeightedAggregate (hLiu : LiuPanWangDingTheorem) (hQ1 : SwitchingPrinciple.Q1WeightedAggregateTheorem) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (SwitchingPrinciple.q1WeightedAggregateConstant hQ1 + 1 / 2)) / 2) : SwitchingPrinciple.CorrectedChenOmegaUpperBound

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.

theorem MathlibNt.SieveTheory.LiuWeight.corrected_chens_theorem_of_liuPanWangDing_q1WeightedAggregate (hW : SwitchingPrinciple.ChenWeightedPanInput) (hLiu : LiuPanWangDingTheorem) (hQ1 : SwitchingPrinciple.Q1WeightedAggregateTheorem) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (SwitchingPrinciple.q1WeightedAggregateConstant hQ1 + 1 / 2)) / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

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.

theorem MathlibNt.SieveTheory.LiuWeight.corrected_chens_theorem_of_liuPanWangDing_sourceFaithful_q1WeightedAggregate {u v : ℕ} (hI : AnalyticNumberTheory.Sieve.PanTypeICharacterMeanValue (fun (N : ℕ) => ↑N) SwitchingPrinciple.chenPanWeightOne u) (hII : AnalyticNumberTheory.Sieve.PanTypeIICharacterMeanValue (fun (N : ℕ) => ↑N) SwitchingPrinciple.chenPanWeightOne u v) (hM : AnalyticNumberTheory.Sieve.PanSourceFaithfulSignedMainBound (fun (N : ℕ) => ↑N) SwitchingPrinciple.chenPanWeightOne u v) (hWTrunc : SwitchingPrinciple.CorrectedChenPanTruncationInput) (hLiu : LiuPanWangDingTheorem) (hQ1 : SwitchingPrinciple.Q1WeightedAggregateTheorem) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (SwitchingPrinciple.q1WeightedAggregateConstant hQ1 + 1 / 2)) / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Source-faithful W-side specialization of the diagnostic weighted-aggregate q¹ endpoint.

theorem MathlibNt.SieveTheory.LiuWeight.CorrectedChenOmegaUpperBound_of_liuPanWangDing_deltaOnePan (hLiu : LiuPanWangDingTheorem) (hQ1Pan : SwitchingPrinciple.Q1DeltaOnePanMeanValue) (hQ1Trunc : SwitchingPrinciple.Q1DeltaOnePanTruncationInput) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (SwitchingPrinciple.q1DeltaOnePanConstant hQ1Pan hQ1Trunc + 1 / 2)) / 2) : SwitchingPrinciple.CorrectedChenOmegaUpperBound

Diagnostic Liu--Pan--Wang--Ding Omega assembly from the stronger cutoff-free full-divisor-lane delta-one predicates.

theorem MathlibNt.SieveTheory.LiuWeight.corrected_chens_theorem_of_liuPanWangDing_deltaOnePan (hW : SwitchingPrinciple.ChenWeightedPanInput) (hLiu : LiuPanWangDingTheorem) (hQ1Pan : SwitchingPrinciple.Q1DeltaOnePanMeanValue) (hQ1Trunc : SwitchingPrinciple.Q1DeltaOnePanTruncationInput) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (SwitchingPrinciple.q1DeltaOnePanConstant hQ1Pan hQ1Trunc + 1 / 2)) / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Diagnostic corrected-Chen endpoint retaining the stronger full-lane delta-one assumptions for audit compatibility.

theorem MathlibNt.SieveTheory.LiuWeight.corrected_chens_theorem_of_liuPanWangDing_sourceFaithful_deltaOnePan {u v : ℕ} (hI : AnalyticNumberTheory.Sieve.PanTypeICharacterMeanValue (fun (N : ℕ) => ↑N) SwitchingPrinciple.chenPanWeightOne u) (hII : AnalyticNumberTheory.Sieve.PanTypeIICharacterMeanValue (fun (N : ℕ) => ↑N) SwitchingPrinciple.chenPanWeightOne u v) (hM : AnalyticNumberTheory.Sieve.PanSourceFaithfulSignedMainBound (fun (N : ℕ) => ↑N) SwitchingPrinciple.chenPanWeightOne u v) (hWTrunc : SwitchingPrinciple.CorrectedChenPanTruncationInput) (hLiu : LiuPanWangDingTheorem) (hQ1Pan : SwitchingPrinciple.Q1DeltaOnePanMeanValue) (hQ1Trunc : SwitchingPrinciple.Q1DeltaOnePanTruncationInput) (epsilon ηs ηr : ℝ) (hepsilon : 0 < epsilon) (hepsilon_le : epsilon ≤ liuEvenAssemblyEpsilon0) (hηs : 0 < ηs) (hηr : 0 < ηr) (hnum : 10 / 3 > (3.94033 / 2 * (1 + ηs) + ηr + (SwitchingPrinciple.q1DeltaOnePanConstant hQ1Pan hQ1Trunc + 1 / 2)) / 2) : ∃ (N₀ : ℕ), ∀ N ≥ N₀, Even N → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ q ≥ 2 ∧ Nat.IsAtMostAlmostPrime 2 q ∧ N = p + q

Source-faithful W-side specialization of the diagnostic full-lane q¹ endpoint.

theorem MathlibNt.ChensTheorem.chens_theorem_of_jurkat_richert_weighted_lower_bound (hJR : SieveTheory.SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound) (hLiu : SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Even n → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ n = p + q

Public Chen theorem from the derived Jurkat--Richert weighted lower API. This broad intermediate interface is retained for downstream compatibility.

theorem MathlibNt.ChensTheorem.chens_theorem_of_jurkat_richert_weighted_lower_bound_of_liuPanWangDing (hJR : SieveTheory.SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound) (hLiu : SieveTheory.LiuWeight.LiuPanWangDingTheorem) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Even n → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ n = p + q

Backward public wrapper from the stronger canonical source contract.

theorem MathlibNt.ChensTheorem.chens_theorem_of_jurkat_richert_weighted_lower_bound_of_corollary230 (hJR : SieveTheory.SwitchingPrinciple.ChenJurkatRichertWeightedLowerBound) (hLiu : SieveTheory.LiuWeight.LiuPanWangDingCorollary230) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Even n → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ n = p + q

Public source-faithful wrapper from literal Corollary (2.30).

theorem MathlibNt.ChensTheorem.chens_theorem_of_literature_inputs (hLowerDensity : SieveTheory.SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hBV : SieveTheory.BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : SieveTheory.SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) (hLiu : SieveTheory.LiuWeight.LiuPanCanonicalCoprimeTheorem) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Even n → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ n = p + q

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.

theorem MathlibNt.ChensTheorem.chens_theorem_of_literature_inputs_of_liuPanWangDing (hLowerDensity : SieveTheory.SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hBV : SieveTheory.BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : SieveTheory.SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) (hLiu : SieveTheory.LiuWeight.LiuPanWangDingTheorem) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Even n → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ n = p + q

Backward public endpoint from the stronger canonical source contract.

theorem MathlibNt.ChensTheorem.chens_theorem_of_literature_inputs_of_corollary230 (hLowerDensity : SieveTheory.SwitchingPrinciple.DimensionOneLowerRosserDensityFundamentalLemma) (hBV : SieveTheory.BombieriVinogradov.StandardBombieriVinogradov) (hUpperDensity : SieveTheory.SwitchingPrinciple.DimensionOneUpperRosserDensityFundamentalLemma) (hWeightedBV : SieveTheory.SwitchingPrinciple.ChenJurkatRichertVaryingQWeightedBombieriVinogradov) (hLiu : SieveTheory.LiuWeight.LiuPanWangDingCorollary230) : ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → Even n → ∃ (p : ℕ) (q : ℕ), Nat.Prime p ∧ Semiprime q ∧ n = p + q

Public source-faithful endpoint from literal Corollary (2.30).