diff --git a/backlog/gself-pow-four-add-pow-two.md b/backlog/gself-pow-four-add-pow-two.md new file mode 100644 index 000000000..4d76ec37e --- /dev/null +++ b/backlog/gself-pow-four-add-pow-two.md @@ -0,0 +1,7 @@ +# gself-pow-four-add-pow-two + +n to the 1 divides n to the 4 plus n to the 2. + +- **Source:** self-seeded polynomial-divisibility identity family. +- **Reference:** n to the 1 divides n to the 4 plus n to the 2. Provable by exhibiting the cofactor and `ring`. +- **Difficulty:** 1 diff --git a/goals/gself-pow-four-add-pow-two.aisp b/goals/gself-pow-four-add-pow-two.aisp new file mode 100644 index 000000000..01961c9e3 --- /dev/null +++ b/goals/gself-pow-four-add-pow-two.aisp @@ -0,0 +1,20 @@ +𝔸5.1.goal.gself-pow-four-add-pow-two@2026-06-17 +γ≔unsorry.goal +⟦Ω:Goal⟧{ + id≜gself-pow-four-add-pow-two + phase≜prove + status≜proved + difficulty≜1 +} +⟦Σ:Source⟧{ + src≜backlog/gself-pow-four-add-pow-two.md +} +⟦Γ:Deps⟧{ + deps≜⟨⟩ +} +⟦Λ:Artifact⟧{ + lean≜goals/gself-pow-four-add-pow-two.lean + sha≜606984ed3145cd857a17033830761f57fc2fb37b3a0679f01eaa63f70104cef8 + aff≜0 +} +⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩ diff --git a/goals/gself-pow-four-add-pow-two.lean b/goals/gself-pow-four-add-pow-two.lean new file mode 100644 index 000000000..78fcdf525 --- /dev/null +++ b/goals/gself-pow-four-add-pow-two.lean @@ -0,0 +1,4 @@ +import Mathlib + +theorem gself_pow_four_add_pow_two (n : ℤ) : (n) ∣ (n^4 + n^2) := by + sorry diff --git a/library/Unsorry/GselfPowFourAddPowTwo.lean b/library/Unsorry/GselfPowFourAddPowTwo.lean new file mode 100644 index 000000000..50159b353 --- /dev/null +++ b/library/Unsorry/GselfPowFourAddPowTwo.lean @@ -0,0 +1,4 @@ +import Mathlib + +theorem gself_pow_four_add_pow_two (n : ℤ) : (n) ∣ (n^4 + n^2) := by + exact ⟨n^3 + n, by ring⟩ diff --git a/library/index/606984ed3145cd857a17033830761f57fc2fb37b3a0679f01eaa63f70104cef8.aisp b/library/index/606984ed3145cd857a17033830761f57fc2fb37b3a0679f01eaa63f70104cef8.aisp new file mode 100644 index 000000000..bf244ffe5 --- /dev/null +++ b/library/index/606984ed3145cd857a17033830761f57fc2fb37b3a0679f01eaa63f70104cef8.aisp @@ -0,0 +1,8 @@ +𝔸5.1.lemma.606984ed3145@2026-06-17 +γ≔unsorry.lemma.index +⟦Ω:Lemma⟧{sha≜606984ed3145cd857a17033830761f57fc2fb37b3a0679f01eaa63f70104cef8; goal≜gself-pow-four-add-pow-two; name≜gself_pow_four_add_pow_two} +⟦Σ:Source⟧{src≜goals/gself-pow-four-add-pow-two.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-four-add-pow-two.mac-158f.20260617t182241255352z-4725992c.aisp b/proof-runs/gself-pow-four-add-pow-two.mac-158f.20260617t182241255352z-4725992c.aisp new file mode 100644 index 000000000..ec94b0555 --- /dev/null +++ b/proof-runs/gself-pow-four-add-pow-two.mac-158f.20260617t182241255352z-4725992c.aisp @@ -0,0 +1,8 @@ +𝔸5.1.run.gself-pow-four-add-pow-two.mac-158f.20260617t182241255352z-4725992c@2026-06-17 +γ≔unsorry.proof.run +⟦Ω:Run⟧{id≜20260617t182241255352z-4725992c; goal≜gself-pow-four-add-pow-two; agent≜mac-158f; outcome≜proved} +⟦Π:Provenance⟧{solver≜ohdearquant; provider≜claude; model≜template-ring-cofactor} +⟦Γ:Goal⟧{goal≜gself-pow-four-add-pow-two} +⟦Λ:Metrics⟧{attempts≜1; solve_s≜0; ended≜2026-06-17T18:22:41Z} +⟦Σ:Artifact⟧{sha≜606984ed3145cd857a17033830761f57fc2fb37b3a0679f01eaa63f70104cef8} +⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩