Conditional uniform level-zero endpoint for Chen equation (21)

Finite character summation and all scalar constant absorption are internal. The actual termwise contour shift and primitive vertical bound remain explicit. No unconditional equation-(21) claim is made, and no positive-level dispatcher is claimed in this module.

def AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21PrimitiveAlphaToLeftShift (x L B k m : ℕ) : Prop

The genuinely primitive contour input still missing from the current production stack. It is termwise and conditional on nonvanishing of the literal equation-(21) line; unlike a terminal hypothesis, it is not a block bound.

Equations

• AnalyticNumberTheory.LargeSieve.Chen1973Lemma6Eq21PrimitiveAlphaToLeftShift x L B k m = ∀ d ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6ConductorBlock x L 0, ∀ (χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d), ∀ pp ∈ AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimePairShell x B k m, (∀ (t : ℝ), AnalyticNumberTheory.LargeSieve.chen1973Lemma6PrimitiveLValue d (AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21Line x t) χ ≠ 0) → AnalyticNumberTheory.LargeSieve.chen1973Lemma6ActualPhi x d χ pp * ↑χ ↑(pp.1 * pp.2) = -AnalyticNumberTheory.LargeSieve.chen1973Lemma6Eq21VerticalIntegral x d χ pp

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_eq21_actual_le_contourMajorant {x L B k m : ℕ} (hline : ∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d) (t : ℝ), chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ ≠ 0) (hshift : Chen1973Lemma6Eq21PrimitiveAlphaToLeftShift x L B k m) : chen1973Lemma6NmBlockActual x L 0 B k m ≤ chen1973Lemma6Eq21ContourMajorant x L B k m

Finite character triangle and the exact termwise shift turn the actual level-zero block into the equation-(21) contour majorant.

theorem AnalyticNumberTheory.LargeSieve.chen1973Lemma6_equation21_levelZero_eventually_of_primitive_inputs (Cvert : ℝ) : ∃ (x₀ : ℕ), ∀ x ≥ x₀, ∀ (L B k m l₂ : ℕ), Chen1973Lemma6Eq21SourceParameters x L B k m l₂ → chen1973Lemma6PrimePairShell x B k m ⊆ chen1973Lemma6Eq21PrimeRegion x → (∀ d ∈ chen1973Lemma6ConductorBlock x L 0, ∀ (χ : PrimitiveCharacter d) (t : ℝ), chen1973Lemma6PrimitiveLValue d (chen1973Lemma6Eq21Line x t) χ ≠ 0) → Chen1973Lemma6Eq21PrimitiveAlphaToLeftShift x L B k m → Chen1973Lemma6Eq21PrimitiveVerticalEstimate Cvert x L B k m → chen1973Lemma6NmBlockActual x L 0 B k m ≤ ↑x / Real.log ↑x ^ 20

For each fixed vertical-estimate constant, one cutoff precedes all source cell parameters. No smallness assumption on that constant or external Mertens or scalar-decay payment is required. The two analytic producers remain open.