primesBetween
plain-language theorem explainer
The definition counts the number of prime integers lying in the real interval from a to b. Researchers porting the Brun-Titchmarsh theorem into Recognition Science cite it as the basic counting object for interval prime densities. It is realized by taking the cardinality of the Finset of integers from the ceiling of a to the floor of b that satisfy the prime predicate.
Claim. $π(a,b) := |{p ∈ ℕ | ⌈a⌉ ≤ p ≤ ⌊b⌋ and p prime}|$
background
The module imports the Primes set from EulerInstantiation, defined as the subset of natural numbers satisfying Nat.Prime, and uses the local alias Prime for the same predicate. This counting function serves as the foundation for explicit prime bounds in the Brun-Titchmarsh port. Upstream results supply the prime predicate without additional structure. Conventions follow standard analytic number theory, with a and b real numbers to allow flexible interval endpoints.
proof idea
The definition is a direct one-line construction: it forms the integer interval with Finset.Icc, applies the filter for primes, and extracts the cardinality.
why it matters
It anchors the Brun-Titchmarsh port by providing the interval prime count used in monotonicity and normalization lemmas. These feed into bounds that align with Recognition Science constants such as the phi-ladder in mass formulas. The definition closes the gap between classical prime counting and the framework's number-theoretic scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.