From 646053eaf6be94a0949cd00f663969d81c32b57b Mon Sep 17 00:00:00 2001
From: OceanLi <122793010+ohdearquant@users.noreply.github.com>
Date: Wed, 17 Jun 2026 14:25:04 -0400
Subject: [PATCH] prove(gself-pow-six-add-pow-five): gself_pow_six_add_pow_five
 by mac-158f

---
 backlog/gself-pow-six-add-pow-five.md         |  7 +++++++
 goals/gself-pow-six-add-pow-five.aisp         | 20 +++++++++++++++++++
 goals/gself-pow-six-add-pow-five.lean         |  4 ++++
 library/Unsorry/GselfPowSixAddPowFive.lean    |  4 ++++
 ...e68efe2a707be003b411ce53fc58c30f5b6c1.aisp |  8 ++++++++
 ...-158f.20260617t182503672930z-3256d501.aisp |  8 ++++++++
 6 files changed, 51 insertions(+)
 create mode 100644 backlog/gself-pow-six-add-pow-five.md
 create mode 100644 goals/gself-pow-six-add-pow-five.aisp
 create mode 100644 goals/gself-pow-six-add-pow-five.lean
 create mode 100644 library/Unsorry/GselfPowSixAddPowFive.lean
 create mode 100644 library/index/b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1.aisp
 create mode 100644 proof-runs/gself-pow-six-add-pow-five.mac-158f.20260617t182503672930z-3256d501.aisp

diff --git a/backlog/gself-pow-six-add-pow-five.md b/backlog/gself-pow-six-add-pow-five.md
new file mode 100644
index 000000000..5f2cda5fd
--- /dev/null
+++ b/backlog/gself-pow-six-add-pow-five.md
@@ -0,0 +1,7 @@
+# gself-pow-six-add-pow-five
+
+n to the 1 divides n to the 6 plus n to the 5.
+
+- **Source:** self-seeded polynomial-divisibility identity family.
+- **Reference:** n to the 1 divides n to the 6 plus n to the 5. Provable by exhibiting the cofactor and `ring`.
+- **Difficulty:** 1
diff --git a/goals/gself-pow-six-add-pow-five.aisp b/goals/gself-pow-six-add-pow-five.aisp
new file mode 100644
index 000000000..f91a72d61
--- /dev/null
+++ b/goals/gself-pow-six-add-pow-five.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gself-pow-six-add-pow-five@2026-06-17
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gself-pow-six-add-pow-five
+  phase≜prove
+  status≜proved
+  difficulty≜1
+}
+⟦Σ:Source⟧{
+  src≜backlog/gself-pow-six-add-pow-five.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gself-pow-six-add-pow-five.lean
+  sha≜b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1
+  aff≜0
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gself-pow-six-add-pow-five.lean b/goals/gself-pow-six-add-pow-five.lean
new file mode 100644
index 000000000..9cad8ea1c
--- /dev/null
+++ b/goals/gself-pow-six-add-pow-five.lean
@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem gself_pow_six_add_pow_five (n : ℤ) : (n) ∣ (n^6 + n^5) := by
+  sorry
diff --git a/library/Unsorry/GselfPowSixAddPowFive.lean b/library/Unsorry/GselfPowSixAddPowFive.lean
new file mode 100644
index 000000000..c82d34554
--- /dev/null
+++ b/library/Unsorry/GselfPowSixAddPowFive.lean
@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem gself_pow_six_add_pow_five (n : ℤ) : (n) ∣ (n^6 + n^5) := by
+  exact ⟨n^5 + n^4, by ring⟩
diff --git a/library/index/b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1.aisp b/library/index/b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1.aisp
new file mode 100644
index 000000000..286220cbc
--- /dev/null
+++ b/library/index/b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1.aisp
@@ -0,0 +1,8 @@
+𝔸5.1.lemma.b9725c3d8a3c@2026-06-17
+γ≔unsorry.lemma.index
+⟦Ω:Lemma⟧{sha≜b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1; goal≜gself-pow-six-add-pow-five; name≜gself_pow_six_add_pow_five}
+⟦Σ:Source⟧{src≜goals/gself-pow-six-add-pow-five.lean}
+⟦Γ:Tags⟧{tags≜⟨⟩}
+⟦Λ:Meta⟧{use≜0; aff≜0}
+⟦Π:Provenance⟧{solver≜ohdearquant; agent≜mac-158f; provider≜claude; model≜template-ring-cofactor; attempts≜1}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/proof-runs/gself-pow-six-add-pow-five.mac-158f.20260617t182503672930z-3256d501.aisp b/proof-runs/gself-pow-six-add-pow-five.mac-158f.20260617t182503672930z-3256d501.aisp
new file mode 100644
index 000000000..0ae990d97
--- /dev/null
+++ b/proof-runs/gself-pow-six-add-pow-five.mac-158f.20260617t182503672930z-3256d501.aisp
@@ -0,0 +1,8 @@
+𝔸5.1.run.gself-pow-six-add-pow-five.mac-158f.20260617t182503672930z-3256d501@2026-06-17
+γ≔unsorry.proof.run
+⟦Ω:Run⟧{id≜20260617t182503672930z-3256d501; goal≜gself-pow-six-add-pow-five; agent≜mac-158f; outcome≜proved}
+⟦Π:Provenance⟧{solver≜ohdearquant; provider≜claude; model≜template-ring-cofactor}
+⟦Γ:Goal⟧{goal≜gself-pow-six-add-pow-five}
+⟦Λ:Metrics⟧{attempts≜1; solve_s≜0; ended≜2026-06-17T18:25:03Z}
+⟦Σ:Artifact⟧{sha≜b9725c3d8a3cc92f34a58bac9aae68efe2a707be003b411ce53fc58c30f5b6c1}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩