Actual high-conductor Type-II ledger on one canonical shell

The outer row lies in [2^k,2^(k+1)); the collected inner coefficient is cut off by the physical condition r*t ≤ N. Thus every row has the common short length N / 2^k. The theorem below applies the canonical prefix-maximal primitive large sieve row by row and keeps the conductor range R < d ≤ Q.

def AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell (k : ℕ) : Finset ℕ

Canonical outer Type-II shell.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell k = Finset.Ico (2 ^ k) (2 ^ (k + 1))

def AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellLength (N k : ℕ) : ℕ

Common inner length forced by the closed lower endpoint of the shell.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellLength N k = N / 2 ^ k

def AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedRowCoefficient (N r : ℕ) (c : ℕ → ℕ → ℂ) (t : ℤ) : ℂ

One actual collected row, including its physical product cutoff.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedRowCoefficient N r c t = if _ht : 0 < t then if r * t.toNat ≤ N then c r t.toNat else 0 else 0

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellOuterEnergy (k : ℕ) (a : ℕ → ℂ) : ℝ

Outer coefficient energy on the actual shell.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellOuterEnergy k a = ∑ r ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell k, ‖a r‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellTensorEnergy (N k : ℕ) (c : ℕ → ℕ → ℂ) : ℝ

Summed energy of all physically collected rows at the canonical short length.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellTensorEnergy N k c = ∑ r ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell k, ∑ t ∈ Finset.Icc 1 ↑(AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellLength N k), ‖AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedRowCoefficient N r c t‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixSquare (N k y d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

The actual fixed-shell Type-II square for one character and one prefix.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixSquare N k y d a c χ = ‖∑ r ∈ AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell k, a r * ∑ t ∈ Finset.Icc 1 ↑y, AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedRowCoefficient N r c t * ↑χ ↑t‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixMaxSquare (N k d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

The literal maximum over all prefixes of the canonical short row.

Equations

• AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixMaxSquare N k d a c χ = (Finset.image (fun (y : ℕ) => AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixSquare N k y d a c χ) (Finset.range (AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellLength N k + 1))).max' ⋯

noncomputable def AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIFixedShellAmplitude (N k d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : ℝ

AP-normalized amplitude of the actual shell.

Equations

• AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIFixedShellAmplitude N k d a c χ = √(AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixMaxSquare N k d a c χ)

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIICollectedRowCoefficient_eq_zero_of_length_lt {N k r t : ℕ} {c : ℕ → ℕ → ℂ} (hr : r ∈ vaughanTypeIIFixedShell k) (ht : vaughanTypeIIFixedShellLength N k < t) : vaughanTypeIICollectedRowCoefficient N r c ↑t = 0

The physical cutoff and shell lower endpoint force support in the common short interval.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShellPrefixMaxSquare_le_rowLedger (N k d : ℕ) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) (χ : PrimitiveCharacter d) : vaughanTypeIIFixedShellPrefixMaxSquare N k d a c χ ≤ vaughanTypeIIFixedShellOuterEnergy k a * ∑ r ∈ vaughanTypeIIFixedShell k, primitiveCharacterPrefixMaxSquare (vaughanTypeIICollectedRowCoefficient N r c) 0 (vaughanTypeIIFixedShellLength N k) d χ

Row Cauchy for the literal collected shell, with each row controlled by its own complete canonical prefix maximum.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIFixedShell_squareLedger_le (R Q N k : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) : (highConductorPrimitiveSquareLedger R Q fun (d : ℕ) => highConductorVaughanTypeIIFixedShellAmplitude N k d a c) ≤ ↑((vaughanTypeIIFixedShellLength N k).log2 + 1) ^ 2 * primitiveLargeSieveConstant (vaughanTypeIIFixedShellLength N k) Q * (vaughanTypeIIFixedShellOuterEnergy k a * vaughanTypeIIFixedShellTensorEnergy N k c)

Actual collected-shell Type-II square ledger. Primitive conductors stay in R < d ≤ Q; row Cauchy is followed by the canonical row-prefix tensor large sieve at the physically shortened length N / 2^k. No HighConductorTypeIISquareSaving premise occurs.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIIFixedShell_mean_sq_le (R Q N k : ℕ) (hQ : 0 < Q) (a : ℕ → ℂ) (c : ℕ → ℕ → ℂ) : (highConductorPrimitiveMean R Q fun (d : ℕ) => highConductorVaughanTypeIIFixedShellAmplitude N k d a c) ^ 2 ≤ highConductorHarmonicTail R Q * (↑((vaughanTypeIIFixedShellLength N k).log2 + 1) ^ 2 * primitiveLargeSieveConstant (vaughanTypeIIFixedShellLength N k) Q * (vaughanTypeIIFixedShellOuterEnergy k a * vaughanTypeIIFixedShellTensorEnergy N k c))

The AP-normalized 1/φ(d) mean is converted by the genuine conductor Cauchy connector to the proved actual fixed-shell square ledger.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell_diagonal_scale (N k : ℕ) : 2 ^ k * vaughanTypeIIFixedShellLength N k ≤ N

The shortened large-sieve diagonal pays the shell cardinality scale without losing 2^k: 2^k * (N / 2^k) ≤ N.

theorem AnalyticNumberTheory.LargeSieve.vaughanTypeIIFixedShell_largeSieve_scale (N Q k : ℕ) : 2 ^ k * primitiveLargeSieveConstant (vaughanTypeIIFixedShellLength N k) Q ≤ ↑N + 2 ^ k * (2 * ↑⌈Real.log (↑Q ^ 2) / Real.log 2⌉₊ + 12) * ↑Q ^ 2

Exact diagonal/modulus audit after paying a shell energy bounded by 2^k. The shortened diagonal is at most N; the modulus term remains 2^k Q². No power of the conductor cutoff R appears in this rowwise large-sieve step.