feat(GreensOpenProblems/64): formalize Ω(p-2) odd infinitude question

[Sanexxxx777]

Formalizes Green's open problem 64:

Do there exist infinitely many primes $p$ for which $p - 2$ has an odd number of prime factors, counted with multiplicity?

Statement

@[category research open, AMS 11]
theorem green_64 :
    answer(sorry) ↔ {p : ℕ | p.Prime ∧ Odd (Ω (p - 2))}.Infinite

where Ω is ArithmeticFunction.cardFactors (number of prime factors with multiplicity). This mirrors the existing twin-prime style infinitude statements in the repo.

Test witnesses

Three decidable category test lemmas keep the definition honest:

• green_64_mem_five / green_64_mem_seven: 5 and 7 qualify (for these, p - 2 is itself prime, so Ω (p - 2) = 1 is odd).
• green_64_not_mem_eleven: 11 does not qualify, since 11 - 2 = 9 = 3 ^ 2 gives Ω 9 = 2, which is even — showing the condition is non-trivial.

Verification

• lake build --wfail 'FormalConjectures.GreensOpenProblems.«64»' passes clean (linters as errors).
• #print axioms on all three test lemmas: [propext, Classical.choice, Quot.sound] only (no sorryAx).

Closes #1684.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.