Prove the first five A317940 values

[DomTheDeveloper]

Closes the five category test placeholders in FormalConjectures/OEIS/317940.lean by unfolding the exact well-founded recurrence and kernel-normalizing the small prime-factorization/divisor calculations.

Targets:

• a_1 : a 1 = 1
• a_2 : a 2 = 1
• a_3 : a 3 = 1
• a_4 : a 4 = 7
• a_5 : a 5 = 1

Validation:

• final immutable commit: 7f19c892cc0e328736c106d270444e4bfb0e1191;
• ProofPlaygrond run 30214340477: green;
• exact Lake module FormalConjectures.OEIS.«317940»: compiled;
• target-region scan rejected sorry, admit, native_decide, unsafe, and custom axioms;
• #print axioms passed for all five theorems with no sorryAx or compiler-trust dependency.

One commit and one canonical source file. Repository-wide fork CI remains the final integration gate before any upstream promotion.

[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.