IndisputableMonolith.NumberTheory.Port.BrunTitchmarsh
BrunTitchmarsh module supplies explicit upper bounds for the number of primes in the interval [a, b]. Number theorists inside the Recognition monolith cite these estimates when controlling prime densities and gaps. The module reuses Mathlib together with the axiom-free Primes.Basic layer to deliver interval-counting functions and their asymptotic controls.
claimLet $N(a,b)$ denote the number of primes $p$ with $a < p < b$. The module supplies explicit upper bounds of Brun-Titchmarsh type on $N(a,b)$ for real $a < b$.
background
The upstream Primes.Basic module supplies axiom-free sanity theorems on Nat.Prime that reuse Mathlib while keeping the namespace sorry-free. This BrunTitchmarsh module extends the algebraic layer into analytic number theory by defining interval prime counts. The local setting follows the design goal of growing upward only after the algebraic layer is stable.
proof idea
This is a definition module, no proofs. It organizes declarations for primesBetween and associated big-O estimates that build directly on the imported Primes.Basic results.
why it matters in Recognition Science
The module feeds the parent NumberTheory.Port namespace that integrates these bounds into the Recognition framework. It fills the analytic number theory layer needed for prime-related constants and distributions, following the upstream design goal of confirming algebraic stability first.
scope and limits
- Does not derive the Brun-Titchmarsh inequality from first principles.
- Does not apply the bounds to specific physical models or constants.
- Does not extend the estimates beyond real intervals.