Repository navigation
Build a Prime Distribution packet family from first principles to the research frontier #12
Description
Summary
Create a dedicated NumberTheory/PrimeDistribution packet family that consolidates the reusable analytic-number-theory infrastructure emerging from current proof-search campaigns.
This should extend the taxonomy and authoring architecture in #11. Preserve the existing invariant that a MathCorpus packet is an atomic JSON concept record, not a directory. Category directories organize packets, while paired Lean modules live under the matching lean/MathCorpus/... tree.
Motivation
Recent campaigns have repeatedly needed the same mathematical stack:
- prime counting;
- Chebyshev theta and psi;
- Mertens identities and explicit bounds;
- reciprocal-prime sums;
- harmonic and logarithmic asymptotics;
- Selberg and Brun sieve machinery;
- CRT and multiplicative-function infrastructure;
- explicit prime-distribution error bounds;
- consequences conditional on the Riemann hypothesis.
These should become reusable corpus knowledge rather than remain embedded in individual Erdős campaigns.
Proposed packet family
NumberTheory/PrimeDistribution/
PrimeCounting
ChebyshevTheta
ChebyshevPsi
Mertens
PrimeReciprocalSums
HarmonicAsymptotics
SelbergSieve
BrunSieve
LargeSieve
BombieriVinogradov
ExplicitBounds
RHConsequences
Each concept should be represented by one or more atomic packets with paired Lean modules, dependency edges, provenance, trust status, theorem statements, proof evidence, failed approaches, and frontier gaps.
Initial source artifacts to ingest
From Mnehmos/llm-driven-proof-search, identify and ingest reusable verified artifacts produced by the Erdős 647 campaign, including:
- real-valued Chebyshev theta lower-bound bridge;
- exact Mertens identity;
- explicit Mertens error-integral bounds;
- quantitative reciprocal-prime lower bound;
- Selberg diagonalization and optimal-weight work;
- CRT residue-counting lemmas;
- squarefree divisibility lemmas;
- harmonic block asymptotics;
- logarithmic endpoint limits;
- generic Riemann-sum infrastructure as it lands.
Campaign-specific wrappers should remain campaign-specific. General mathematical lemmas should be promoted into neutral packet and Lean namespaces.
Deliverables
- Prime Distribution dependency map from elementary prerequisites to frontier topics
- Mathlib availability and gap map for every proposed concept
- Initial packet set for existing verified artifacts
- Paired Lean modules under
lean/MathCorpus/NumberTheory/PrimeDistribution/... - Provenance links back to source campaigns, papers, books, and theorem versions
- Coverage dashboard showing verified, partially formalized, literature-only, and missing concepts
- JSONL and Parquet export eligibility for verified packets
- Benchmark set spanning pedagogy, formal proof, explicit estimates, and frontier applications
Success criterion
A future proof campaign should be able to retrieve a verified Prime Distribution concept or theorem by type, dependency, semantic meaning, provenance, and trust level without reconstructing the result from an unrelated campaign transcript.
Activity
feat(mcp): Prime Distribution promotion machinery — source map + clas…
fix(review): reuse sibling packets in capstone, fresh manifests, real…