/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilMultiplicative order of 2 mod $2n+1$
The multiplicative order of 2 modulo $2n+1$. In other words, the least $m > 0$ such that $2n+1$ divides $2^m - 1$.
References:
namespace OeisA2326The multiplicative order of 2 modulo $2n+1$.
noncomputable def a (n : ℕ) : ℕ :=
orderOf (2 : ZMod (2 * n + 1))
Value of the sequence a at 0.
@[category test, AMS 11]
theorem a_0 : a 0 = 1 := ⊢ a 0 = 1
⊢ orderOf 2 = 1
All goals completed! 🐙
Value of the sequence a at 1.
⊢ 2 ^ 2 = 1 ∧ ∀ m < 2, 0 < m → 2 ^ m ≠ 1
exact ⟨⊢ 2 ^ 2 = 1 All goals completed! 🐙, fun m hm1 hm2 ↦ m:ℕhm1:m < 2hm2:0 < m⊢ 2 ^ m ≠ 1 m:ℕhm1:1 < 2hm2:0 < 1⊢ 2 ^ 1 ≠ 1; All goals completed! 🐙⟩
Value of the sequence a at 2.
⊢ 2 ^ 4 = 1 ∧ ∀ m < 4, 0 < m → 2 ^ m ≠ 1
exact ⟨⊢ 2 ^ 4 = 1 All goals completed! 🐙, fun m hm1 hm2 ↦ m:ℕhm1:m < 4hm2:0 < m⊢ 2 ^ m ≠ 1 m:ℕhm1:1 < 4hm2:0 < 1⊢ 2 ^ 1 ≠ 1m:ℕhm1:2 < 4hm2:0 < 2⊢ 2 ^ 2 ≠ 1m:ℕhm1:3 < 4hm2:0 < 3⊢ 2 ^ 3 ≠ 1 m:ℕhm1:1 < 4hm2:0 < 1⊢ 2 ^ 1 ≠ 1m:ℕhm1:2 < 4hm2:0 < 2⊢ 2 ^ 2 ≠ 1m:ℕhm1:3 < 4hm2:0 < 3⊢ 2 ^ 3 ≠ 1 All goals completed! 🐙⟩
Value of the sequence a at 3.
⊢ 2 ^ 3 = 1 ∧ ∀ m < 3, 0 < m → 2 ^ m ≠ 1
exact ⟨⊢ 2 ^ 3 = 1 All goals completed! 🐙, fun m hm1 hm2 ↦ m:ℕhm1:m < 3hm2:0 < m⊢ 2 ^ m ≠ 1 m:ℕhm1:1 < 3hm2:0 < 1⊢ 2 ^ 1 ≠ 1m:ℕhm1:2 < 3hm2:0 < 2⊢ 2 ^ 2 ≠ 1 m:ℕhm1:1 < 3hm2:0 < 1⊢ 2 ^ 1 ≠ 1m:ℕhm1:2 < 3hm2:0 < 2⊢ 2 ^ 2 ≠ 1 All goals completed! 🐙⟩
Value of the sequence a at 4.
⊢ 2 ^ 6 = 1 ∧ ∀ m < 6, 0 < m → 2 ^ m ≠ 1
exact ⟨⊢ 2 ^ 6 = 1 All goals completed! 🐙, fun m hm1 hm2 ↦ m:ℕhm1:m < 6hm2:0 < m⊢ 2 ^ m ≠ 1 m:ℕhm1:1 < 6hm2:0 < 1⊢ 2 ^ 1 ≠ 1m:ℕhm1:2 < 6hm2:0 < 2⊢ 2 ^ 2 ≠ 1m:ℕhm1:3 < 6hm2:0 < 3⊢ 2 ^ 3 ≠ 1m:ℕhm1:4 < 6hm2:0 < 4⊢ 2 ^ 4 ≠ 1m:ℕhm1:5 < 6hm2:0 < 5⊢ 2 ^ 5 ≠ 1 m:ℕhm1:1 < 6hm2:0 < 1⊢ 2 ^ 1 ≠ 1m:ℕhm1:2 < 6hm2:0 < 2⊢ 2 ^ 2 ≠ 1m:ℕhm1:3 < 6hm2:0 < 3⊢ 2 ^ 3 ≠ 1m:ℕhm1:4 < 6hm2:0 < 4⊢ 2 ^ 4 ≠ 1m:ℕhm1:5 < 6hm2:0 < 5⊢ 2 ^ 5 ≠ 1 All goals completed! 🐙⟩If $p$ is an odd prime then $a((p^3-1)/2) = p \cdot a((p^2-1)/2)$. Because otherwise $a((p^3-1)/2) < p \cdot a((p^2-1)/2)$ iff $a((p^3-1)/2) = a((p-1)/2)$ for a prime $p$. Equivalently $p^3$ divides $2^{p-1}-1$, but no such prime $p$ is known.
Thomas Ordowski, Feb 10 2014
@[category research open, AMS 11]
theorem conjecture1 (p : ℕ) (hp : p.Prime) (hp_odd : p ≠ 2) :
a ((p ^ 3 - 1) / 2) = p * a ((p ^ 2 - 1) / 2) := p:ℕhp:Nat.Prime php_odd:p ≠ 2⊢ a ((p ^ 3 - 1) / 2) = p * a ((p ^ 2 - 1) / 2)
All goals completed! 🐙A generalization of the previous conjecture: For each $k \ge 2$, if $p$ is an odd prime then $a((p^{k+1}-1)/2) = p \cdot a((p^k-1)/2)$. Computer testing of this generalized conjecture shows that there is no counterexample for $k$ and $p$ both up to 1000.
Ahmad J. Masad, Oct 17 2020
@[category research open, AMS 11]
theorem conjecture2 (k : ℕ) (hk : 2 ≤ k) (p : ℕ) (hp : p.Prime) (hp_odd : p ≠ 2) :
a ((p ^ (k + 1) - 1) / 2) = p * a ((p ^ k - 1) / 2) := k:ℕhk:2 ≤ kp:ℕhp:Nat.Prime php_odd:p ≠ 2⊢ a ((p ^ (k + 1) - 1) / 2) = p * a ((p ^ k - 1) / 2)
All goals completed! 🐙end OeisA2326