Kernel-prove the larger unitary-perfect examples

[DomTheDeveloper]

Result

Kernel-proves two nontrivial unitary-perfect numbers:

• 87360 = 2^6 · 3 · 5 · 7 · 13;
• 146361946186458562560000 = 2^18 · 3 · 5^4 · 7 · 11 · 13 · 19 · 37 · 79 · 109 · 157 · 313.

The proof establishes the prime-power formula and multiplicativity of the sum of unitary divisors, then reduces both examples to exact arithmetic. It does not enumerate every integer below either number.

Green verification

Focused audit run 30211997936 passed every gate:

• source scan rejecting sorry, admit, native_decide, unsafe/custom axioms, and compiler-trust shortcuts;
• exact registered Lake-module build;
• exact theorem axiom audit.

Both exported theorems depend only on:

[propext, Classical.choice, Quot.sound]

No sorryAx or compiler-trust dependency appears.

Status

The proof module is green. The canonical catalog declarations still need focused wrapper replacement and current-main validation before this can enter _PRs/ready/.

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