diff --git a/backlog/gself-pow-three-add-pow-one.md b/backlog/gself-pow-three-add-pow-one.md
new file mode 100644
index 000000000..137059955
--- /dev/null
+++ b/backlog/gself-pow-three-add-pow-one.md
@@ -0,0 +1,7 @@
+# gself-pow-three-add-pow-one
+
+n to the 1 divides n to the 3 plus n to the 1.
+
+- **Source:** self-seeded polynomial-divisibility identity family.
+- **Reference:** n to the 1 divides n to the 3 plus n to the 1. Provable by exhibiting the cofactor and `ring`.
+- **Difficulty:** 1
diff --git a/goals/gself-pow-three-add-pow-one.aisp b/goals/gself-pow-three-add-pow-one.aisp
new file mode 100644
index 000000000..56f49f6b6
--- /dev/null
+++ b/goals/gself-pow-three-add-pow-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gself-pow-three-add-pow-one@2026-06-17
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gself-pow-three-add-pow-one
+  phase≜prove
+  status≜proved
+  difficulty≜1
+}
+⟦Σ:Source⟧{
+  src≜backlog/gself-pow-three-add-pow-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gself-pow-three-add-pow-one.lean
+  sha≜d942597fe63e61ed2431392f32de229816b74d0520ce1fb224327e93687b9db6
+  aff≜0
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gself-pow-three-add-pow-one.lean b/goals/gself-pow-three-add-pow-one.lean
new file mode 100644
index 000000000..596dcb97c
--- /dev/null
+++ b/goals/gself-pow-three-add-pow-one.lean
@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem gself_pow_three_add_pow_one (n : ℤ) : (n) ∣ (n^3 + n) := by
+  sorry
diff --git a/library/Unsorry/GselfPowThreeAddPowOne.lean b/library/Unsorry/GselfPowThreeAddPowOne.lean
new file mode 100644
index 000000000..7af0b8340
--- /dev/null
+++ b/library/Unsorry/GselfPowThreeAddPowOne.lean
@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem gself_pow_three_add_pow_one (n : ℤ) : (n) ∣ (n^3 + n) := by
+  exact ⟨n^2 + 1, by ring⟩
diff --git a/library/index/d942597fe63e61ed2431392f32de229816b74d0520ce1fb224327e93687b9db6.aisp b/library/index/d942597fe63e61ed2431392f32de229816b74d0520ce1fb224327e93687b9db6.aisp
new file mode 100644
index 000000000..7b3a746fb
--- /dev/null
+++ b/library/index/d942597fe63e61ed2431392f32de229816b74d0520ce1fb224327e93687b9db6.aisp
@@ -0,0 +1,8 @@
+𝔸5.1.lemma.d942597fe63e@2026-06-17
+γ≔unsorry.lemma.index
+⟦Ω:Lemma⟧{sha≜d942597fe63e61ed2431392f32de229816b74d0520ce1fb224327e93687b9db6; goal≜gself-pow-three-add-pow-one; name≜gself_pow_three_add_pow_one}
+⟦Σ:Source⟧{src≜goals/gself-pow-three-add-pow-one.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-three-add-pow-one.mac-158f.20260617t182159514538z-b3016b04.aisp b/proof-runs/gself-pow-three-add-pow-one.mac-158f.20260617t182159514538z-b3016b04.aisp
new file mode 100644
index 000000000..0b683154f
--- /dev/null
+++ b/proof-runs/gself-pow-three-add-pow-one.mac-158f.20260617t182159514538z-b3016b04.aisp
@@ -0,0 +1,8 @@
+𝔸5.1.run.gself-pow-three-add-pow-one.mac-158f.20260617t182159514538z-b3016b04@2026-06-17
+γ≔unsorry.proof.run
+⟦Ω:Run⟧{id≜20260617t182159514538z-b3016b04; goal≜gself-pow-three-add-pow-one; agent≜mac-158f; outcome≜proved}
+⟦Π:Provenance⟧{solver≜ohdearquant; provider≜claude; model≜template-ring-cofactor}
+⟦Γ:Goal⟧{goal≜gself-pow-three-add-pow-one}
+⟦Λ:Metrics⟧{attempts≜1; solve_s≜0; ended≜2026-06-17T18:21:59Z}
+⟦Σ:Artifact⟧{sha≜d942597fe63e61ed2431392f32de229816b74d0520ce1fb224327e93687b9db6}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩