Actual pair-shell energy and sharp primitive large sieve on its true dyadic interval. The weight remains the public chen1973Lemma6Eq19I; no printed exponential bridge is asserted here.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_product_mem {x B k m : ℕ} {pp : ℕ × ℕ} (hpp : pp ∈ chen1973Lemma6PrimePairShell x B k m) : pp.1 * pp.2 ∈ Finset.Ioc (B * 2 ^ k) (2 * (B * 2 ^ k))

The actual shell, without a source-parameter premise, maps into (Y,2Y].

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_card (x B k m : ℕ) : (chen1973Lemma6PrimePairShell x B k m).card ≤ B * 2 ^ k

Injectivity of ordered prime products gives at most Y pairs, not x².

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_atom_sq_le {x B k m : ℕ} (hx : 3 ≤ x) (hB : 0 < B) {σ : ℝ} (hσ : 1 / 2 ≤ σ) (v : ℝ) {pp : ℕ × ℕ} (hpp : pp ∈ chen1973Lemma6PrimePairShell x B k m) : ‖chen1973Lemma6Eq19PairAtom x (↑σ + ↑v * Complex.I) pp‖ ^ 2 ≤ 9 * ↑(B * 2 ^ k) ^ (-2 * σ) / Real.log ↑x ^ 2

Pointwise norm bound; the logarithmic lower bound is derived from the actual prime-pair carrier, rather than assumed as an extra region hypothesis.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_energy (x B k m : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (σ v : ℝ) (hσ : 1 / 2 ≤ σ) : ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6Eq19PairAtom x (↑σ + ↑v * Complex.I) pp‖ ^ 2 ≤ 9 * ↑(B * 2 ^ k) ^ (1 - 2 * σ) / Real.log ↑x ^ 2

Uniform dyadic energy bound for Chen's literal pair shell.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pairPolynomial_eq_collected (x B k m : ℕ) (s : ℂ) {d : ℕ} (χ : PrimitiveCharacter d) : ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ↑χ ↑(pp.1 * pp.2) / ((↑pp.1 * ↑pp.2) ^ s * ↑(Real.log (↑x / (↑pp.1 * ↑pp.2)))) = ∑ n ∈ Finset.Icc (↑(B * 2 ^ k) + 1) (↑(B * 2 ^ k) + ↑(B * 2 ^ k)), chen1973Lemma6Eq19PairCoefficient x B k m s n * ↑χ ↑n

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pairCoefficient_square_energy (x B k m : ℕ) (s : ℂ) : ∑ n ∈ Finset.Icc (↑(B * 2 ^ k) + 1) (↑(B * 2 ^ k) + ↑(B * 2 ^ k)), ‖chen1973Lemma6Eq19PairCoefficient x B k m s n‖ ^ 2 = ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6Eq19PairAtom x s pp‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_second_moment_fixed (x L level B k m D Q : ℕ) (s : ℂ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq19PairSecondMoment x L level B k m s ≤ chen1973Lemma6Eq19I x L level * (chen1973Lemma6Eq19SharpConstant * (↑Q + ↑(B * 2 ^ k) / ↑D) * ∑ pp ∈ chen1973Lemma6PrimePairShell x B k m, ‖chen1973Lemma6Eq19PairAtom x s pp‖ ^ 2)

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_second_moment_scalar (x L level B k m D Q : ℕ) (hx : 3 ≤ x) (hB : 0 < B) (σ v : ℝ) (hσ : 1 / 2 ≤ σ) (hD : 0 < D) (hcell : chen1973Lemma6ConductorBlock x L level ⊆ Finset.Ioc D Q) : chen1973Lemma6Eq19PairSecondMoment x L level B k m (↑σ + ↑v * Complex.I) ≤ 9 * chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level / Real.log ↑x ^ 2 * (↑Q + ↑(B * 2 ^ k) / ↑D) * ↑(B * 2 ^ k) ^ (1 - 2 * σ)

Dyadic primitive-LS payment of the original pair second moment. Sharp Lemma 2 is applied with M = Y and N = Y, and its fixed absolute constant is independent of every cell and vertical height.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq19_dyadic_pair_second_moment_source {x L B lastD level k : ℕ} (P : Chen1973Lemma6Eq19SourceParameters x L B lastD level k) (m : ℕ) (σ v : ℝ) (hσ : 1 / 2 ≤ σ) : chen1973Lemma6Eq19PairSecondMoment x L level B k m (↑σ + ↑v * Complex.I) ≤ 9 * chen1973Lemma6Eq19SharpConstant * chen1973Lemma6Eq19I x L level / Real.log ↑x ^ 2 * (↑(chen1973Lemma6Eq19SourceQ L level) + ↑(chen1973Lemma6Eq19PairD B k) / ↑(chen1973Lemma6Eq19SourceD L level)) * ↑(chen1973Lemma6Eq19PairD B k) ^ (1 - 2 * σ)

Literal positive-level source-cell specialization. The interval containment is derived from the real source packet; Eq19I is not replaced by an unproved printed exponential expression.