primesBetween_one
plain-language theorem explainer
primesBetween 1 n counts the primes up to n and equals the standard prime counting function π(n). Number theorists porting analytic bounds into Recognition Science cite this to align interval counts with classical notation. The proof is a term-mode verification that unfolds the definition and equates the two filtered sets by bidirectional membership checks on the integer intervals.
Claim. For any natural number $n$, the number of primes in the closed interval $[1,n]$ equals the cardinality of the set of primes $p$ satisfying $p < n+1$.
background
primesBetween a b is defined as the cardinality of the primes in the integer interval from ceil(a) to floor(b). This theorem specializes the definition at a=1 and b=n (with n natural) to recover the usual π(n). The module NumberTheory.Port.BrunTitchmarsh imports Mathlib and the basic Prime predicate to support ported results on prime distributions. Upstream structures supply the surrounding Recognition Science setting: J-cost convexity from PhiForcingDerived, 8-tick local dynamics from PhysicsComplexityStructure, and the discrete φ-tier organization of physical quantities from NucleosynthesisTiers.
proof idea
The term proof unfolds primesBetween, simplifies ceil(1) and floor of a cast, then applies congr 1 followed by ext on the filtered sets. Membership is shown in both directions: one side uses lt_succ_of_le on the upper bound, the other uses one_le together with lt_succ_iff on the lower bound.
why it matters
The equivalence supplies the base case for the Brun-Titchmarsh port, letting later declarations such as card_range_filter_prime_isBigO and prime_counting_explicit_bound operate with standard π(n) notation. It sits inside the NumberTheory layer that feeds prime-counting estimates into the broader forcing chain and complexity structures, though it touches none of the T0-T8 landmarks directly. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.