prime_between
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not derive the existence of N₀ from Recognition Science axioms.
- Does not bound how large N₀ must be in terms of ε.
- Does not extend the statement to complex numbers or other rings.
- Does not connect the gap property to the J-function or eight-tick octave.
formal statement (Lean)
97theorem prime_between {ε : ℝ} (hε : 0 < ε)
98 (hPrimeBetween :
99 ∃ N₀ : ℕ, ∀ x : ℝ, N₀ ≤ x → ∃ p : ℕ, Nat.Prime p ∧ x < p ∧ (p : ℝ) ≤ x * (1 + ε)) :
100 ∃ N₀ : ℕ, ∀ x : ℝ, N₀ ≤ x → ∃ p : ℕ, Nat.Prime p ∧ x < p ∧ (p : ℝ) ≤ x * (1 + ε)
101 := hPrimeBetween
proof body
Term-mode proof.
102
103/-- **TECHNICAL SCAFFOLD**: Prime counting function asymptotic (π(x) ~ x / log x). -/