diff --git a/backlog/gself-pow-six-add-pow-four.md b/backlog/gself-pow-six-add-pow-four.md new file mode 100644 index 000000000..09e41d0c2 --- /dev/null +++ b/backlog/gself-pow-six-add-pow-four.md @@ -0,0 +1,7 @@ +# gself-pow-six-add-pow-four + +n to the 1 divides n to the 6 plus n to the 4. + +- **Source:** self-seeded polynomial-divisibility identity family. +- **Reference:** n to the 1 divides n to the 6 plus n to the 4. Provable by exhibiting the cofactor and `ring`. +- **Difficulty:** 1 diff --git a/goals/gself-pow-six-add-pow-four.aisp b/goals/gself-pow-six-add-pow-four.aisp new file mode 100644 index 000000000..d74b903ef --- /dev/null +++ b/goals/gself-pow-six-add-pow-four.aisp @@ -0,0 +1,20 @@ +𝔸5.1.goal.gself-pow-six-add-pow-four@2026-06-17 +γ≔unsorry.goal +⟦Ω:Goal⟧{ + id≜gself-pow-six-add-pow-four + phase≜prove + status≜proved + difficulty≜1 +} +⟦Σ:Source⟧{ + src≜backlog/gself-pow-six-add-pow-four.md +} +⟦Γ:Deps⟧{ + deps≜⟨⟩ +} +⟦Λ:Artifact⟧{ + lean≜goals/gself-pow-six-add-pow-four.lean + sha≜fabd9af2348551dd0d3d368701ad8a88fc6589529147a2da5439692d152ff44a + aff≜0 +} +⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩ diff --git a/goals/gself-pow-six-add-pow-four.lean b/goals/gself-pow-six-add-pow-four.lean new file mode 100644 index 000000000..b5a343199 --- /dev/null +++ b/goals/gself-pow-six-add-pow-four.lean @@ -0,0 +1,4 @@ +import Mathlib + +theorem gself_pow_six_add_pow_four (n : ℤ) : (n) ∣ (n^6 + n^4) := by + sorry diff --git a/library/Unsorry/GselfPowSixAddPowFour.lean b/library/Unsorry/GselfPowSixAddPowFour.lean new file mode 100644 index 000000000..7722a7e29 --- /dev/null +++ b/library/Unsorry/GselfPowSixAddPowFour.lean @@ -0,0 +1,4 @@ +import Mathlib + +theorem gself_pow_six_add_pow_four (n : ℤ) : (n) ∣ (n^6 + n^4) := by + exact ⟨n^5 + n^3, by ring⟩ diff --git a/library/index/fabd9af2348551dd0d3d368701ad8a88fc6589529147a2da5439692d152ff44a.aisp b/library/index/fabd9af2348551dd0d3d368701ad8a88fc6589529147a2da5439692d152ff44a.aisp new file mode 100644 index 000000000..f0de15bf3 --- /dev/null +++ b/library/index/fabd9af2348551dd0d3d368701ad8a88fc6589529147a2da5439692d152ff44a.aisp @@ -0,0 +1,8 @@ +𝔸5.1.lemma.fabd9af23485@2026-06-17 +γ≔unsorry.lemma.index +⟦Ω:Lemma⟧{sha≜fabd9af2348551dd0d3d368701ad8a88fc6589529147a2da5439692d152ff44a; goal≜gself-pow-six-add-pow-four; name≜gself_pow_six_add_pow_four} +⟦Σ:Source⟧{src≜goals/gself-pow-six-add-pow-four.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-four.mac-158f.20260617t182449370855z-70e27665.aisp b/proof-runs/gself-pow-six-add-pow-four.mac-158f.20260617t182449370855z-70e27665.aisp new file mode 100644 index 000000000..e1aeab2f7 --- /dev/null +++ b/proof-runs/gself-pow-six-add-pow-four.mac-158f.20260617t182449370855z-70e27665.aisp @@ -0,0 +1,8 @@ +𝔸5.1.run.gself-pow-six-add-pow-four.mac-158f.20260617t182449370855z-70e27665@2026-06-17 +γ≔unsorry.proof.run +⟦Ω:Run⟧{id≜20260617t182449370855z-70e27665; goal≜gself-pow-six-add-pow-four; agent≜mac-158f; outcome≜proved} +⟦Π:Provenance⟧{solver≜ohdearquant; provider≜claude; model≜template-ring-cofactor} +⟦Γ:Goal⟧{goal≜gself-pow-six-add-pow-four} +⟦Λ:Metrics⟧{attempts≜1; solve_s≜0; ended≜2026-06-17T18:24:49Z} +⟦Σ:Artifact⟧{sha≜fabd9af2348551dd0d3d368701ad8a88fc6589529147a2da5439692d152ff44a} +⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩