---
id: F-011
title: Uniform divisibility count in consecutive intervals
tier: lean
polarity: positive
depends_on: []
supersedes: []
verifier: export PATH="$HOME/.elan/bin:$PATH"; diff -u verified_math/F-011_interval-divisibility-count/lean/Research/IntervalDivisors.lean workspace/experiments/experiment_2_elementary_upper_bound/lean/Research/IntervalDivisors.lean && (cd workspace/experiments/experiment_2_elementary_upper_bound/lean && lake build)
date: 2026-07-11
---

## Statement

For positive `p`, every interval of `n` consecutive natural numbers contains at
most `⌊n/p⌋+1` multiples of `p`:

```lean
theorem card_filter_dvd_Ico_le (p k n : ℕ) (hp : p ≠ 0) :
  #{x ∈ Finset.Ico k (k + n) | p ∣ x} ≤ n / p + 1
```

The artifact also proves that every half-open interval of length `p` contains
exactly one multiple of `p`.

## Proof / verification

Divisibility by `p` is periodic with period `p`.  Split the interval into
`⌊n/p⌋` complete periods and one remainder; each complete period contributes
exactly one multiple and the remainder contributes at most one.  The induction
and all endpoint arithmetic are checked by Lean without `sorry`, `admit`, or
axioms.
