Exact primitive Gauss-to-Farey square-ledger bridge

This module deliberately stops before enlarging primitive characters to all characters. It records the exact Gauss expansion of each primitive character interval sum, keeps both the Gauss factor and the reciprocal-totient weight, and isolates the one finite numerical estimate needed before the additive Farey large sieve can be applied.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveIntervalAmplitude {q : ℕ} (b : ℤ → ℂ) (M : ℤ) (N : ℕ) (χ : PrimitiveCharacter q) : ℂ

The interval sum in the primitive-character square ledger.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveIntervalAmplitude b M N χ = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), b n * ↑χ ↑n

noncomputable def AnalyticNumberTheory.LargeSieve.reducedAdditiveAmplitude (q : ℕ) (b : ℤ → ℂ) (M : ℤ) (N a : ℕ) : ℂ

The additive amplitude at the canonical reduced frequency a/q.

Equations

• AnalyticNumberTheory.LargeSieve.reducedAdditiveAmplitude q b M N a = ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), AnalyticNumberTheory.LargeSieve.charReal (↑n * ↑a / ↑q) * b n

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveReducedGaussAmplitude {q : ℕ} (b : ℤ → ℂ) (M : ℤ) (N : ℕ) (χ : PrimitiveCharacter q) : ℂ

The coherent reduced-frequency Gauss expansion belonging to one primitive character. The character coefficient remains inside the norm.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveReducedGaussAmplitude b M N χ = ∑ a ∈ AnalyticNumberTheory.LargeSieve.reducedResidues q, (↑χ)⁻¹ ↑a * AnalyticNumberTheory.LargeSieve.reducedAdditiveAmplitude q b M N a

theorem AnalyticNumberTheory.LargeSieve.primitiveIntervalAmplitude_gauss_exact {q : ℕ} [NeZero q] (b : ℤ → ℂ) (M : ℤ) (N : ℕ) (χ : PrimitiveCharacter q) : gaussSum (↑χ)⁻¹ (primitiveGaussAddChar q) * primitiveIntervalAmplitude b M N χ = primitiveReducedGaussAmplitude b M N χ

Exact primitive Gauss inversion, with no sum over all characters.

theorem AnalyticNumberTheory.LargeSieve.primitiveGaussSquareLedger_exact {q : ℕ} [NeZero q] (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖gaussSum (↑χ)⁻¹ (primitiveGaussAddChar q) * primitiveIntervalAmplitude b M N χ‖ ^ 2 = 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveReducedGaussAmplitude b M N χ‖ ^ 2

Exact square-ledger identity retaining the Gauss factors and the 1 / φ(q) weight. This is the strongest unconditional bridge supplied by the current primitive Gauss/Farey API without introducing all characters.

theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveSquareLedger_eq_reducedGauss {q : ℕ} [NeZero q] (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveIntervalAmplitude b M N χ‖ ^ 2 = 1 / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveReducedGaussAmplitude b M N χ‖ ^ 2

Equivalent AP-normalized form of the exact ledger. The equality uses only |τ(χ⁻¹)|² = q; no character-family enlargement occurs.

def AnalyticNumberTheory.LargeSieve.PrimitiveReducedBesselDirect (q : ℕ) [NeZero q] : Prop

The direct primitive Bessel statement. Its coefficient cancels the retained 1 / φ(q) weight and exposes the unweighted reduced additive energy.

Equations

• AnalyticNumberTheory.LargeSieve.PrimitiveReducedBesselDirect q = ∀ (c : ℕ → ℂ), ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖∑ a ∈ AnalyticNumberTheory.LargeSieve.reducedResidues q, c a * (↑χ)⁻¹ ↑a‖ ^ 2 ≤ ↑q.totient * ∑ a ∈ AnalyticNumberTheory.LargeSieve.reducedResidues q, ‖c a‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.primitiveReducedBesselDirect (q : ℕ) [NeZero q] : PrimitiveReducedBesselDirect q

Direct finite-dimensional Bessel inequality for the primitive-character orthonormal subfamily. The proof never compares the primitive ledger with an all-character energy.

theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveSquareLedger_le_reducedAdditive_of_directBessel {q : ℕ} [NeZero q] (hB : PrimitiveReducedBesselDirect q) (b : ℤ → ℂ) (M : ℤ) (N : ℕ) : ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveIntervalAmplitude b M N χ‖ ^ 2 ≤ ∑ a ∈ reducedResidues q, ‖reducedAdditiveAmplitude q b M N a‖ ^ 2

Once the direct primitive Bessel estimate is supplied, the exact ledger reduces to the unweighted reduced additive energy. This consumer itself never introduces all characters.

theorem AnalyticNumberTheory.LargeSieve.reducedAdditiveEnergy_reindex_exact (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) : ∑ q ∈ Finset.Icc 1 Q, ∑ a ∈ reducedResidues q, ‖reducedAdditiveAmplitude q b M N a‖ ^ 2 = ∑ qa ∈ reducedFareyIndices Q, ‖∑ n ∈ Finset.Icc (M + 1) (M + ↑N), charReal (↑n * reducedFareyPoint qa) * b n‖ ^ 2

Reindex the complete reduced additive energy by the multiplicity-free Farey index. This is an equality, not a relaxation to unreduced representatives.

theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveSquareLedger_largeSieve_of_directBessel (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) (hB : ∀ (q : ℕ) (hq : q ∈ Finset.Icc 1 Q), PrimitiveReducedBesselDirect q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveIntervalAmplitude b M N χ‖ ^ 2 ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

End-to-end additive large-sieve consumer parameterized by a direct primitive Bessel estimate, retained as a reusable compatibility theorem.

theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveSquareLedger_largeSieve (b : ℤ → ℂ) (M : ℤ) (N Q : ℕ) (hQ : 0 < Q) : ∑ q ∈ Finset.Icc 1 Q, ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveIntervalAmplitude b M N χ‖ ^ 2 ≤ largeSieveBound N (1 / ↑Q ^ 2) * ∑ n ∈ Finset.Icc (M + 1) (M + ↑N), ‖b n‖ ^ 2

Unconditional primitive square-ledger large sieve. Primitive characters are handled as an orthonormal subfamily on the finite unit support, without enlarging the original ledger to all-character energy.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveGaussFareyCellFactor (R L : ℕ) : ℝ

The exact factor delivered by the current production reduced-Farey theorem on a conductor cell (R,2R] and an interval of length L.

This name is intentionally transparent. With the present well-spaced additive large-sieve API it unfolds to L + (2 * ⌈log (4R²) / log 2⌉₊ + 12) * 4R²; in particular no downstream consumer may silently replace it by the sharper classical factor L + 4R².

Equations

• AnalyticNumberTheory.LargeSieve.primitiveGaussFareyCellFactor R L = AnalyticNumberTheory.LargeSieve.largeSieveBound L (1 / ↑(2 * R) ^ 2)

theorem AnalyticNumberTheory.LargeSieve.weightedPrimitiveSquareLedger_cell_largeSieve (b : ℤ → ℂ) (M : ℤ) (L R : ℕ) (hR : 0 < R) : ∑ q ∈ Finset.Ioc R (2 * R), ↑q / ↑q.totient * ∑ χ : PrimitiveCharacter q, ‖primitiveIntervalAmplitude b M L χ‖ ^ 2 ≤ primitiveGaussFareyCellFactor R L * ∑ n ∈ Finset.Icc (M + 1) (M + ↑L), ‖b n‖ ^ 2

Cell-local primitive Gauss--Farey large sieve. Restricting from all q ≤ 2R to the literal cell (R,2R] costs nothing because every summand is nonnegative.

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveGaussFareyDyadicLayerLedger (b : ℕ → ℤ → ℂ) (N R k : ℕ) : ℝ

One dyadic layer of a primitive prefix decomposition on (R,2R]. The coefficient function may depend on the aligned interval j; this lets lane consumers insert their actual grouped coefficient rather than an atomwise triangle majorant.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveGaussFareyDyadicLayerLedger b N R k = ∑ j ∈ Finset.range (N + 1), ∑ q ∈ Finset.Ioc R (2 * R), ↑q / ↑q.totient * ∑ χ : AnalyticNumberTheory.LargeSieve.PrimitiveCharacter q, ‖AnalyticNumberTheory.LargeSieve.primitiveIntervalAmplitude (b j) (↑(j * 2 ^ k)) (2 ^ k) χ‖ ^ 2

noncomputable def AnalyticNumberTheory.LargeSieve.primitiveGaussFareyDyadicLayerCoefficientEnergy (b : ℕ → ℤ → ℂ) (N k : ℕ) : ℝ

The real coefficient energy of the aligned intervals at level k. There is no factor N+1: a lane with one global coefficient sequence proves its intervals disjoint and bounds this exact sum by the global grouped energy.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveGaussFareyDyadicLayerCoefficientEnergy b N k = ∑ j ∈ Finset.range (N + 1), ∑ n ∈ Finset.Icc (↑(j * 2 ^ k) + 1) (↑(j * 2 ^ k) + ↑(2 ^ k)), ‖b j n‖ ^ 2

theorem AnalyticNumberTheory.LargeSieve.primitiveGaussFareyDyadicLayerLedger_le (b : ℕ → ℤ → ℂ) (N R k : ℕ) (hR : 0 < R) : primitiveGaussFareyDyadicLayerLedger b N R k ≤ primitiveGaussFareyCellFactor R (2 ^ k) * primitiveGaussFareyDyadicLayerCoefficientEnergy b N k

Unconditional cell payment for one dyadic layer. This is the exact Gauss--Farey factor times the true coefficient energy, summed over j before any estimate is made.

def AnalyticNumberTheory.LargeSieve.primitiveGaussFareyMediumLongLayers (N R : ℕ) : Finset ℕ

Medium-long dyadic layers are exactly R < 2^k ≤ R².

Equations

• AnalyticNumberTheory.LargeSieve.primitiveGaussFareyMediumLongLayers N R = {k ∈ Finset.range (N.log2 + 1) | R < 2 ^ k ∧ 2 ^ k ≤ R ^ 2}

theorem AnalyticNumberTheory.LargeSieve.primitiveGaussFareyMediumLongLedger_le (b : ℕ → ℕ → ℤ → ℂ) (N R : ℕ) (hR : 0 < R) : ↑(N.log2 + 1) * ∑ k ∈ primitiveGaussFareyMediumLongLayers N R, primitiveGaussFareyDyadicLayerLedger (b k) N R k ≤ ↑(N.log2 + 1) * ∑ k ∈ primitiveGaussFareyMediumLongLayers N R, primitiveGaussFareyCellFactor R (2 ^ k) * primitiveGaussFareyDyadicLayerCoefficientEnergy (b k) N k

Medium-long payment with the single external Rademacher--Menshov factor visible. The right side retains the exact layer length and the true j-summed coefficient energy; hence it is the faithful scale to use when deciding whether a half-budget closes.

def AnalyticNumberTheory.LargeSieve.primitiveGaussFareyUltraLongLayers (N R : ℕ) : Finset ℕ

The layers still requiring a primitive analytic source after the medium-long Gauss--Farey payment: precisely R² < 2^k.

Equations

• AnalyticNumberTheory.LargeSieve.primitiveGaussFareyUltraLongLayers N R = {k ∈ Finset.range (N.log2 + 1) | R ^ 2 < 2 ^ k}