All-character nonprincipal Vaughan ledger and Type-II scale audit

This module only assembles proved producers. It keeps the principal character out, keeps the full prefix maximum on the all-character side, and records that the currently proved tensor Type-II estimate is only an endpoint estimate. Consequently no Standard Bombieri--Vinogradov theorem is claimed.

def AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff : ℤ → ℂ

The coefficient 1, used to specialize Vaughan's identity to Λ.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff x✝ = 1

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

One conductor-weighted primitive prefix-maximal lane.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanConductorPrefixLane a N Q = ∑ d ∈ Finset.Icc 2 Q, AnalyticNumberTheory.LargeSieve.imprimitiveConductorWeight Q d * ∑ ψ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter d, AnalyticNumberTheory.LargeSieve.primitiveCharacterPrefixMaxSquare a 0 N d ψ

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

The closed Λ-specific conductor correction, with every N,Q,log factor kept literal.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanLambdaConductorCorrectionScale N Q = 2 * ↑Q ^ 2 * (2 * ↑Q.log2 * (↑N.log2 + 1) * Real.log ↑N) ^ 2

theorem AnalyticNumberTheory.LargeSieve.vaughanLambdaCoeff_unit_eq (n : ℤ) : vaughanLambdaCoeff vaughanUnitIntegerCoeff n = vonMangoldtIntegerCoeff n

theorem AnalyticNumberTheory.LargeSieve.weighted_allCharacter_nonprincipal_vaughan_analytic_ledger (N Q u v : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, characterPrefixMaxSquare χ vonMangoldtIntegerCoeff 0 N ≤ 6 * (vaughanConductorPrefixLane (vaughanTypeICoeff vaughanUnitIntegerCoeff u v) N Q + vaughanConductorPrefixLane (vaughanTypeIICoeff vaughanUnitIntegerCoeff u v) N Q + vaughanConductorPrefixLane (vaughanSmallCoeff vaughanUnitIntegerCoeff v) N Q) + vaughanLambdaConductorCorrectionScale N Q

The real all-character, nonprincipal Vaughan ledger. This theorem combines (1) exact conductor grouping, (2) the full prefix-maximal three-piece Vaughan identity, and (3) the proved Λ-specific Q² polylog change-level correction. The principal character is absent from the left side and is not estimated here.

noncomputable def AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale (N Q C k B : ℕ) : ℝ

The exact endpoint-only Type-II scale delivered by the current producers on one conductor window C ≤ conductor ≤ 2C and one Vaughan outer shell 2^k. It includes, in order: linear imprimitive transport, outer Möbius Cauchy, the primitive large-sieve charge, and the unconditional constant-27 tensor moment.

Equations

• AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale N Q C k B = ↑(Q / C) * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor (Q / C) * ↑(2 ^ k) * (↑N + (2 * ↑⌈Real.log (↑(2 * C) ^ 2) / Real.log 2⌉₊ + 12) * ↑(2 * C) ^ 2) * (27 * ↑B ^ 2 * ↑N * Real.log ↑(N + 1) ^ 5)

theorem AnalyticNumberTheory.LargeSieve.weighted_imprimitive_vaughanTypeII_endpoint_window_unconditional (N Q C u v k l B : ℕ) (hC : 0 < C) (hB : ∀ n ≤ N, ‖vaughanUnitIntegerCoeff ↑n‖ ≤ ↑B) : ∑ d ∈ Finset.Icc C (2 * C), imprimitiveConductorWeight Q d * ∑ ψ : PrimitiveCharacter d, ‖vaughanTypeIICanonicalBilinearBlock (fun (x : ℕ) => 1) N N u v k l d ψ‖ ^ 2 ≤ existingTypeIIEndpointWindowScale N Q C k B

Actual assembly of the current Type-II producers. This is deliberately an endpoint square at y=N, not a maximum over all prefixes.

theorem AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale_split (N Q C k B : ℕ) : existingTypeIIEndpointWindowScale N Q C k B = 27 * ↑B ^ 2 * ↑(Q / C) * conductorHarmonicFactor (Q / C) * ↑(2 ^ k) * Real.log ↑(N + 1) ^ 5 * (↑N ^ 2 + ↑N * ((2 * ↑⌈Real.log (↑(2 * C) ^ 2) / Real.log 2⌉₊ + 12) * ↑(2 * C) ^ 2))

Algebraic payment audit: the length term of the primitive large sieve pays N a second time after the tensor moment has already paid its physical row mass N; the outer-shell Cauchy separately pays 2^k.

theorem AnalyticNumberTheory.LargeSieve.existingTypeIIEndpointWindowScale_not_BV_saving (N Q C k B A : ℕ) (hN : 0 < N) (hBC : C ≤ Q) (hC : 0 < C) (hB : 0 < B) (hlog : 1 < Real.log ↑(N + 1) ^ A) : ¬existingTypeIIEndpointWindowScale N Q C k B ≤ ↑B ^ 2 * ↑N ^ 2 / Real.log ↑(N + 1) ^ A

Formal scale obstruction. Once every non-log factor is at least one, the current endpoint Type-II route is at least 27 B² N² log(N+1)^5; hence it cannot supply an inverse-log saving over the square-mean BV benchmark B²N²/log^A. This is a statement about this produced majorant, not a lower bound on the true character sum.

def AnalyticNumberTheory.LargeSieve.VaughanTypeIIPrefixTensorRepair (N Q u v A : ℕ) (K : ℝ) : Prop

Minimal missing Type-II interface. Unlike the proved endpoint theorem, this contract retains the maximum over every prefix before summing over characters and conductors, and it asks for the inverse-log square-mean scale with no repeated outer-shell/row-length payment. It is intentionally a named Prop, not asserted as a theorem.

Equations

• AnalyticNumberTheory.LargeSieve.VaughanTypeIIPrefixTensorRepair N Q u v A K = (AnalyticNumberTheory.LargeSieve.vaughanConductorPrefixLane (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N Q ≤ K * ↑N ^ 2 / Real.log ↑(N + 1) ^ A)