Conductor-local input on the actual Vaughan rows

This module specializes the arbitrary-coefficient conductor-local square input at the two row types which occur in the production Type-I and Type-II shell ledgers. It deliberately stops before shell aggregation: the production Type-II fixed-shell family has not yet been identified with the canonical hyperbolic shells in the actual Vaughan decomposition.

def AnalyticNumberTheory.LargeSieve.ConductorLocalPrimitiveLargeSieveSource : Prop

The single allowed high analytic input, with its harmless positive constant existentially packaged.

Equations

• AnalyticNumberTheory.LargeSieve.ConductorLocalPrimitiveLargeSieveSource = ∃ (K : ℝ), 0 < K ∧ AnalyticNumberTheory.LargeSieve.ConductorLocalPrimitiveLargeSieve K

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIRow_mean_le_of_conductorLocal {K : ℝ} (hK : 0 ≤ K) (hLS : ConductorLocalPrimitiveLargeSieve K) (R Q L X : ℕ) (a : ℂ) (b : ℤ → ℂ) (M : ℤ) (hR : 0 < R) (hQ : 0 < Q) (hdiag : ↑L * conductorLocalRowEnergy (vaughanTypeIRowCoefficient a b) M L ≤ ↑X ^ 2) (henergy : conductorLocalRowEnergy (vaughanTypeIRowCoefficient a b) M L ≤ ↑X) : highConductorPrimitiveMean R Q (highConductorVaughanTypeIRowAmplitude a b M L) ≤ K * ↑(L.log2 + 1) * (↑X / √↑R + ↑Q * √↑X)

The arbitrary-row conductor-local estimate specializes directly to every literal Vaughan Type-I row. No Type-I mean estimate is assumed.

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanTypeIICollectedRow_mean_le_of_conductorLocal {K : ℝ} (hK : 0 ≤ K) (hLS : ConductorLocalPrimitiveLargeSieve K) (R Q N k X r : ℕ) (c : ℕ → ℕ → ℂ) (hR : 0 < R) (hQ : 0 < Q) (hdiag : ↑(vaughanTypeIIFixedShellLength N k) * conductorLocalRowEnergy (vaughanTypeIICollectedRowCoefficient N r c) 0 (vaughanTypeIIFixedShellLength N k) ≤ ↑X ^ 2) (henergy : conductorLocalRowEnergy (vaughanTypeIICollectedRowCoefficient N r c) 0 (vaughanTypeIIFixedShellLength N k) ≤ ↑X) : (highConductorPrimitiveMean R Q fun (d : ℕ) (χ : PrimitiveCharacter d) => √(primitiveCharacterPrefixMaxSquare (vaughanTypeIICollectedRowCoefficient N r c) 0 (vaughanTypeIIFixedShellLength N k) d χ)) ≤ K * ↑((vaughanTypeIIFixedShellLength N k).log2 + 1) * (↑X / √↑R + ↑Q * √↑X)

The same analytic input specializes to every physical Type-II collected row, retaining the actual shell length N / 2^k and product cutoff. No fixed-shell or final high-mean estimate is assumed.

theorem AnalyticNumberTheory.LargeSieve.ConductorLocalPrimitiveLargeSieveSource.panPayable (hLS : ConductorLocalPrimitiveLargeSieveSource) (A κ : ℕ) : ∃ (K : ℝ), 0 < K ∧ ConductorLocalPrimitiveLargeSieve K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have C := conductorLocalPanConductorExponent A κ; have B := conductorLocalPanModulusExponent A κ; have R := logConductorThreshold N C; have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; Real.log ↑N ^ κ * (↑N / √↑R + ↑Q * √↑N) ≤ 2 * ↑N / Real.log ↑N ^ A

The packaged square-level source always carries the already-proved scalar Pan payment. This is the complete source-independent terminal scalar step.