prime_between
plain-language theorem explainer
The prime_between declaration asserts that for any ε > 0 the interval (x, x(1+ε)] contains a prime for all sufficiently large real x. It is invoked inside derivations of the prime counting asymptotic in the NumberTheory.Port.PNT module. The proof is a direct term that forwards the supplied hypothesis without alteration.
Claim. For every real number ε > 0 there exists a natural number N₀ such that for all real x ≥ N₀ there exists a prime p satisfying x < p ≤ x(1 + ε).
background
The NumberTheory.Port.PNT module assembles technical interfaces for the prime number theorem. Prime is the transparent alias for the standard Nat.Prime predicate. The declaration sits between the basic prime definition and the asymptotic statement for the prime counting function. No deeper Recognition Science objects such as the J-cost or phi-ladder appear in this file.
proof idea
The proof is a one-line term wrapper that returns the hypothesis hPrimeBetween verbatim.
why it matters
The result supplies the prime-gap hypothesis to prime_counting_asymptotic_pnt, which itself scaffolds the statement that the prime counting function is asymptotic to x / log x. It therefore forms part of the number-theoretic scaffolding required before Recognition Science mass formulas or forcing-chain arguments can invoke prime distributions. The underlying existence of N₀ remains an open assumption within the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.