English
For natural numbers n and k, k ≡ k/2^n + k mod (2^n − 1).
Русский
Для натуральных чисел n и k выполняется k ≡ k/2^n + k mod (2^n−1).
LaTeX
$$$k \equiv k / 2^{n} + k \bmod (2^{n} - 1)$$$
Lean4
theorem modEq_mersenne (n k : ℕ) : k ≡ k / 2 ^ n + k % 2 ^ n [MOD 2 ^ n - 1] :=
-- See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/help.20finding.20a.20lemma/near/177698446
calc
k = 2 ^ n * (k / 2 ^ n) + k % 2 ^ n := (Nat.div_add_mod k (2 ^ n)).symm
_ ≡ 1 * (k / 2 ^ n) + k % 2 ^ n [MOD 2 ^ n - 1] :=
(((Nat.modEq_sub <| Nat.succ_le_of_lt <| pow_pos zero_lt_two _).mul_right _).add_right _)
_ = k / 2 ^ n + k % 2 ^ n := by
rw [one_mul]
-- It's hard to know what the limiting factor for large Mersenne primes would be.
-- In the purely computational world, I think it's the squaring operation in `s`.
