prove(gself-pow-three-pow-four-add-pow-three): gself_pow_three_pow_four_add_pow_three by mac-158f

backlog/gself-pow-three-pow-four-add-pow-three.md

@@ -0,0 +1,7 @@
+# gself-pow-three-pow-four-add-pow-three
+
+n to the 3 divides n to the 4 plus n to the 3.
+
+- **Source:** self-seeded polynomial-divisibility identity family.
+- **Reference:** n to the 3 divides n to the 4 plus n to the 3. Provable by exhibiting the cofactor and `ring`.
+- **Difficulty:** 1

goals/gself-pow-three-pow-four-add-pow-three.aisp

@@ -0,0 +1,20 @@
+𝔸5.1.goal.gself-pow-three-pow-four-add-pow-three@2026-06-17
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gself-pow-three-pow-four-add-pow-three
+  phase≜prove
+  status≜proved
+  difficulty≜1
+}
+⟦Σ:Source⟧{
+  src≜backlog/gself-pow-three-pow-four-add-pow-three.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gself-pow-three-pow-four-add-pow-three.lean
+  sha≜aa6046930a688d24083bcd080c76c6d8c60d92d27ed95c01f58a2d51fd6f87ec
+  aff≜0
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩

goals/gself-pow-three-pow-four-add-pow-three.lean

@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem gself_pow_three_pow_four_add_pow_three (n : ℤ) : (n^3) ∣ (n^4 + n^3) := by
+  sorry

library/Unsorry/GselfPowThreePowFourAddPowThree.lean

@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem gself_pow_three_pow_four_add_pow_three (n : ℤ) : (n^3) ∣ (n^4 + n^3) := by
+  exact ⟨n + 1, by ring⟩

library/index/aa6046930a688d24083bcd080c76c6d8c60d92d27ed95c01f58a2d51fd6f87ec.aisp

@@ -0,0 +1,8 @@
+𝔸5.1.lemma.aa6046930a68@2026-06-17
+γ≔unsorry.lemma.index
+⟦Ω:Lemma⟧{sha≜aa6046930a688d24083bcd080c76c6d8c60d92d27ed95c01f58a2d51fd6f87ec; goal≜gself-pow-three-pow-four-add-pow-three; name≜gself_pow_three_pow_four_add_pow_three}
+⟦Σ:Source⟧{src≜goals/gself-pow-three-pow-four-add-pow-three.lean}
+⟦Γ:Tags⟧{tags≜⟨⟩}
+⟦Λ:Meta⟧{use≜0; aff≜0}
+⟦Π:Provenance⟧{solver≜ohdearquant; agent≜mac-158f; provider≜claude; model≜template-ring-cofactor; attempts≜1}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩

proof-runs/gself-pow-three-pow-four-add-pow-three.mac-158f.20260617t182814933645z-ff62eaa6.aisp

@@ -0,0 +1,8 @@
+𝔸5.1.run.gself-pow-three-pow-four-add-pow-three.mac-158f.20260617t182814933645z-ff62eaa6@2026-06-17
+γ≔unsorry.proof.run
+⟦Ω:Run⟧{id≜20260617t182814933645z-ff62eaa6; goal≜gself-pow-three-pow-four-add-pow-three; agent≜mac-158f; outcome≜proved}
+⟦Π:Provenance⟧{solver≜ohdearquant; provider≜claude; model≜template-ring-cofactor}
+⟦Γ:Goal⟧{goal≜gself-pow-three-pow-four-add-pow-three}
+⟦Λ:Metrics⟧{attempts≜1; solve_s≜0; ended≜2026-06-17T18:28:14Z}
+⟦Σ:Artifact⟧{sha≜aa6046930a688d24083bcd080c76c6d8c60d92d27ed95c01f58a2d51fd6f87ec}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩