Exact lambda-prefix to low/high conductor connector

This module closes the finite normalization gap between the natural-number prefix used by Standard-BV character orthogonality and the integer interval prefix used by conductor regrouping. It then applies the exact low/high Finset partition, with no analytic hypothesis.

theorem AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefix_eq_integerInterval (y q : ℕ) (χ : DirichletCharacter ℂ q) : lambdaCharacterPrefix y q χ = ∑ n ∈ Finset.Icc 1 ↑y, vonMangoldtIntegerCoeff n * χ ↑n

The natural Chebyshev character prefix is exactly the integer interval prefix used by the conductor machinery. The only extra natural term is zero, and Λ(0)=0.

theorem AnalyticNumberTheory.LargeSieve.norm_lambdaCharacterPrefix_sq_le_characterPrefixMaxSquare (N y q : ℕ) (hy : y ≤ N) (χ : DirichletCharacter ℂ q) : ‖lambdaCharacterPrefix y q χ‖ ^ 2 ≤ characterPrefixMaxSquare χ vonMangoldtIntegerCoeff 0 N

The squared norm of every natural lambda prefix is one of the values in the integer-prefix maximum.

theorem AnalyticNumberTheory.LargeSieve.lambdaCharacterPrefixMaxAmplitude_le_nonprincipalPrefixAmplitude (N q : ℕ) (χ : DirichletCharacter ℂ q) : lambdaCharacterPrefixMaxAmplitude N q χ ≤ nonprincipalPrefixAmplitude vonMangoldtIntegerCoeff N q χ

The natural prefix maximum from character orthogonality is bounded by the square-root integer prefix maximum used by conductor regrouping.

theorem AnalyticNumberTheory.LargeSieve.nonprincipalLambdaPhysical_le_directAllCharacterMean (N Q : ℕ) : nonprincipalLambdaPhysical N Q ≤ directAllCharacterMean vonMangoldtIntegerCoeff N Q

The literal lambda nonprincipal mean is bounded by the all-character mean already consumed by the conductor theorem.

theorem AnalyticNumberTheory.LargeSieve.lambdaToLowHighConductorConnector (N Q C : ℕ) : nonprincipalLambdaPhysical N Q ≤ 2 * (lowConductorPhysical N Q C + highConductorPhysical N Q C) + 2 * directConductorCorrectionMean vonMangoldtIntegerCoeff N Q

Exact, premise-free lambda-to-low/high conductor connector.