Carmichael's totient function conjecture

For every positive natural number $n$, there exists a natural number $m$ with $m ≠ n$, such that $φ(n) = φ(m)$ where $φ$ is the Euler totient function.

References:

• Wikipedia
• [F1998] Kevin Ford. The distribution of totients. https://arxiv.org/abs/1104.3264

def CarmichaelTotient.CarmichaelTotientFor (n : ℕ) : Prop

Natural number $n$ for which there exists a $m ≠ n$ with $φ(m) = φ(n)$

Equations

• CarmichaelTotient.CarmichaelTotientFor n = ∃ (m : ℕ), m ≠ n ∧ m.totient = n.totient

theorem CarmichaelTotient.carchimichealTotientFor_zero : ¬CarmichaelTotientFor 0

$n = 0 ↔ φ(n) = 0$

theorem CarmichaelTotient.carmichealTotientFor_odd {n : ℕ} (hn : Odd n) : CarmichaelTotientFor n

For every odd number $n$, $φ(2n) = φ(n)$

theorem CarmichaelTotient.charmichaelTotient ⦃n : ℕ⦄ : 0 < n → CarmichaelTotientFor n

Carmichael's totient function conjecture: For every positive natural number $n$, there exists a natural number $m$ with $m ≠ n$, such that $φ(n) = φ(m)$.

theorem CarmichaelTotient.carchimaelTotient_bound {n : ℕ} (hn : 0 < n) (hn' : n < 10 ^ 10 ^ 10) : CarmichaelTotientFor n

In Theorem 6 in [F1998], Kevin Ford proves that the smallest counterexample to Carmichael's totient function conjecture must be $≥ 10 ^ (10 ^ 10)$