Bad-prime compression for conductor change-level corrections

This file is deliberately independent of the existing change-level ledger. It makes the support ¬ IsCoprime n q into a literal union over prime divisors of q, reorders the resulting coefficient energy by prime/multiple, and isolates the exact non-maximal aggregate input needed to replace the old per-character 4 * N Cauchy bound by a dyadic prefix argument.

The finite reductions below contain no prime-number theorem, Bombieri--Vinogradov claim, or new axiom. In particular, ConductorCorrectionBlockBound is a named predicate, not a claimed theorem: it freezes the remaining analytic square-mean estimate in its weakest useful (block, not maximal-prefix) form.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorBadPrimeMultiples (p : ℕ) (M : ℤ) (N : ℕ) : Finset ℤ

Multiples of one candidate bad prime in the ambient integer interval.

Equations

• AnalyticNumberTheory.LargeSieve.conductorBadPrimeMultiples p M N = {n ∈ Finset.Icc (M + 1) (M + ↑N) | ↑p ∣ n}

@[simp]

theorem AnalyticNumberTheory.LargeSieve.mem_conductorBadPrimeMultiples {p : ℕ} {M n : ℤ} {N : ℕ} : n ∈ conductorBadPrimeMultiples p M N ↔ M + 1 ≤ n ∧ n ≤ M + ↑N ∧ ↑p ∣ n

noncomputable def AnalyticNumberTheory.LargeSieve.conductorBadPrimeUnion (q : ℕ) (M : ℤ) (N : ℕ) : Finset ℤ

The union of the prime-multiple fibres attached to a positive level.

Equations

• AnalyticNumberTheory.LargeSieve.conductorBadPrimeUnion q M N = q.primeFactors.biUnion fun (p : ℕ) => AnalyticNumberTheory.LargeSieve.conductorBadPrimeMultiples p M N

theorem AnalyticNumberTheory.LargeSieve.not_isCoprime_iff_exists_primeFactor_dvd {q : ℕ} (hq : 0 < q) (n : ℤ) : ¬IsCoprime n ↑q ↔ ∃ p ∈ q.primeFactors, ↑p ∣ n

A positive-level integer is non-coprime to q exactly when some prime factor of q divides it.

theorem AnalyticNumberTheory.LargeSieve.conductorBadSupport_eq_biUnion_primeMultiples {q : ℕ} (hq : 0 < q) (M : ℤ) (N : ℕ) : conductorBadSupport q M N = conductorBadPrimeUnion q M N

Exact support decomposition into bad-prime/multiple fibres.

theorem AnalyticNumberTheory.LargeSieve.sum_biUnion_le_sum_sum_nonneg {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (t : α → Finset β) (w : β → ℝ) (hw : ∀ (x : β), 0 ≤ w x) : ∑ x ∈ s.biUnion t, w x ≤ ∑ a ∈ s, ∑ x ∈ t a, w x

Union bound for a nonnegative weight, with no disjointness hypothesis.

theorem AnalyticNumberTheory.LargeSieve.conductorBadSupport_energy_le_primeMultiples {q : ℕ} (hq : 0 < q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ∑ n ∈ conductorBadSupport q M N, ‖b n‖ ^ 2 ≤ ∑ p ∈ q.primeFactors, ∑ n ∈ conductorBadPrimeMultiples p M N, ‖b n‖ ^ 2

The bad-support coefficient energy is bounded by the sum of the energies on prime-multiple fibres. This is the useful support compression before any character or modulus Cauchy inequality is taken.

noncomputable def AnalyticNumberTheory.LargeSieve.badPrimeLevelCharacterWeight (Q p : ℕ) : ℝ

Total level/character weight attached to one bad prime. The definition retains exact level weights and exact nonprincipal-character cardinalities.

Equations

• AnalyticNumberTheory.LargeSieve.badPrimeLevelCharacterWeight Q p = ∑ q ∈ Finset.Icc 1 Q with p ∈ q.primeFactors, ↑q / ↑q.totient * ↑(AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q).card

theorem AnalyticNumberTheory.LargeSieve.weighted_badSupport_energy_le_primeFirst (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ _χ ∈ nonprincipalCharacters q, ∑ n ∈ conductorBadSupport q M N, ‖b n‖ ^ 2 ≤ ∑ p ∈ Finset.Icc 2 Q, badPrimeLevelCharacterWeight Q p * ∑ n ∈ conductorBadPrimeMultiples p M N, ‖b n‖ ^ 2

Prime-first form of the elementary bad-support energy majorant. The right side is already grouped by multiples of p; no character-dependent 4*N factor has yet been introduced.

noncomputable def AnalyticNumberTheory.LargeSieve.conductorCorrectionBlockSquare {q : ℕ} (χ : DirichletCharacter ℂ q) (b : ℤ → ℂ) (A : ℤ) (L : ℕ) : ℝ

Squared correction on one interval block.

Equations

• AnalyticNumberTheory.LargeSieve.conductorCorrectionBlockSquare χ b A L = ‖∑ n ∈ Finset.Icc (A + 1) (A + ↑L), AnalyticNumberTheory.LargeSieve.conductorChangeLevelError χ b n‖ ^ 2

def AnalyticNumberTheory.LargeSieve.ConductorCorrectionBlockBound {ι : Type u_1} [Fintype ι] (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (blockStart : ι → ℤ) (blockLength : ι → ℕ) (C : ℝ) : Prop

The genuine remaining analytic input after bad-prime compression and dyadic prefix decomposition. It is only a non-maximal aggregate square-mean estimate for a finite family of interval blocks; it does not assume the desired prefix maximum. A large-sieve proof should establish this after rewriting each block by prime multiples (or by conductor/cofactor Möbius dilation).

Equations

• AnalyticNumberTheory.LargeSieve.ConductorCorrectionBlockBound b M N Q blockStart blockLength C = (∑ i : ι, ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ AnalyticNumberTheory.LargeSieve.nonprincipalCharacters q, AnalyticNumberTheory.LargeSieve.conductorCorrectionBlockSquare χ b (blockStart i) (blockLength i) ≤ C * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2)

theorem AnalyticNumberTheory.LargeSieve.weighted_conductorError_prefixMax_le_of_blockBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] (b : ℤ → ℂ) (M : ℤ) (N Q L : ℕ) (blockStart : ι → ℤ) (blockLength : ι → ℕ) (prefixBlocks : ℕ → Finset ι) (hdecomp : ∀ y ∈ Finset.range (N + 1), ∀ (f : ℤ → ℂ), ∑ n ∈ Finset.Icc (M + 1) (M + ↑y), f n = ∑ i ∈ prefixBlocks y, ∑ n ∈ Finset.Icc (blockStart i + 1) (blockStart i + ↑(blockLength i)), f n) (hcard : ∀ y ∈ Finset.range (N + 1), (prefixBlocks y).card ≤ L) {C : ℝ} (hC : ConductorCorrectionBlockBound b M N Q blockStart blockLength C) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ ∈ nonprincipalCharacters q, conductorErrorPrefixMaxSquare χ b M N ≤ ↑L * C * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Finite Rademacher--Menshov transfer for the change-level correction. This is the advertised replacement for applying full-interval Cauchy separately to every character: the loss is the number L of blocks in one prefix, while the analytic input is an aggregate block square mean.

Scale audit

The closed theorem above shows exactly where the old power loss disappears. An aligned dyadic decomposition has L = log₂ N + 1. Thus a block estimate with

C ≪ (log N)^A * primitiveLargeSieveConstant N Q

gives an aggregate maximal correction of size

≪ (log N)^(A+1) * (N + Q^2 log Q) * ∑ |b(n)|^2.

At Q ≤ sqrt(N) / (log N)^B, only the Q^2 part is reduced to N / (log N)^(2B) (up to the explicit logarithm already present in primitiveLargeSieveConstant). The leading N part is independent of Q. Consequently the level restriction alone does not make this correction N / (log N)^A-negligible for arbitrary coefficients; it merely restores the same power scale as the primitive maximal large sieve and removes the fatal extra factor N. Any claimed logarithmic negligibility still needs a source-specific saving in C (for example, a prime-multiple/conductor-first block square mean with the required inverse-log gain), or a separately proved small energy for the actual coefficient sequence on these prime multiples. Thus the block square-mean predicate above, or an equivalent conductor-first maximal large sieve for the prime-multiple dilations, is the minimal honest analytic input; a stronger all-prefix correction axiom is unnecessary.