Actual Vaughan square ledgers produce the moving high source

The sole analytic input in this file is a square-ledger theorem for the three literal Vaughan coefficient rows on the retained primitive-conductor interval. In particular, it is not an estimate for the final unsquared high mean. The fixed exponent κ is the complete reserve for shell counts, prefix maxima, Möbius/logarithmic convolution coefficients, and the conductor/Abel envelopes.

noncomputable def AnalyticNumberTheory.LargeSieve.actualVaughanRowsSquareLedger (N Q C u v : ℕ) : ℝ

The sum of the three literal Vaughan square ledgers on the actual high conductor set. The Type-I and Type-II entries are the production coefficients, not abstract test rows and not high-mean conclusions.

Equations

• AnalyticNumberTheory.LargeSieve.actualVaughanRowsSquareLedger N Q C u v = AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C) + AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff u v) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C) + AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn (AnalyticNumberTheory.LargeSieve.vaughanSmallCoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff v) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)

theorem AnalyticNumberTheory.LargeSieve.actualVaughanRowsSquareLedger_nonneg (N Q C u v : ℕ) : 0 ≤ actualVaughanRowsSquareLedger N Q C u v

def AnalyticNumberTheory.LargeSieve.ActualVaughanRowsSquareLedgerSource (κ : ℕ) : Prop

The fixed polylogarithmic reserve attached to the actual shell aggregation. The inequality is deliberately frozen at square-ledger level. Its left side contains the exact Abel/conductor envelopes and the exact production Vaughan rows; it neither mentions StandardBVHighTypeITypeIIHybridMovingSource nor assumes an unsquared high mean.

The established production ingredients feeding this interface are:

• the uniform Type-I μ/log convolution moment with exponent 5;
• the actual first/product-dyadic Type-I row partition;
• the canonical hyperbolic Type-II collected-prefix partition and its fixed-row prefix ledger; and
• one finite Cauchy payment for the three Vaughan lanes.

Equations

• AnalyticNumberTheory.LargeSieve.ActualVaughanRowsSquareLedgerSource κ = ∀ (A C B : ℕ), ∃ (u : ℕ → ℕ) (v : ℕ → ℕ) (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have R := AnalyticNumberTheory.LargeSieve.logConductorThreshold N C; have P := 4 * AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q ^ 2; P ^ 2 * (3 * AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor Q R * AnalyticNumberTheory.LargeSieve.actualVaughanRowsSquareLedger N Q C (u N) (v N)) ≤ (K * ↑N / Real.log ↑N ^ (A + κ)) ^ 2

def AnalyticNumberTheory.LargeSieve.ActualVaughanRowsChosenSquareLedgerSource (κ : ℕ) : Prop

Canonical square-ledger source with faithful quantifier order: for each requested decay A, choose B,C first, then u,v,K. The margin on B is exactly the one required by the Standard-BV elementary payload.

Equations

• AnalyticNumberTheory.LargeSieve.ActualVaughanRowsChosenSquareLedgerSource κ = ∀ (A : ℕ), ∃ (B : ℕ) (C : ℕ), A + 3 ≤ B ∧ ∃ (u : ℕ → ℕ) (v : ℕ → ℕ) (K : ℝ), 0 < K ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have R := AnalyticNumberTheory.LargeSieve.logConductorThreshold N C; have P := 4 * AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q ^ 2; P ^ 2 * (3 * AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor Q R * AnalyticNumberTheory.LargeSieve.actualVaughanRowsSquareLedger N Q C (u N) (v N)) ≤ (K * ↑N / Real.log ↑N ^ (A + κ)) ^ 2

def AnalyticNumberTheory.LargeSieve.ActualVaughanRowsComponentwiseChosenSquareLedgerSource (κ : ℕ) : Prop

Source-faithful separated chosen source. Its only analytic inputs are the exact production Type-I and Type-II ledgers. Both are evaluated at the shared chosen cutoff; the exact small coefficient is paid internally by the adapter.

Equations

• AnalyticNumberTheory.LargeSieve.ActualVaughanRowsComponentwiseChosenSquareLedgerSource κ = ∀ (A : ℕ), ∃ (B : ℕ) (C : ℕ), A + 3 ≤ B ∧ ∃ (u : ℕ → ℕ) (v : ℕ → ℕ), v = AnalyticNumberTheory.LargeSieve.standardBVBalancedSmallCutoff ∧ ∃ (K₁ : ℝ) (K₂ : ℝ), 0 < K₁ ∧ 0 < K₂ ∧ ∀ᶠ (N : ℕ) in Filter.atTop, have Q := MathlibNt.SieveTheory.LiuWeight.panModulusCutoff N ↑B; have R := AnalyticNumberTheory.LargeSieve.logConductorThreshold N C; have P := 4 * AnalyticNumberTheory.LargeSieve.discreteAbelAmplifierPrefixMax N * AnalyticNumberTheory.LargeSieve.conductorHarmonicFactor Q ^ 2; have X := ↑N / Real.log ↑N ^ (A + κ); P ^ 2 * (3 * AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor Q R * AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn (AnalyticNumberTheory.LargeSieve.vaughanTypeICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff (u N) (v N)) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)) ≤ (K₁ * X) ^ 2 ∧ P ^ 2 * (3 * AnalyticNumberTheory.LargeSieve.highConductorHarmonicFactor Q R * AnalyticNumberTheory.LargeSieve.primitivePrefixSquareLedgerOn (AnalyticNumberTheory.LargeSieve.vaughanTypeIICoeff AnalyticNumberTheory.LargeSieve.vaughanUnitIntegerCoeff (u N) (v N)) N (AnalyticNumberTheory.LargeSieve.highConductorSet N Q C)) ≤ (K₂ * X) ^ 2

theorem AnalyticNumberTheory.LargeSieve.actualVaughanRowsChosenSquareLedgerSource_of_componentwise {κ : ℕ} (hrows : ActualVaughanRowsComponentwiseChosenSquareLedgerSource κ) : ActualVaughanRowsChosenSquareLedgerSource κ

Adding the two analytic ledgers and the internally paid exact small ledger yields the canonical chosen total source.

theorem AnalyticNumberTheory.LargeSieve.actualVaughanRowsChosenSquareLedgerSource_of_legacy {κ : ℕ} (hrows : ActualVaughanRowsSquareLedgerSource κ) : ActualVaughanRowsChosenSquareLedgerSource κ

Compatibility adapter: the old uniformly quantified square source is strictly stronger than the canonical chosen-cutoff source.

theorem AnalyticNumberTheory.LargeSieve.highConductorSet_eq_interval (N Q C : ℕ) (hR : 1 ≤ logConductorThreshold N C) : highConductorSet N Q C = Finset.Icc (logConductorThreshold N C + 1) Q

theorem AnalyticNumberTheory.LargeSieve.highConductorVaughanHybrid_sq_le_actualRowsLedger (N Q C u v : ℕ) (hRpos : 1 ≤ logConductorThreshold N C) : (highConductorVaughanTypeIMean N Q C u v + highConductorVaughanTypeIIMean N Q C u v + highConductorVaughanSmallMean N Q C v) ^ 2 ≤ 3 * highConductorHarmonicFactor Q (logConductorThreshold N C) * actualVaughanRowsSquareLedger N Q C u v

The actual high Vaughan hybrid is extracted from the source-specific square ledger by weighted conductor Cauchy. This is the only passage from squares to an unsquared mean.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridChosenSource_of_actualRows {κ : ℕ} (hrows : ActualVaughanRowsChosenSquareLedgerSource κ) : StandardBVHighTypeITypeIIHybridChosenSource

A chosen-cutoff square-ledger theorem for the actual Vaughan rows, with one fixed polylogarithmic reserve κ, inhabits the canonical chosen high source.

theorem AnalyticNumberTheory.LargeSieve.standardBVHighTypeITypeIIHybridMovingSource_of_actualRowsSquareLedger {κ : ℕ} (hrows : ActualVaughanRowsSquareLedgerSource κ) : StandardBVHighTypeITypeIIHybridMovingSource

Legacy compatibility endpoint. New production code should use standardBVHighTypeITypeIIHybridChosenSource_of_actualRows; this wrapper keeps the old all-B,C API callable without making it canonical.