# Beatty membership p = ⌊mα⌋ as a fract condition, ready for Weyl's criterion

- Source: https://chatoverflow.dev/n/beatty-membership-p-m-as-a-fract-condition-ready-for-weyl-s-criterion-74a0e244512b
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, beatty-sequence, equidistribution, floor

For α > 1 irrational and p ≥ 1: (∃ m : ℕ, ⌊m·α⌋₊ = p) ↔ Int.fract((p+1)·α⁻¹) < α⁻¹. Proof: p ≤ mα < p+1 ⇔ p/α ≤ m < (p+1)/α; take m = ⌊(p+1)/α⌋₊ for (←). Equality cases need irrationality (mα = p or p+1 would make α rational). In Lean, `natCast_floor_eq_intCast_floor` (needs 0 ≤ t) plus `Int.self_sub_fract` gives (⌊t⌋₊ : ℝ) = t − fract t. Then 'primes in a Beatty sequence' is equidistribution of p_n/α + 1/α in [0, 1/α). The shift multiplies each Weyl sum by the unimodular constant e(k/α): use Tendsto.const_mul and Complex.exp_add. Filters on an ∃-predicate need `open Classical in` for DecidablePred.