feat(ErdosProblems/418): state the Odd Noncototient Conjecture

FormalConjectures/ErdosProblems/418.lean

@@ -21,6 +21,7 @@ import FormalConjectures.Util.ProblemImports
 
 *References:*
 - [erdosproblems.com/418](https://www.erdosproblems.com/418)
+- [Wikipedia: Noncototient](https://en.wikipedia.org/wiki/Noncototient)
 - [BaLu05] Banks, William D. and Luca, Florian, Nonaliquots and {R}obbins numbers. Colloq. Math.
   (2005), 27--32.
 - [BrSc95] Browkin, J. and Schinzel, A., On integers not of the form {$n-\phi(n)$}. Colloq. Math.
@@ -83,6 +84,27 @@ theorem erdos_418.variants.conditional
     linear_combination hm
   rwa [Nat.coprime_primes hp hq]
 
+/--
+The **Odd Noncototient Conjecture**: every non-cototient is even. Equivalently, every odd natural
+number is of the form $n - \phi(n)$ for some $n$.
+
+This is the unconditional form of `erdos_418.variants.conditional`, which derives the odd case from a
+strengthening of the Goldbach conjecture. See [Wikipedia: Noncototient].
+-/
+@[category research open, AMS 11]
+theorem erdos_418.variants.odd_noncototient :
+    { (n - n.totient : ℕ) | n }ᶜ ⊆ { k | Even k } := by
+  sorry
+
+/--
+A sanity check for the definition: $7$ is a cototient, since $7 = 15 - \phi(15)$ and $\phi(15) = 8$.
+In particular $7$ is not a non-cototient.
+-/
+@[category test, AMS 11]
+theorem erdos_418.variants.seven_mem_cototient :
+    7 ∈ { (n - n.totient : ℕ) | n } :=
+  ⟨15, by decide⟩
+
 /--
 Erdős [Er73b] has shown that a positive density set of natural numbers cannot be written as
 $\sigma(n)-n$ (numbers not of this form are called nonaliquot, or sometimes untouchable).