LargeSieveLib

LargeSieveLib is a proposed Mathlib-only formalization of the additive and multiplicative large sieve, designed as the first upstream component of a future unconditional Bombieri–Vinogradov pipeline. It does not yet prove Bombieri–Vinogradov or make PrimeGapsLib unconditional.

Apache-2.0. Lean v4.28.0, Mathlib v4.28.0 (the pair validated by Aristotle cloud elaboration, 2026-08-18) (one exact stable release pair; see lean-toolchain and lakefile.toml).

Status: entirely red. Every theorem in this repository is a sorry'd statement. Nothing here is proved. This is v0.2 of the trusted contract — the audited, repaired theorem statements plus a reproducible verification harness — not a body of completed proofs.

This package targets the classical Bombieri–Vinogradov lane (single primes in arithmetic progressions, on average over moduli) — not the Hardy–Littlewood prime-pair-correlation lane. The eventual downstream consumer is Axiom Math's public PrimeGapsLib, whose BombieriVinogradov : Prop (stated Mathlib-only in their Challenge/Basic.lean) is the exact hypothesis a future bridge must discharge — verified against upstream commit 1faa7b14e82d (2026-08-18); see docs/AXIOM-COMPAT.md.

Headline targets (v0.2 constants — decision record)

• LargeSieve.additive_large_sieve: ∑_{α ∈ T} ‖S_C(α)‖² ≤ (2πN + δ⁻¹) · ∑‖a_n‖² for δ-spaced T.
• LargeSieve.multiplicative_large_sieve: ∑_{q ≤ Q} (q/φ(q)) ∑*_χ ‖∑ a_n χ(n)‖² ≤ (2πN + Q²) · ∑‖a_n‖².

Why 2πN: the audit (docs/AUDIT-2026-08-18.md, Blocker A) showed the previous (πN + 1/δ) headline did not follow from the package's own lemma graph (gallagher_sum: δ⁻¹A + 2√A√B with B ≤ π²N²A gives δ⁻¹A + 2πNA). v0.2 adopts the audit's fast conservative repair: keep the arbitrary-point gallagher_sum shape and state the 2πN headline, which is entirely sufficient for downstream Bombieri–Vinogradov work.

v0.3 target: the audit's preferred repair — centered-interval averaging (centered_sobolev_pointwise / gallagher_sum_centered), which halves the derivative contribution and recovers the classical πN + δ⁻¹ constant.

Layout

Path	Role
Statement/	Trusted challenge library: shared definitions + the two headline theorem statements (2 intentional contract placeholders, never proved here)
LargeSieveLib/	Untrusted solution library: analytic, Farey, and character tracks + solution-side headline declarations (all red)
comparator.json	Lean Comparator config, current PrimeGapsLib schema (challenge_module/solution_module/theorem_names/permitted_axioms/enable_nanoda) — field-for-field confirmed against AxiomMath/PrimeGapsLib@1faa7b14e82d Comparator/comparator.json; run with lake env comparator comparator.json (Linux)
docs/AXIOM-COMPAT.md	Cross-check of this repo against the real public AxiomMath/PrimeGapsLib (BV Prop verbatim, schema, toolchain matrix, adapter plan)
scripts/gen_status.py	Status generator, 4-state model (red/amber/green/mathlib) with per-declaration evidence records
scripts/print_axioms.lean	Declaration-level axiom audit — run with lake env lean scripts/print_axioms.lean (no --run)
.github/workflows/ci.yml	build · exact placeholder count · forbidden-token scan · axiom audit · Comparator · status generation
docs/AUDIT-2026-08-18.md	The third-party audit this v0.2 implements (provenance)
docs/DEPENDENCY-GRAPH.md	v0.2 dependency graph (audit §6)
docs/ROADMAP.md	Execution sequence (audit §7)

Contract repairs applied in v0.2 (audit §2)

• Blocker A — headline constants changed to 2πN + 1/δ and 2πN + Q² (conservative repair; πN refinement deferred to v0.3).
• Blocker B — centre is integer-valued: def centre (M N : ℕ) : ℝ := ((M + (N + 1) / 2 : ℕ) : ℝ) (ℕ-division before the cast). The old real-division centre made expSumC anti-periodic for even N, falsifying Function.Periodic (expSumC a M N) 1.
• Blocker C — the false wraparound equality ‖a/q − a′/q′‖ = |aq′−a′q|/(qq′) is removed from all specs. The recorded valid argument: both numerators |aq′−a′q| ≥ 1 and qq′−|aq′−a′q| ≥ 1, so both direct and wraparound distances are ≥ 1/(qq′) ≥ 1/Q².
• Blocker D — explicit bookkeeping nodes added as sorry'd statements: reducedFraction_injective, farey_denominator_sets_pairwiseDisjoint, sum_reducedFractions_eq_sum_fareySet.

Placeholder counts (generated, enforced exactly in CI)

• 2 trusted-contract placeholders (Statement/LargeSieve.lean).
• 18 library placeholders (16 supporting lemmas + the 2 solution-side headline re-declarations).

Regenerate: python3 scripts/gen_status.py.

Provenance (future tense — nothing has been proved)

Proof bodies will be generated with Aristotle and independently re-derived with AXLE. No such run has occurred. After each closure a per-declaration evidence record will be attached (statement hash, proof hash, Lean/Mathlib revisions, build result, #print axioms output, Comparator result, independent-verifier result, human reviewer and date) — see status.json, whose evidence fields remain null until the corresponding real event.

Source recovery note: the original archive reviewed by the audit could not be recovered on the authoring machine; this tree was reconstructed from the audit's quoted declarations and repaired per its Phase 0. The Lean files have not yet been elaboration-checked (no local Mathlib build was possible at authoring time); the first lake build in CI or on the owner's machine is the statement-validation gate (ROADMAP Phase 0, step 5).

Novelty claim (measured)

"I found no public Lean/Mathlib implementation of the full additive-and-multiplicative large-sieve package in the repositories searched."

No stronger claim is made; no documented cross-system survey exists yet.

Scope fence

In scope: additive and multiplicative large sieve, Farey spacing, Gauss-sum bridge — Mathlib-only. Explicitly out of scope for v0.2: Vaughan's identity, Type I/II estimates, Siegel–Walfisz, dyadic decomposition, classical Bombieri–Vinogradov itself, and the adapter to Axiom PrimeGapsLib.