feat(ErdosProblems/418): state the Odd Noncototient Conjecture#4361
feat(ErdosProblems/418): state the Odd Noncototient Conjecture#4361Sanexxxx777 wants to merge 1 commit into
Conversation
Adds the unconditional Odd Noncototient Conjecture (every non-cototient is even, equivalently every odd number is of the form n - φ(n)) as a variant of Erdős 418, complementing the existing conditional variant that derives the odd case from a strengthening of Goldbach. Adds a sanity-check test that 7 = 15 - φ(15) is a cototient. Verified: lake --wfail build succeeds on the 418 module. Closes google-deepmind#2249.
|
👋 This is an automated welcome message. 🤖 A few friendly reminders while the review gets started:
Thanks again for helping improve Formal Conjectures. |
|
Should these changes also be added to _FormalConjectures/Wikipedia/Noncototient.lean_, just like it was done in #2276? |
|
Good question — I looked into it. It turns out #2276 was closed without being merged (the CLA was never signed), so |
2 participants
Summary
Closes #2249.
Adds the Odd Noncototient Conjecture — every non-cototient is even, equivalently every odd natural number is of the form$n - \phi(n)$ — as a variant of Erdős 418.
I stated it inside
ErdosProblems/418.leanrather than as a new file because 418 already defines the non-cototient set{ n - n.totient | n }ᶜand already containserdos_418.variants.conditional, which derives the odd case from a strengthening of Goldbach. The newerdos_418.variants.odd_noncototientis precisely the unconditional form of that conditional variant, so keeping them together (and reusing the existing definition) follows the "state a problem in one place" convention. Happy to move it toWikipedia/with a pointer if you'd prefer, since #2249 is taggedwikipedia.Changes
erdos_418.variants.odd_noncototient(category research open):{ (n - n.totient : ℕ) | n }ᶜ ⊆ { k | Even k }.erdos_418.variants.seven_mem_cototient(category test): a proven sanity check that7 = 15 - φ(15)is a cototient (⟨15, by decide⟩).Verification
lake --wfail build FormalConjectures.ErdosProblems.«418»succeeds. The onlysorrys are the research statements (as expected for benchmark statements); thetestlemma is fully proved.