Prime windows below a square root

This finite window is independent of the application that chooses a prime from it. Membership has both real-endpoint and integer-square characterizations, including the closed lower and open upper endpoints. Counting reuses the general prime-window estimates.

Main definitions

• Nat.sqrtPrimeWindow: the primes in [sqrt D / 2, sqrt D).

Main results

• Real.four_le_sqrt_natCast: the shared endpoint bound for natural parameters at least 16.
• Nat.mem_sqrtPrimeWindow, Nat.mem_sqrtPrimeWindow_iff_sq: membership tests.
• Nat.sqrtPrimeWindow_eq_filter: an integer-only enumeration.
• Nat.card_sqrtPrimeWindow_lt_sqrt: the upper cardinality bound.
• Nat.exists_pos_mul_sqrt_div_log_le_card_sqrtPrimeWindow: a uniform lower bound.

References

Adapted from the prime-window definitions and estimates in Anthropic's pinned hashing source.

theorem Real.four_le_sqrt_natCast {D : ℕ} (hD : 16 ≤ D) : 4 ≤ √↑D

The real square root of a natural window parameter at least 16 is at least four.

noncomputable def Nat.sqrtPrimeWindow (D : ℕ) : Finset ℕ

Prime numbers in the half-open real interval [sqrt D / 2, sqrt D).

theorem Nat.mem_sqrtPrimeWindow {D p : ℕ} : p ∈ D.sqrtPrimeWindow ↔ Prime p ∧ √↑D / 2 ≤ ↑p ∧ ↑p < √↑D

Window membership is equivalent to primality and the two real endpoint inequalities. The finite enumeration bound in sqrtPrimeWindow excludes no member of the interval.

theorem Nat.mem_sqrtPrimeWindow_iff_sq {D p : ℕ} : p ∈ D.sqrtPrimeWindow ↔ Prime p ∧ D ≤ 4 * p ^ 2 ∧ p ^ 2 < D

Characterize window membership using primality and integer-square inequalities, including the closed lower and open upper endpoints.

theorem Nat.sqrtPrimeWindow_eq_filter (D : ℕ) : D.sqrtPrimeWindow = {p ∈ Finset.range D | Prime p ∧ D ≤ 4 * p ^ 2 ∧ p ^ 2 < D}

Enumerate the real prime window using a decidable filter of the integers below D.

theorem Nat.card_sqrtPrimeWindow_lt_sqrt (D : ℕ) (hD : 16 ≤ D) : ↑D.sqrtPrimeWindow.card < √↑D

For D ≥ 16, the number of primes in sqrtPrimeWindow D is strictly less than sqrt D.

theorem Nat.exists_pos_mul_sqrt_div_log_le_card_sqrtPrimeWindow : ∃ (c : ℝ), 0 < c ∧ ∀ (D : ℕ), 16 ≤ D → c * (√↑D / Real.log ↑D) ≤ ↑D.sqrtPrimeWindow.card

There is a universal positive c such that every window with D ≥ 16 contains at least c * sqrt D / log D primes. The proof uses the all-window counting form of Bertrand’s postulate from PrimeWindow, with no prime-number-theorem assumption.