Direct L¹ Vaughan route at the physical scale

This module deliberately does not pass through a square mean for the complete von Mangoldt coefficient sequence. It proves the finite character, conductor, and Vaughan assembly for the literal prefix maxima. The main unresolved analytic interfaces are the Type-I and Type-II mean values themselves; the small/correction terms remain visible, while the reciprocal-totient conductor weight is discharged by a separate unconditional finite-arithmetic module.

noncomputable def AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude (a : ℤ → ℂ) (N q : ℕ) (χ : PrimitiveCharacter q) : ℝ

Unsquared primitive-character prefix maximum.

Equations

• AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude a N q χ = √(AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare a 0 N q χ)

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude_nonneg (a : ℤ → ℂ) (N q : ℕ) (χ : PrimitiveCharacter q) : 0 ≤ primitivePrefixAmplitude a N q χ

theorem AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude_sq (a : ℤ → ℂ) (N q : ℕ) (χ : PrimitiveCharacter q) : primitivePrefixAmplitude a N q χ ^ 2 = primitiveCharacterPrefixMaxSquare a 0 N q χ

noncomputable def AnalyticNumberTheory.LargeSieve.directPrimitiveMean (a : ℤ → ℂ) (N Q : ℕ) : ℝ

The classical direct primitive L¹ mean. This, rather than a square mean of an already collected length-N coefficient sequence, is the proper target of Vaughan's Type-I/II argument.

Equations

• AnalyticNumberTheory.LargeSieve.directPrimitiveMean a N Q = ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, AnalyticNumberTheory.LargeSieve.primitivePrefixAmplitude a N q χ

theorem AnalyticNumberTheory.LargeSieve.directPrimitiveMean_nonneg (a : ℤ → ℂ) (N Q : ℕ) : 0 ≤ directPrimitiveMean a N Q

noncomputable def AnalyticNumberTheory.LargeSieve.directVaughanTypeIMean (N Q u v : ℕ) : ℝ

The three genuine Vaughan means.

Equations

• AnalyticNumberTheory.LargeSieve.directVaughanTypeIMean N Q u v = AnalyticNumberTheory.LargeSieve.directPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N Q

noncomputable def AnalyticNumberTheory.LargeSieve.directVaughanTypeIIMean (N Q u v : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.directVaughanTypeIIMean N Q u v = AnalyticNumberTheory.LargeSieve.directPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N Q

noncomputable def AnalyticNumberTheory.LargeSieve.directVaughanSmallMean (N Q v : ℕ) : ℝ

Equations

• AnalyticNumberTheory.LargeSieve.directVaughanSmallMean N Q v = AnalyticNumberTheory.LargeSieve.directPrimitiveMean (AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff v) N Q

theorem AnalyticNumberTheory.LargeSieve.directPrimitiveMean_vaughan_le (N Q u v : ℕ) : directPrimitiveMean vonMangoldtIntegerCoeff N Q ≤ 2 * (directVaughanTypeIMean N Q u v + directVaughanTypeIIMean N Q u v + directVaughanSmallMean N Q v)

Exact Vaughan decomposition consumed directly in L¹. This is the crucial finite assembly: no N² square-mean target appears.

noncomputable def AnalyticNumberTheory.LargeSieve.directAllCharacterMean (a : ℤ → ℂ) (N Q : ℕ) : ℝ

Direct all-character nonprincipal prefix mean before conductor reduction.

Equations

• AnalyticNumberTheory.LargeSieve.directAllCharacterMean a N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q, AnalyticNumberTheory.LargeSieve.nonprincipalPrefixAmplitude a N q χ

theorem AnalyticNumberTheory.LargeSieve.residue_errors_le_directAllCharacterMean (E : ℕ → ℝ) (N Q : ℕ) (hE : ∀ q ∈ Finset.Icc 1 Q, E q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude vonMangoldtIntegerCoeff N q χ) : ∑ q ∈ Finset.Icc 1 Q, E q ≤ directAllCharacterMean vonMangoldtIntegerCoeff N Q

The starting character-orthogonality step for arbitrary nonnegative residue errors. The caller supplies only the literal one-modulus character expansion.

theorem AnalyticNumberTheory.LargeSieve.direct_sum_nonprincipal_by_conductor (Q : ℕ) (F : (d : ℕ) → PrimitiveCharacter d → ℝ) : ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, F χ.conductor (conductorPrimitiveCharacter χ) = ∑ d ∈ Finset.Icc 2 Q, directConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, F d ψ

Exact conductor regrouping with the direct 1/φ(q) weight.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorErrorAmplitude {q : ℕ} (χ : DirichletCharacter ℂ q) (a : ℤ → ℂ) (N : ℕ) : ℝ

Prefix correction amplitude at change of level.

Equations

• AnalyticNumberTheory.LargeSieve.conductorErrorAmplitude χ a N = √(AnalyticNumberTheory.LargeSieve.conductorErrorPrefixMaxSquare χ a 0 N)

theorem AnalyticNumberTheory.LargeSieve.conductorErrorAmplitude_sq {q : ℕ} (χ : DirichletCharacter ℂ q) (a : ℤ → ℂ) (N : ℕ) : conductorErrorAmplitude χ a N ^ 2 = conductorErrorPrefixMaxSquare χ a 0 N

theorem AnalyticNumberTheory.LargeSieve.conductorErrorAmplitude_nonneg {q : ℕ} (χ : DirichletCharacter ℂ q) (a : ℤ → ℂ) (N : ℕ) : 0 ≤ conductorErrorAmplitude χ a N

theorem AnalyticNumberTheory.LargeSieve.nonprincipalAmplitude_le_conductor {q : ℕ} (χ : DirichletCharacter ℂ q) (a : ℤ → ℂ) (N : ℕ) : nonprincipalPrefixAmplitude a N q χ ≤ 2 * (primitivePrefixAmplitude a N χ.conductor (conductorPrimitiveCharacter χ) + conductorErrorAmplitude χ a N)

noncomputable def AnalyticNumberTheory.LargeSieve.directConductorCorrectionMean (a : ℤ → ℂ) (N Q : ℕ) : ℝ

Literal correction mean; this is separate from the Type-I/II hybrid input.

Equations

• AnalyticNumberTheory.LargeSieve.directConductorCorrectionMean a N Q = ∑ q ∈ Finset.Icc 1 Q, (↑q.totient)⁻¹ * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q, AnalyticNumberTheory.LargeSieve.conductorErrorAmplitude χ a N

theorem AnalyticNumberTheory.LargeSieve.directAllCharacterMean_le_conductor (a : ℤ → ℂ) (N Q : ℕ) : directAllCharacterMean a N Q ≤ 2 * ∑ d ∈ Finset.Icc 2 Q, directConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitivePrefixAmplitude a N d ψ + 2 * directConductorCorrectionMean a N Q

Finite all-character to primitive-conductor L¹ reduction.

theorem AnalyticNumberTheory.LargeSieve.direct_conductor_sum_le_primitive (a : ℤ → ℂ) (N Q : ℕ) : ∑ d ∈ Finset.Icc 2 Q, directConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, primitivePrefixAmplitude a N d ψ ≤ conductorHarmonicFactor Q ^ 2 * directPrimitiveMean a N Q

Compatibility transport to the historical q / φ(q) primitive mean. The stronger production transport is direct_conductor_sum_le_apNormalizedPrimitive in the AP-normalized assembly; this theorem deliberately retains the old majorant for downstream API compatibility only.

def AnalyticNumberTheory.LargeSieve.VaughanDirectTypeIInput (N Q u v : ℕ) (K logPay : ℝ) : Prop

Minimal missing Type-I direct mean input. It is an inequality on the real Vaughan lane, not a BV endpoint and not a conclusion-shaped AP error premise.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanDirectTypeIInput N Q u v K logPay = (AnalyticNumberTheory.LargeSieve.directVaughanTypeIMean N Q u v ≤ K * logPay * (↑N + ↑Q ^ 2 * √↑N))

def AnalyticNumberTheory.LargeSieve.VaughanDirectTypeIIInput (N Q u v : ℕ) (K logPay : ℝ) : Prop

Minimal missing Type-II hybrid mean input. The last term retains the cutoff payment QN/√(u+1) which becomes Q N^(13/14) for u≈N^(1/7).

Equations

• AnalyticNumberTheory.LargeSieve.VaughanDirectTypeIIInput N Q u v K logPay = (AnalyticNumberTheory.LargeSieve.directVaughanTypeIIMean N Q u v ≤ K * logPay * (↑N + ↑Q ^ 2 * √↑N + ↑Q * ↑N / √↑(u + 1)))

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanDirectPhysicalMajorant (N Q u : ℕ) (K logPay : ℝ) : ℝ

The honest physical majorant exposed by the direct route.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanDirectPhysicalMajorant N Q u K logPay = K * logPay * (↑N + ↑Q ^ 2 * √↑N + ↑Q * ↑N / √↑(u + 1))

theorem AnalyticNumberTheory.LargeSieve.direct_L1_vaughan_physical_assembly (E : ℕ → ℝ) (N Q u v : ℕ) (K logPay : ℝ) (hK : 0 ≤ K) (hlogPay : 0 ≤ logPay) (hE : ∀ q ∈ Finset.Icc 1 Q, E q ≤ (↑q.totient)⁻¹ * ∑ χ ∈ nonprincipalCharacters q, nonprincipalPrefixAmplitude vonMangoldtIntegerCoeff N q χ) (hI : VaughanDirectTypeIInput N Q u v K logPay) (hII : VaughanDirectTypeIIInput N Q u v K logPay) : ∑ q ∈ Finset.Icc 1 Q, E q ≤ 4 * conductorHarmonicFactor Q ^ 2 * (2 * vaughanDirectPhysicalMajorant N Q u K logPay + directVaughanSmallMean N Q v) + 2 * directConductorCorrectionMean vonMangoldtIntegerCoeff N Q

Finite substitution of the two minimal analytic inputs. The small lane and change-level correction remain explicit, so this theorem cannot be mistaken for Bombieri--Vinogradov.

theorem AnalyticNumberTheory.LargeSieve.vaughan_cutoff_fourteen_payment (N Q u : ℕ) (R : ℝ) (hR : 0 < R) (hu : R ^ 2 ≤ ↑(u + 1)) (hN : ↑N ≤ R ^ 14) : ↑Q * ↑N / √↑(u + 1) ≤ ↑Q * R ^ 13

Pure cutoff algebra. If u+1 ≥ R² and N ≤ R¹⁴, then the Type-II tail is at most Q R¹³; choosing R=N^(1/14) means u≈N^(1/7).

theorem AnalyticNumberTheory.LargeSieve.vaughan_log_exponent_payment (A C B : ℕ) (L : ℝ) (hL : 1 ≤ L) (hB : A + C + 2 ≤ B) : L ^ (C + 2) / L ^ B ≤ 1 / L ^ A

Log ledger: conductor regrouping contributes two powers. If the direct Type-I/II theorem costs log^C, choosing B ≥ A+C+2 pays all displayed logs in the usual cutoff Q≤√N/log^B. This is exponent bookkeeping only.