Replay the A080170 gcd/prime-power equivalence proof

[DomTheDeveloper]

Green result

The complete immutable A080170 proof now compiles against the current pinned Lean and Mathlib toolchain.

It proves, for k ≥ 2,

GCDCondition k ↔ PrimePowerCondition (k + 1)

through the full binomial-gcd, exact prime-power component, and largest-prime-power-divisor development—not merely the final three-line rewrite.

Immutable provenance

• Historical commit: 0720658844d76a50d48e4baa152eef14d4462907
• Historical source blob: 4985c414321be15ed18552834b7aa7c0d9644eb7
• Audit branch head: ca28a389683ebfa9154c55019aaa0b1fd2fdd21a
• Focused run: 30213920030

The run passed source identity verification, no-hole/no-trust scanning, complete proof compilation, and exact theorem axiom inspection.

Axiom footprint:

[propext, Classical.choice, Quot.sound]

No sorryAx or compiler-trust dependency appears.

Status

Green full-proof recovery. The current admitted catalog file still needs a focused restoration/package patch before promotion to _PRs/ready/. This audit-only PR should not merge.

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