From 91fe64b89ad9de121c74c3ffb447701aa261cb3c Mon Sep 17 00:00:00 2001
From: OceanLi <122793010+ohdearquant@users.noreply.github.com>
Date: Wed, 17 Jun 2026 14:18:34 -0400
Subject: [PATCH] prove(ggeom-pred-pow-four-sub-one):
 ggeom_pred_pow_four_sub_one by mac-158f

---
 backlog/ggeom-pred-pow-four-sub-one.md        |  7 +++++++
 goals/ggeom-pred-pow-four-sub-one.aisp        | 20 +++++++++++++++++++
 goals/ggeom-pred-pow-four-sub-one.lean        |  4 ++++
 library/Unsorry/GgeomPredPowFourSubOne.lean   |  4 ++++
 ...f20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad.aisp |  8 ++++++++
 ...-158f.20260617t181833587508z-a91d5d21.aisp |  8 ++++++++
 6 files changed, 51 insertions(+)
 create mode 100644 backlog/ggeom-pred-pow-four-sub-one.md
 create mode 100644 goals/ggeom-pred-pow-four-sub-one.aisp
 create mode 100644 goals/ggeom-pred-pow-four-sub-one.lean
 create mode 100644 library/Unsorry/GgeomPredPowFourSubOne.lean
 create mode 100644 library/index/c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad.aisp
 create mode 100644 proof-runs/ggeom-pred-pow-four-sub-one.mac-158f.20260617t181833587508z-a91d5d21.aisp

diff --git a/backlog/ggeom-pred-pow-four-sub-one.md b/backlog/ggeom-pred-pow-four-sub-one.md
new file mode 100644
index 000000000..7e9de3827
--- /dev/null
+++ b/backlog/ggeom-pred-pow-four-sub-one.md
@@ -0,0 +1,7 @@
+# ggeom-pred-pow-four-sub-one
+
+n minus one divides n to the 4 minus one.
+
+- **Source:** self-seeded polynomial-divisibility identity family.
+- **Reference:** n minus one divides n to the 4 minus one. Provable by exhibiting the cofactor and `ring`.
+- **Difficulty:** 1
diff --git a/goals/ggeom-pred-pow-four-sub-one.aisp b/goals/ggeom-pred-pow-four-sub-one.aisp
new file mode 100644
index 000000000..3c0cd8332
--- /dev/null
+++ b/goals/ggeom-pred-pow-four-sub-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.ggeom-pred-pow-four-sub-one@2026-06-17
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜ggeom-pred-pow-four-sub-one
+  phase≜prove
+  status≜proved
+  difficulty≜1
+}
+⟦Σ:Source⟧{
+  src≜backlog/ggeom-pred-pow-four-sub-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/ggeom-pred-pow-four-sub-one.lean
+  sha≜c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad
+  aff≜0
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/ggeom-pred-pow-four-sub-one.lean b/goals/ggeom-pred-pow-four-sub-one.lean
new file mode 100644
index 000000000..be6ccab9f
--- /dev/null
+++ b/goals/ggeom-pred-pow-four-sub-one.lean
@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem ggeom_pred_pow_four_sub_one (n : ℤ) : (n - 1) ∣ (n^4 - 1) := by
+  sorry
diff --git a/library/Unsorry/GgeomPredPowFourSubOne.lean b/library/Unsorry/GgeomPredPowFourSubOne.lean
new file mode 100644
index 000000000..80dd7e579
--- /dev/null
+++ b/library/Unsorry/GgeomPredPowFourSubOne.lean
@@ -0,0 +1,4 @@
+import Mathlib
+
+theorem ggeom_pred_pow_four_sub_one (n : ℤ) : (n - 1) ∣ (n^4 - 1) := by
+  exact ⟨n^3 + n^2 + n + 1, by ring⟩
diff --git a/library/index/c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad.aisp b/library/index/c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad.aisp
new file mode 100644
index 000000000..cfa144bca
--- /dev/null
+++ b/library/index/c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad.aisp
@@ -0,0 +1,8 @@
+𝔸5.1.lemma.c08fe23d1086@2026-06-17
+γ≔unsorry.lemma.index
+⟦Ω:Lemma⟧{sha≜c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad; goal≜ggeom-pred-pow-four-sub-one; name≜ggeom_pred_pow_four_sub_one}
+⟦Σ:Source⟧{src≜goals/ggeom-pred-pow-four-sub-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/ggeom-pred-pow-four-sub-one.mac-158f.20260617t181833587508z-a91d5d21.aisp b/proof-runs/ggeom-pred-pow-four-sub-one.mac-158f.20260617t181833587508z-a91d5d21.aisp
new file mode 100644
index 000000000..174abf3c4
--- /dev/null
+++ b/proof-runs/ggeom-pred-pow-four-sub-one.mac-158f.20260617t181833587508z-a91d5d21.aisp
@@ -0,0 +1,8 @@
+𝔸5.1.run.ggeom-pred-pow-four-sub-one.mac-158f.20260617t181833587508z-a91d5d21@2026-06-17
+γ≔unsorry.proof.run
+⟦Ω:Run⟧{id≜20260617t181833587508z-a91d5d21; goal≜ggeom-pred-pow-four-sub-one; agent≜mac-158f; outcome≜proved}
+⟦Π:Provenance⟧{solver≜ohdearquant; provider≜claude; model≜template-ring-cofactor}
+⟦Γ:Goal⟧{goal≜ggeom-pred-pow-four-sub-one}
+⟦Λ:Metrics⟧{attempts≜1; solve_s≜0; ended≜2026-06-17T18:18:33Z}
+⟦Σ:Artifact⟧{sha≜c08fe23d10861338eb62e64cd5df20d28c7ba0f1d3e247cdd2dd6b5fe9a022ad}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩