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

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.