From c08b38a60e7f3717c61e07d1a6c0d7cb88ed3058 Mon Sep 17 00:00:00 2001
From: unsorry-auto-archive <noreply@unsorry>
Date: Thu, 18 Jun 2026 18:54:57 +0000
Subject: [PATCH] chore(archive): auto-retire active copies for block
 unsorry-archive-0008
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Automated ADR-041 / SPEC-041-A §9 cut: active proved-not-archived (332) >=
ceiling (40). Keeps the active full-replay/build set bounded to prevent the
exit-137 OOM; archived proofs are provenance+packaging validated, not re-replayed
(ADR-048).
---
 goals/gcd-5n3-7n4-eq-one.aisp                 |   6 +-
 goals/gcd-6n5-4n3-eq-one.aisp                 |   6 +-
 goals/gcd-6n5-6n11-eq-one.aisp                |   6 +-
 goals/gcd-factorial-succ-eq-factorial.aisp    |   6 +-
 goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp    |   6 +-
 goals/gcd-n-add-six-dvd-six.aisp              |   6 +-
 goals/gcd-n-factorial-succ-eq-one.aisp        |   6 +-
 goals/gcd-n1-n7-dvd-six.aisp                  |   6 +-
 goals/gcd-n2-2n5-eq-one.aisp                  |   6 +-
 goals/gcd-n2-n4-dvd-two.aisp                  |   6 +-
 goals/gcd-n2-n6-dvd-four.aisp                 |   6 +-
 goals/gcd-n2-n8-dvd-six.aisp                  |   6 +-
 goals/gcd-n2p1-n2p3-dvd-two.aisp              |   6 +-
 goals/gcd-n3-2n7-eq-one.aisp                  |   6 +-
 goals/gcd-n3p1-np1-eq-np1.aisp                |   6 +-
 goals/gcd-n4p1-n2p1-dvd-two.aisp              |   6 +-
 goals/gcd-np1-2np1-eq-one.aisp                |   6 +-
 goals/gcd-np1-n2p1-dvd-two.aisp               |   6 +-
 goals/gcd-nsq1-n1-dvd-two.aisp                |   6 +-
 goals/gcd-nsq1-nsq3-dvd-two.aisp              |   6 +-
 goals/gcd-quad-factored-n1-eq-n1.aisp         |   6 +-
 goals/gcd-sq-n-sq-n-one.aisp                  |   6 +-
 .../gcd-three-pow-succ-three-pow-add-one.aisp |   6 +-
 goals/gcd-threen-n7-dvd-twentyone.aisp        |   6 +-
 .../gcd-two-pow-add-one-sub-one-dvd-two.aisp  |   6 +-
 goals/gcd-twon-n5-dvd-ten.aisp                |   6 +-
 ...s-succ-add-lucas-pred-eq-five-mul-fib.aisp |   6 +-
 goals/ninth-power-mod-nineteen-mem.aisp       |   6 +-
 goals/pair-sum-sq-ge-three-abc-sum.aisp       |   6 +-
 ...rwise-product-sum-sq-ge-three-abc-sum.aisp |   6 +-
 ...ell-brahmagupta-composition-generic-d.aisp |   6 +-
 ...d10-fundamental-ladder-step-preserves.aisp |   6 +-
 goals/pell-d11-ladder-step-preserves.aisp     |   6 +-
 goals/pell-d12-ladder-step-preserves.aisp     |   6 +-
 goals/pell-d13-ladder-step-preserves.aisp     |   6 +-
 goals/pell-d14-ladder-step-preserves.aisp     |   6 +-
 goals/pell-d15-ladder-step-preserves.aisp     |   6 +-
 goals/pell-d17-ladder-step-preserves.aisp     |   6 +-
 goals/pell-d18-ladder-step-preserves.aisp     |   6 +-
 .../pell-d2-form-product-telescope-step.aisp  |   6 +-
 .../archive-manifest.json                     | 179 ++++++++++++++++++
 .../backlog}/gcd-5n3-7n4-eq-one.md            |   0
 .../backlog}/gcd-6n5-4n3-eq-one.md            |   0
 .../backlog}/gcd-6n5-6n11-eq-one.md           |   0
 .../gcd-factorial-succ-eq-factorial.md        |   0
 .../gcd-fib-add-two-eq-gcd-fib-succ.md        |   0
 .../backlog}/gcd-n-add-six-dvd-six.md         |   0
 .../backlog}/gcd-n-factorial-succ-eq-one.md   |   0
 .../backlog}/gcd-n1-n7-dvd-six.md             |   0
 .../backlog}/gcd-n2-2n5-eq-one.md             |   0
 .../backlog}/gcd-n2-n4-dvd-two.md             |   0
 .../backlog}/gcd-n2-n6-dvd-four.md            |   0
 .../backlog}/gcd-n2-n8-dvd-six.md             |   0
 .../backlog}/gcd-n2p1-n2p3-dvd-two.md         |   0
 .../backlog}/gcd-n3-2n7-eq-one.md             |   0
 .../backlog}/gcd-n3p1-np1-eq-np1.md           |   0
 .../backlog}/gcd-n4p1-n2p1-dvd-two.md         |   0
 .../backlog}/gcd-np1-2np1-eq-one.md           |   0
 .../backlog}/gcd-np1-n2p1-dvd-two.md          |   0
 .../backlog}/gcd-nsq1-n1-dvd-two.md           |   0
 .../backlog}/gcd-nsq1-nsq3-dvd-two.md         |   0
 .../backlog}/gcd-quad-factored-n1-eq-n1.md    |   0
 .../backlog}/gcd-sq-n-sq-n-one.md             |   0
 .../gcd-three-pow-succ-three-pow-add-one.md   |   0
 .../backlog}/gcd-threen-n7-dvd-twentyone.md   |   0
 .../gcd-two-pow-add-one-sub-one-dvd-two.md    |   0
 .../backlog}/gcd-twon-n5-dvd-ten.md           |   0
 ...cas-succ-add-lucas-pred-eq-five-mul-fib.md |   0
 .../backlog}/ninth-power-mod-nineteen-mem.md  |   0
 .../backlog}/pair-sum-sq-ge-three-abc-sum.md  |   0
 ...airwise-product-sum-sq-ge-three-abc-sum.md |   0
 .../pell-brahmagupta-composition-generic-d.md |   0
 ...l-d10-fundamental-ladder-step-preserves.md |   0
 .../pell-d11-ladder-step-preserves.md         |   0
 .../pell-d12-ladder-step-preserves.md         |   0
 .../pell-d13-ladder-step-preserves.md         |   0
 .../pell-d14-ladder-step-preserves.md         |   0
 .../pell-d15-ladder-step-preserves.md         |   0
 .../pell-d17-ladder-step-preserves.md         |   0
 .../pell-d18-ladder-step-preserves.md         |   0
 .../pell-d2-form-product-telescope-step.md    |   0
 .../goals/gcd-5n3-7n4-eq-one.aisp             |  20 ++
 .../goals}/gcd-5n3-7n4-eq-one.lean            |   0
 .../goals/gcd-6n5-4n3-eq-one.aisp             |  20 ++
 .../goals}/gcd-6n5-4n3-eq-one.lean            |   0
 .../goals/gcd-6n5-6n11-eq-one.aisp            |  20 ++
 .../goals}/gcd-6n5-6n11-eq-one.lean           |   0
 .../gcd-factorial-succ-eq-factorial.aisp      |  20 ++
 .../gcd-factorial-succ-eq-factorial.lean      |   0
 .../gcd-fib-add-two-eq-gcd-fib-succ.aisp      |  20 ++
 .../gcd-fib-add-two-eq-gcd-fib-succ.lean      |   0
 .../goals/gcd-n-add-six-dvd-six.aisp          |  20 ++
 .../goals}/gcd-n-add-six-dvd-six.lean         |   0
 .../goals/gcd-n-factorial-succ-eq-one.aisp    |  20 ++
 .../goals}/gcd-n-factorial-succ-eq-one.lean   |   0
 .../goals/gcd-n1-n7-dvd-six.aisp              |  20 ++
 .../goals}/gcd-n1-n7-dvd-six.lean             |   0
 .../goals/gcd-n2-2n5-eq-one.aisp              |  20 ++
 .../goals}/gcd-n2-2n5-eq-one.lean             |   0
 .../goals/gcd-n2-n4-dvd-two.aisp              |  20 ++
 .../goals}/gcd-n2-n4-dvd-two.lean             |   0
 .../goals/gcd-n2-n6-dvd-four.aisp             |  20 ++
 .../goals}/gcd-n2-n6-dvd-four.lean            |   0
 .../goals/gcd-n2-n8-dvd-six.aisp              |  20 ++
 .../goals}/gcd-n2-n8-dvd-six.lean             |   0
 .../goals/gcd-n2p1-n2p3-dvd-two.aisp          |  20 ++
 .../goals}/gcd-n2p1-n2p3-dvd-two.lean         |   0
 .../goals/gcd-n3-2n7-eq-one.aisp              |  20 ++
 .../goals}/gcd-n3-2n7-eq-one.lean             |   0
 .../goals/gcd-n3p1-np1-eq-np1.aisp            |  20 ++
 .../goals}/gcd-n3p1-np1-eq-np1.lean           |   0
 .../goals/gcd-n4p1-n2p1-dvd-two.aisp          |  20 ++
 .../goals}/gcd-n4p1-n2p1-dvd-two.lean         |   0
 .../goals/gcd-np1-2np1-eq-one.aisp            |  20 ++
 .../goals}/gcd-np1-2np1-eq-one.lean           |   0
 .../goals/gcd-np1-n2p1-dvd-two.aisp           |  20 ++
 .../goals}/gcd-np1-n2p1-dvd-two.lean          |   0
 .../goals/gcd-nsq1-n1-dvd-two.aisp            |  20 ++
 .../goals}/gcd-nsq1-n1-dvd-two.lean           |   0
 .../goals/gcd-nsq1-nsq3-dvd-two.aisp          |  20 ++
 .../goals}/gcd-nsq1-nsq3-dvd-two.lean         |   0
 .../goals/gcd-quad-factored-n1-eq-n1.aisp     |  20 ++
 .../goals}/gcd-quad-factored-n1-eq-n1.lean    |   0
 .../goals/gcd-sq-n-sq-n-one.aisp              |  20 ++
 .../goals}/gcd-sq-n-sq-n-one.lean             |   0
 .../gcd-three-pow-succ-three-pow-add-one.aisp |  20 ++
 .../gcd-three-pow-succ-three-pow-add-one.lean |   0
 .../goals/gcd-threen-n7-dvd-twentyone.aisp    |  20 ++
 .../goals}/gcd-threen-n7-dvd-twentyone.lean   |   0
 .../gcd-two-pow-add-one-sub-one-dvd-two.aisp  |  20 ++
 .../gcd-two-pow-add-one-sub-one-dvd-two.lean  |   0
 .../goals/gcd-twon-n5-dvd-ten.aisp            |  20 ++
 .../goals}/gcd-twon-n5-dvd-ten.lean           |   0
 ...s-succ-add-lucas-pred-eq-five-mul-fib.aisp |  20 ++
 ...s-succ-add-lucas-pred-eq-five-mul-fib.lean |   0
 .../goals/ninth-power-mod-nineteen-mem.aisp   |  20 ++
 .../goals}/ninth-power-mod-nineteen-mem.lean  |   0
 .../goals/pair-sum-sq-ge-three-abc-sum.aisp   |  20 ++
 .../goals}/pair-sum-sq-ge-three-abc-sum.lean  |   0
 ...rwise-product-sum-sq-ge-three-abc-sum.aisp |  20 ++
 ...rwise-product-sum-sq-ge-three-abc-sum.lean |   0
 ...ell-brahmagupta-composition-generic-d.aisp |  20 ++
 ...ell-brahmagupta-composition-generic-d.lean |   0
 ...d10-fundamental-ladder-step-preserves.aisp |  20 ++
 ...d10-fundamental-ladder-step-preserves.lean |   0
 .../goals/pell-d11-ladder-step-preserves.aisp |  20 ++
 .../pell-d11-ladder-step-preserves.lean       |   0
 .../goals/pell-d12-ladder-step-preserves.aisp |  20 ++
 .../pell-d12-ladder-step-preserves.lean       |   0
 .../goals/pell-d13-ladder-step-preserves.aisp |  20 ++
 .../pell-d13-ladder-step-preserves.lean       |   0
 .../goals/pell-d14-ladder-step-preserves.aisp |  20 ++
 .../pell-d14-ladder-step-preserves.lean       |   0
 .../goals/pell-d15-ladder-step-preserves.aisp |  20 ++
 .../pell-d15-ladder-step-preserves.lean       |   0
 .../goals/pell-d17-ladder-step-preserves.aisp |  20 ++
 .../pell-d17-ladder-step-preserves.lean       |   0
 .../goals/pell-d18-ladder-step-preserves.aisp |  20 ++
 .../pell-d18-ladder-step-preserves.lean       |   0
 .../pell-d2-form-product-telescope-step.aisp  |  20 ++
 .../pell-d2-form-product-telescope-step.lean  |   0
 .../unsorry-archive-0008/lake-manifest.json   |  96 ++++++++++
 packages/unsorry-archive-0008/lakefile.toml   |  19 ++
 packages/unsorry-archive-0008/lean-toolchain  |   1 +
 .../library}/Unsorry/Gcd5n37n4EqOne.lean      |   0
 .../library}/Unsorry/Gcd6n54n3EqOne.lean      |   0
 .../library}/Unsorry/Gcd6n56n11EqOne.lean     |   0
 .../Unsorry/GcdFactorialSuccEqFactorial.lean  |   0
 .../Unsorry/GcdFibAddTwoEqGcdFibSucc.lean     |   0
 .../library}/Unsorry/GcdN1N7DvdSix.lean       |   0
 .../library}/Unsorry/GcdN22n5EqOne.lean       |   0
 .../library}/Unsorry/GcdN2N4DvdTwo.lean       |   0
 .../library}/Unsorry/GcdN2N6DvdFour.lean      |   0
 .../library}/Unsorry/GcdN2N8DvdSix.lean       |   0
 .../library}/Unsorry/GcdN2p1N2p3DvdTwo.lean   |   0
 .../library}/Unsorry/GcdN32n7EqOne.lean       |   0
 .../library}/Unsorry/GcdN3p1Np1EqNp1.lean     |   0
 .../library}/Unsorry/GcdN4p1N2p1DvdTwo.lean   |   0
 .../library}/Unsorry/GcdNAddSixDvdSix.lean    |   0
 .../Unsorry/GcdNFactorialSuccEqOne.lean       |   0
 .../library}/Unsorry/GcdNp12np1EqOne.lean     |   0
 .../library}/Unsorry/GcdNp1N2p1DvdTwo.lean    |   0
 .../library}/Unsorry/GcdNsq1N1DvdTwo.lean     |   0
 .../library}/Unsorry/GcdNsq1Nsq3DvdTwo.lean   |   0
 .../Unsorry/GcdQuadFactoredN1EqN1.lean        |   0
 .../library}/Unsorry/GcdSqNSqNOne.lean        |   0
 .../GcdThreePowSuccThreePowAddOne.lean        |   0
 .../Unsorry/GcdThreenN7DvdTwentyone.lean      |   0
 .../Unsorry/GcdTwoPowAddOneSubOneDvdTwo.lean  |   0
 .../library}/Unsorry/GcdTwonN5DvdTen.lean     |   0
 .../LucasSuccAddLucasPredEqFiveMulFib.lean    |   0
 .../Unsorry/NinthPowerModNineteenMem.lean     |   0
 .../Unsorry/PairSumSqGeThreeAbcSum.lean       |   0
 .../PairwiseProductSumSqGeThreeAbcSum.lean    |   0
 .../PellBrahmaguptaCompositionGenericD.lean   |   0
 ...PellD10FundamentalLadderStepPreserves.lean |   0
 .../Unsorry/PellD11LadderStepPreserves.lean   |   0
 .../Unsorry/PellD12LadderStepPreserves.lean   |   0
 .../Unsorry/PellD13LadderStepPreserves.lean   |   0
 .../Unsorry/PellD14LadderStepPreserves.lean   |   0
 .../Unsorry/PellD15LadderStepPreserves.lean   |   0
 .../Unsorry/PellD17LadderStepPreserves.lean   |   0
 .../Unsorry/PellD18LadderStepPreserves.lean   |   0
 .../PellD2FormProductTelescopeStep.lean       |   0
 ...fcc883bf907094752825b176920ba04dca541.aisp |   0
 ...794a2c4869d8a033d7b6663a8fe019113075a.aisp |   0
 ...c650fa72713e697a977fae440c8206daa846c.aisp |   0
 ...e3d5102ee0dfa45e7d93ad3a5d27081047e0f.aisp |   0
 ...f879efeca95a7659fdcc455d82825d2b5eb53.aisp |   0
 ...96c2d1a7f66be09d9757ae7be7826b26b2ee0.aisp |   0
 ...82ab947d163d4bf572d8aa1beb67f3ca3ddf2.aisp |   0
 ...437ade2204a79336534c418b82679d3b2a5c4.aisp |   0
 ...86c99a00bb230f80bab431c71744e2e7913fe.aisp |   0
 ...2a6bf7197d4721a37a0d3123ae268408b9c49.aisp |   0
 ...3cb785c124444f8cc83f0573f277a6b5a8083.aisp |   0
 ...dfac9445450e0b1476cfbb17898e80abbc218.aisp |   0
 ...307ebdd7a08251c47abd62cbd314b82051562.aisp |   0
 ...f6fc546aaea76608b07dd9b5387dea1c3838b.aisp |   0
 ...fa5420d5b84799ec33173e3ad9f179eeab7f2.aisp |   0
 ...609308c6e1a7eb0e42c583aee984ca3e8072a.aisp |   0
 ...8045c674dc4f1e78703074e4905c8f6d080cb.aisp |   0
 ...7c3dd915bedbfd8bc799804c38bb5c203f3dd.aisp |   0
 ...9c0811a1e4e9525de6f8dc8b325cd5c68c633.aisp |   0
 ...c91b8ee79a17b760017f45dd6487a226303ad.aisp |   0
 ...b85f21e58904b58f7ba1fee1ee15100b4dbde.aisp |   0
 ...31a9b3e6e49faca199b59099661203575ac6b.aisp |   0
 ...d93bcd33e22aa0b5e4a3c2326d1057c6bb866.aisp |   0
 ...dff0433299992151f143fa01f7ccf221ae6ca.aisp |   0
 ...1f22c798ec68e88c1de770b1d2126703e91d0.aisp |   0
 ...fa207aebce2e771a2c76b6a63a6dd8add7310.aisp |   0
 ...c5fed71c7c1d70e5d576c26523661f5ca6274.aisp |   0
 ...ed22f0b3bfce874cfb7265bf341aa1729205b.aisp |   0
 ...2b362cc632946435f2b1fd8075dcda5c64fb0.aisp |   0
 ...337721b38e10b087f44a1ff32aaf0550022cd.aisp |   0
 ...878d978468849aea54fc8edd840e7f5d27520.aisp |   0
 ...8cc9e5a3cce110d6335735be6d9ac6a6ee337.aisp |   0
 ...9177d86a426210872ec4133e31e01c160e44a.aisp |   0
 ...200fff6fdb19c077687d94e2a14da640c1934.aisp |   0
 ...bdc2c2123a91c94f73b657559774a68955528.aisp |   0
 ...e7edd819573d85528bb7bc6a4e72579ae7216.aisp |   0
 ...7bc864a559198820ae251a46663498fb7943f.aisp |   0
 ...bb369dd29d4a63e7c1fee0531ad30b30ffce8.aisp |   0
 ...ffc147f193ac2e82f1d37ffbdf69d92d01c8a.aisp |   0
 ...808c67ae87454d2db4f429bde563ceac11874.aisp |   0
 244 files changed, 1215 insertions(+), 120 deletions(-)
 create mode 100644 packages/unsorry-archive-0008/archive-manifest.json
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-5n3-7n4-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-6n5-4n3-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-6n5-6n11-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-factorial-succ-eq-factorial.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-fib-add-two-eq-gcd-fib-succ.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n-add-six-dvd-six.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n-factorial-succ-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n1-n7-dvd-six.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n2-2n5-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n2-n4-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n2-n6-dvd-four.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n2-n8-dvd-six.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n2p1-n2p3-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n3-2n7-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n3p1-np1-eq-np1.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-n4p1-n2p1-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-np1-2np1-eq-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-np1-n2p1-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-nsq1-n1-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-nsq1-nsq3-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-quad-factored-n1-eq-n1.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-sq-n-sq-n-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-three-pow-succ-three-pow-add-one.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-threen-n7-dvd-twentyone.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-two-pow-add-one-sub-one-dvd-two.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/gcd-twon-n5-dvd-ten.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/lucas-succ-add-lucas-pred-eq-five-mul-fib.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/ninth-power-mod-nineteen-mem.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pair-sum-sq-ge-three-abc-sum.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pairwise-product-sum-sq-ge-three-abc-sum.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-brahmagupta-composition-generic-d.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d10-fundamental-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d11-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d12-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d13-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d14-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d15-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d17-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d18-ladder-step-preserves.md (100%)
 rename {backlog => packages/unsorry-archive-0008/backlog}/pell-d2-form-product-telescope-step.md (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-5n3-7n4-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-6n5-4n3-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-6n5-6n11-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-factorial-succ-eq-factorial.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-fib-add-two-eq-gcd-fib-succ.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n-add-six-dvd-six.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n-factorial-succ-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n1-n7-dvd-six.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n2-2n5-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n2-n4-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n2-n6-dvd-four.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n2-n8-dvd-six.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n2p1-n2p3-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n3-2n7-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n3p1-np1-eq-np1.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-n4p1-n2p1-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-np1-2np1-eq-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-np1-n2p1-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-nsq1-n1-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-nsq1-nsq3-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-quad-factored-n1-eq-n1.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-sq-n-sq-n-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-three-pow-succ-three-pow-add-one.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-threen-n7-dvd-twentyone.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-two-pow-add-one-sub-one-dvd-two.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/gcd-twon-n5-dvd-ten.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/ninth-power-mod-nineteen-mem.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pair-sum-sq-ge-three-abc-sum.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pairwise-product-sum-sq-ge-three-abc-sum.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-brahmagupta-composition-generic-d.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d10-fundamental-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d11-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d12-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d13-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d14-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d15-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d17-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d18-ladder-step-preserves.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.aisp
 rename {goals => packages/unsorry-archive-0008/goals}/pell-d2-form-product-telescope-step.lean (100%)
 create mode 100644 packages/unsorry-archive-0008/lake-manifest.json
 create mode 100644 packages/unsorry-archive-0008/lakefile.toml
 create mode 100644 packages/unsorry-archive-0008/lean-toolchain
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/Gcd5n37n4EqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/Gcd6n54n3EqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/Gcd6n56n11EqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdFactorialSuccEqFactorial.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdFibAddTwoEqGcdFibSucc.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN1N7DvdSix.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN22n5EqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN2N4DvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN2N6DvdFour.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN2N8DvdSix.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN2p1N2p3DvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN32n7EqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN3p1Np1EqNp1.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdN4p1N2p1DvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdNAddSixDvdSix.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdNFactorialSuccEqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdNp12np1EqOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdNp1N2p1DvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdNsq1N1DvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdNsq1Nsq3DvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdQuadFactoredN1EqN1.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdSqNSqNOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdThreePowSuccThreePowAddOne.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdThreenN7DvdTwentyone.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdTwoPowAddOneSubOneDvdTwo.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/GcdTwonN5DvdTen.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/LucasSuccAddLucasPredEqFiveMulFib.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/NinthPowerModNineteenMem.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PairSumSqGeThreeAbcSum.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PairwiseProductSumSqGeThreeAbcSum.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellBrahmaguptaCompositionGenericD.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD10FundamentalLadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD11LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD12LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD13LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD14LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD15LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD17LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD18LadderStepPreserves.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/Unsorry/PellD2FormProductTelescopeStep.lean (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a.aisp (100%)
 rename {library => packages/unsorry-archive-0008/library}/index/f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874.aisp (100%)

diff --git a/goals/gcd-5n3-7n4-eq-one.aisp b/goals/gcd-5n3-7n4-eq-one.aisp
index 68bc9bee9..175b70e6a 100644
--- a/goals/gcd-5n3-7n4-eq-one.aisp
+++ b/goals/gcd-5n3-7n4-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-5n3-7n4-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-5n3-7n4-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-5n3-7n4-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-5n3-7n4-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.lean
   sha≜a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b
   aff≜-10
 }
diff --git a/goals/gcd-6n5-4n3-eq-one.aisp b/goals/gcd-6n5-4n3-eq-one.aisp
index ac6097a34..90e62210d 100644
--- a/goals/gcd-6n5-4n3-eq-one.aisp
+++ b/goals/gcd-6n5-4n3-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-6n5-4n3-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-6n5-4n3-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-6n5-4n3-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-6n5-4n3-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.lean
   sha≜da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934
   aff≜-9
 }
diff --git a/goals/gcd-6n5-6n11-eq-one.aisp b/goals/gcd-6n5-6n11-eq-one.aisp
index 7a163fc1f..b9c912b67 100644
--- a/goals/gcd-6n5-6n11-eq-one.aisp
+++ b/goals/gcd-6n5-6n11-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-6n5-6n11-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-6n5-6n11-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-6n5-6n11-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-6n5-6n11-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.lean
   sha≜058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541
   aff≜-9
 }
diff --git a/goals/gcd-factorial-succ-eq-factorial.aisp b/goals/gcd-factorial-succ-eq-factorial.aisp
index 66b25adf3..4e258699a 100644
--- a/goals/gcd-factorial-succ-eq-factorial.aisp
+++ b/goals/gcd-factorial-succ-eq-factorial.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-factorial-succ-eq-factorial
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-factorial-succ-eq-factorial.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-factorial-succ-eq-factorial.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-factorial-succ-eq-factorial.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.lean
   sha≜2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0
   aff≜-10
 }
diff --git a/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp b/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
index df67e7d69..65a300b67 100644
--- a/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
+++ b/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-fib-add-two-eq-gcd-fib-succ
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
   sha≜6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a
   aff≜-10
 }
diff --git a/goals/gcd-n-add-six-dvd-six.aisp b/goals/gcd-n-add-six-dvd-six.aisp
index 9be7228d9..1e5611842 100644
--- a/goals/gcd-n-add-six-dvd-six.aisp
+++ b/goals/gcd-n-add-six-dvd-six.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n-add-six-dvd-six
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n-add-six-dvd-six.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n-add-six-dvd-six.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n-add-six-dvd-six.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.lean
   sha≜4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218
   aff≜-9
 }
diff --git a/goals/gcd-n-factorial-succ-eq-one.aisp b/goals/gcd-n-factorial-succ-eq-one.aisp
index 07be8b28f..a1a92ebd4 100644
--- a/goals/gcd-n-factorial-succ-eq-one.aisp
+++ b/goals/gcd-n-factorial-succ-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n-factorial-succ-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n-factorial-succ-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n-factorial-succ-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n-factorial-succ-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.lean
   sha≜e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528
   aff≜-10
 }
diff --git a/goals/gcd-n1-n7-dvd-six.aisp b/goals/gcd-n1-n7-dvd-six.aisp
index 977cbcc94..3edb224e9 100644
--- a/goals/gcd-n1-n7-dvd-six.aisp
+++ b/goals/gcd-n1-n7-dvd-six.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n1-n7-dvd-six
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n1-n7-dvd-six.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n1-n7-dvd-six.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n1-n7-dvd-six.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.lean
   sha≜2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53
   aff≜-9
 }
diff --git a/goals/gcd-n2-2n5-eq-one.aisp b/goals/gcd-n2-2n5-eq-one.aisp
index f7f511ae7..52503dcba 100644
--- a/goals/gcd-n2-2n5-eq-one.aisp
+++ b/goals/gcd-n2-2n5-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n2-2n5-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n2-2n5-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n2-2n5-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n2-2n5-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.lean
   sha≜794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde
   aff≜-9
 }
diff --git a/goals/gcd-n2-n4-dvd-two.aisp b/goals/gcd-n2-n4-dvd-two.aisp
index 2caed74f0..aedcb9699 100644
--- a/goals/gcd-n2-n4-dvd-two.aisp
+++ b/goals/gcd-n2-n4-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n2-n4-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n2-n4-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n2-n4-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n2-n4-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.lean
   sha≜77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad
   aff≜-9
 }
diff --git a/goals/gcd-n2-n6-dvd-four.aisp b/goals/gcd-n2-n6-dvd-four.aisp
index aa938cf60..9e7fb6567 100644
--- a/goals/gcd-n2-n6-dvd-four.aisp
+++ b/goals/gcd-n2-n6-dvd-four.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n2-n6-dvd-four
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n2-n6-dvd-four.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n2-n6-dvd-four.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n2-n6-dvd-four.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.lean
   sha≜1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c
   aff≜-9
 }
diff --git a/goals/gcd-n2-n8-dvd-six.aisp b/goals/gcd-n2-n8-dvd-six.aisp
index 1c73e283a..9caebad18 100644
--- a/goals/gcd-n2-n8-dvd-six.aisp
+++ b/goals/gcd-n2-n8-dvd-six.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n2-n8-dvd-six
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n2-n8-dvd-six.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n2-n8-dvd-six.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n2-n8-dvd-six.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.lean
   sha≜75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633
   aff≜-9
 }
diff --git a/goals/gcd-n2p1-n2p3-dvd-two.aisp b/goals/gcd-n2p1-n2p3-dvd-two.aisp
index 26bc3c0fa..76c9cbf43 100644
--- a/goals/gcd-n2p1-n2p3-dvd-two.aisp
+++ b/goals/gcd-n2p1-n2p3-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n2p1-n2p3-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n2p1-n2p3-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n2p1-n2p3-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n2p1-n2p3-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.lean
   sha≜8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca
   aff≜-10
 }
diff --git a/goals/gcd-n3-2n7-eq-one.aisp b/goals/gcd-n3-2n7-eq-one.aisp
index 7eb69e98a..a1e3f6d34 100644
--- a/goals/gcd-n3-2n7-eq-one.aisp
+++ b/goals/gcd-n3-2n7-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n3-2n7-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n3-2n7-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n3-2n7-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n3-2n7-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.lean
   sha≜3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2
   aff≜-9
 }
diff --git a/goals/gcd-n3p1-np1-eq-np1.aisp b/goals/gcd-n3p1-np1-eq-np1.aisp
index f87c0ce60..0f2873043 100644
--- a/goals/gcd-n3p1-np1-eq-np1.aisp
+++ b/goals/gcd-n3p1-np1-eq-np1.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n3p1-np1-eq-np1
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n3p1-np1-eq-np1.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n3p1-np1-eq-np1.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n3p1-np1-eq-np1.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.lean
   sha≜5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562
   aff≜-10
 }
diff --git a/goals/gcd-n4p1-n2p1-dvd-two.aisp b/goals/gcd-n4p1-n2p1-dvd-two.aisp
index c0b15fd80..3384e88e3 100644
--- a/goals/gcd-n4p1-n2p1-dvd-two.aisp
+++ b/goals/gcd-n4p1-n2p1-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-n4p1-n2p1-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-n4p1-n2p1-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-n4p1-n2p1-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-n4p1-n2p1-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.lean
   sha≜a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310
   aff≜-10
 }
diff --git a/goals/gcd-np1-2np1-eq-one.aisp b/goals/gcd-np1-2np1-eq-one.aisp
index 8a88d301c..0c764d92c 100644
--- a/goals/gcd-np1-2np1-eq-one.aisp
+++ b/goals/gcd-np1-2np1-eq-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-np1-2np1-eq-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-np1-2np1-eq-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-np1-2np1-eq-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-np1-2np1-eq-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.lean
   sha≜ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337
   aff≜-9
 }
diff --git a/goals/gcd-np1-n2p1-dvd-two.aisp b/goals/gcd-np1-n2p1-dvd-two.aisp
index 4fe1acd93..4d48d170a 100644
--- a/goals/gcd-np1-n2p1-dvd-two.aisp
+++ b/goals/gcd-np1-n2p1-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-np1-n2p1-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-np1-n2p1-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-np1-n2p1-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-np1-n2p1-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.lean
   sha≜410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe
   aff≜-10
 }
diff --git a/goals/gcd-nsq1-n1-dvd-two.aisp b/goals/gcd-nsq1-n1-dvd-two.aisp
index edbac15c7..aefc2956a 100644
--- a/goals/gcd-nsq1-n1-dvd-two.aisp
+++ b/goals/gcd-nsq1-n1-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-nsq1-n1-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-nsq1-n1-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-nsq1-n1-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-nsq1-n1-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.lean
   sha≜43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49
   aff≜-10
 }
diff --git a/goals/gcd-nsq1-nsq3-dvd-two.aisp b/goals/gcd-nsq1-nsq3-dvd-two.aisp
index a87852b27..27f4a3630 100644
--- a/goals/gcd-nsq1-nsq3-dvd-two.aisp
+++ b/goals/gcd-nsq1-nsq3-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-nsq1-nsq3-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-nsq1-nsq3-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-nsq1-nsq3-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-nsq1-nsq3-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.lean
   sha≜ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216
   aff≜-9
 }
diff --git a/goals/gcd-quad-factored-n1-eq-n1.aisp b/goals/gcd-quad-factored-n1-eq-n1.aisp
index 138763e06..4ba54ea52 100644
--- a/goals/gcd-quad-factored-n1-eq-n1.aisp
+++ b/goals/gcd-quad-factored-n1-eq-n1.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-quad-factored-n1-eq-n1
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-quad-factored-n1-eq-n1.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-quad-factored-n1-eq-n1.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-quad-factored-n1-eq-n1.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.lean
   sha≜f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8
   aff≜-10
 }
diff --git a/goals/gcd-sq-n-sq-n-one.aisp b/goals/gcd-sq-n-sq-n-one.aisp
index 05f1549d6..ad5bfd5d1 100644
--- a/goals/gcd-sq-n-sq-n-one.aisp
+++ b/goals/gcd-sq-n-sq-n-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-sq-n-sq-n-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-sq-n-sq-n-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-sq-n-sq-n-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-sq-n-sq-n-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.lean
   sha≜ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0
   aff≜-10
 }
diff --git a/goals/gcd-three-pow-succ-three-pow-add-one.aisp b/goals/gcd-three-pow-succ-three-pow-add-one.aisp
index 99520019e..bc3842d20 100644
--- a/goals/gcd-three-pow-succ-three-pow-add-one.aisp
+++ b/goals/gcd-three-pow-succ-three-pow-add-one.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-three-pow-succ-three-pow-add-one
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-three-pow-succ-three-pow-add-one.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-three-pow-succ-three-pow-add-one.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-three-pow-succ-three-pow-add-one.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.lean
   sha≜85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866
   aff≜-10
 }
diff --git a/goals/gcd-threen-n7-dvd-twentyone.aisp b/goals/gcd-threen-n7-dvd-twentyone.aisp
index 46c92bded..9af8cc232 100644
--- a/goals/gcd-threen-n7-dvd-twentyone.aisp
+++ b/goals/gcd-threen-n7-dvd-twentyone.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-threen-n7-dvd-twentyone
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-threen-n7-dvd-twentyone.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-threen-n7-dvd-twentyone.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-threen-n7-dvd-twentyone.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.lean
   sha≜5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2
   aff≜-10
 }
diff --git a/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp b/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp
index aedd3b0a7..d36da2630 100644
--- a/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp
+++ b/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-two-pow-add-one-sub-one-dvd-two
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-two-pow-add-one-sub-one-dvd-two.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-two-pow-add-one-sub-one-dvd-two.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-two-pow-add-one-sub-one-dvd-two.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.lean
   sha≜136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a
   aff≜-10
 }
diff --git a/goals/gcd-twon-n5-dvd-ten.aisp b/goals/gcd-twon-n5-dvd-ten.aisp
index ae1c04616..eac93384f 100644
--- a/goals/gcd-twon-n5-dvd-ten.aisp
+++ b/goals/gcd-twon-n5-dvd-ten.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜gcd-twon-n5-dvd-ten
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/gcd-twon-n5-dvd-ten.md
+  src≜packages/unsorry-archive-0008/backlog/gcd-twon-n5-dvd-ten.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/gcd-twon-n5-dvd-ten.lean
+  lean≜packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.lean
   sha≜b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520
   aff≜-10
 }
diff --git a/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp b/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp
index 0f45f699e..9d4979678 100644
--- a/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp
+++ b/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜lucas-succ-add-lucas-pred-eq-five-mul-fib
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md
+  src≜packages/unsorry-archive-0008/backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean
+  lean≜packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean
   sha≜f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a
   aff≜-20
 }
diff --git a/goals/ninth-power-mod-nineteen-mem.aisp b/goals/ninth-power-mod-nineteen-mem.aisp
index d0624e82c..7d48a2b68 100644
--- a/goals/ninth-power-mod-nineteen-mem.aisp
+++ b/goals/ninth-power-mod-nineteen-mem.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜ninth-power-mod-nineteen-mem
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/ninth-power-mod-nineteen-mem.md
+  src≜packages/unsorry-archive-0008/backlog/ninth-power-mod-nineteen-mem.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/ninth-power-mod-nineteen-mem.lean
+  lean≜packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.lean
   sha≜d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a
   aff≜-10
 }
diff --git a/goals/pair-sum-sq-ge-three-abc-sum.aisp b/goals/pair-sum-sq-ge-three-abc-sum.aisp
index 667599c12..441fa8ba9 100644
--- a/goals/pair-sum-sq-ge-three-abc-sum.aisp
+++ b/goals/pair-sum-sq-ge-three-abc-sum.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pair-sum-sq-ge-three-abc-sum
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pair-sum-sq-ge-three-abc-sum.md
+  src≜packages/unsorry-archive-0008/backlog/pair-sum-sq-ge-three-abc-sum.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pair-sum-sq-ge-three-abc-sum.lean
+  lean≜packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.lean
   sha≜806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b
   aff≜-20
 }
diff --git a/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp b/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp
index f9e0bed12..440f91537 100644
--- a/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp
+++ b/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pairwise-product-sum-sq-ge-three-abc-sum
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pairwise-product-sum-sq-ge-three-abc-sum.md
+  src≜packages/unsorry-archive-0008/backlog/pairwise-product-sum-sq-ge-three-abc-sum.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pairwise-product-sum-sq-ge-three-abc-sum.lean
+  lean≜packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.lean
   sha≜20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f
   aff≜-20
 }
diff --git a/goals/pell-brahmagupta-composition-generic-d.aisp b/goals/pell-brahmagupta-composition-generic-d.aisp
index a48705299..6a39dad5a 100644
--- a/goals/pell-brahmagupta-composition-generic-d.aisp
+++ b/goals/pell-brahmagupta-composition-generic-d.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-brahmagupta-composition-generic-d
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-brahmagupta-composition-generic-d.md
+  src≜packages/unsorry-archive-0008/backlog/pell-brahmagupta-composition-generic-d.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-brahmagupta-composition-generic-d.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.lean
   sha≜5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b
   aff≜-10
 }
diff --git a/goals/pell-d10-fundamental-ladder-step-preserves.aisp b/goals/pell-d10-fundamental-ladder-step-preserves.aisp
index f14329639..085b1c110 100644
--- a/goals/pell-d10-fundamental-ladder-step-preserves.aisp
+++ b/goals/pell-d10-fundamental-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d10-fundamental-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d10-fundamental-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d10-fundamental-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d10-fundamental-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.lean
   sha≜f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874
   aff≜-10
 }
diff --git a/goals/pell-d11-ladder-step-preserves.aisp b/goals/pell-d11-ladder-step-preserves.aisp
index 30d854eaf..6b978adbe 100644
--- a/goals/pell-d11-ladder-step-preserves.aisp
+++ b/goals/pell-d11-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d11-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d11-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d11-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d11-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.lean
   sha≜963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0
   aff≜-10
 }
diff --git a/goals/pell-d12-ladder-step-preserves.aisp b/goals/pell-d12-ladder-step-preserves.aisp
index 6c030a746..0957a47fe 100644
--- a/goals/pell-d12-ladder-step-preserves.aisp
+++ b/goals/pell-d12-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d12-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d12-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d12-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d12-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.lean
   sha≜6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb
   aff≜-10
 }
diff --git a/goals/pell-d13-ladder-step-preserves.aisp b/goals/pell-d13-ladder-step-preserves.aisp
index bed852d65..bf3603444 100644
--- a/goals/pell-d13-ladder-step-preserves.aisp
+++ b/goals/pell-d13-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d13-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜3
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d13-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d13-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d13-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.lean
   sha≜b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd
   aff≜-10
 }
diff --git a/goals/pell-d14-ladder-step-preserves.aisp b/goals/pell-d14-ladder-step-preserves.aisp
index 268318b25..c54984a55 100644
--- a/goals/pell-d14-ladder-step-preserves.aisp
+++ b/goals/pell-d14-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d14-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d14-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d14-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d14-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.lean
   sha≜3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4
   aff≜-10
 }
diff --git a/goals/pell-d15-ladder-step-preserves.aisp b/goals/pell-d15-ladder-step-preserves.aisp
index f3a2184ef..769c14163 100644
--- a/goals/pell-d15-ladder-step-preserves.aisp
+++ b/goals/pell-d15-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d15-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d15-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d15-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d15-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.lean
   sha≜a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274
   aff≜-10
 }
diff --git a/goals/pell-d17-ladder-step-preserves.aisp b/goals/pell-d17-ladder-step-preserves.aisp
index 3938ed541..95bcd050d 100644
--- a/goals/pell-d17-ladder-step-preserves.aisp
+++ b/goals/pell-d17-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d17-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d17-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d17-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d17-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.lean
   sha≜f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f
   aff≜-10
 }
diff --git a/goals/pell-d18-ladder-step-preserves.aisp b/goals/pell-d18-ladder-step-preserves.aisp
index 8aca65661..4f15a1095 100644
--- a/goals/pell-d18-ladder-step-preserves.aisp
+++ b/goals/pell-d18-ladder-step-preserves.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d18-ladder-step-preserves
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d18-ladder-step-preserves.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d18-ladder-step-preserves.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d18-ladder-step-preserves.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.lean
   sha≜4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083
   aff≜-10
 }
diff --git a/goals/pell-d2-form-product-telescope-step.aisp b/goals/pell-d2-form-product-telescope-step.aisp
index 0fe1f9875..b533b11e4 100644
--- a/goals/pell-d2-form-product-telescope-step.aisp
+++ b/goals/pell-d2-form-product-telescope-step.aisp
@@ -3,17 +3,17 @@
 ⟦Ω:Goal⟧{
   id≜pell-d2-form-product-telescope-step
   phase≜prove
-  status≜proved
+  status≜archived
   difficulty≜2
 }
 ⟦Σ:Source⟧{
-  src≜backlog/pell-d2-form-product-telescope-step.md
+  src≜packages/unsorry-archive-0008/backlog/pell-d2-form-product-telescope-step.md
 }
 ⟦Γ:Deps⟧{
   deps≜⟨⟩
 }
 ⟦Λ:Artifact⟧{
-  lean≜goals/pell-d2-form-product-telescope-step.lean
+  lean≜packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.lean
   sha≜70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd
   aff≜-10
 }
diff --git a/packages/unsorry-archive-0008/archive-manifest.json b/packages/unsorry-archive-0008/archive-manifest.json
new file mode 100644
index 000000000..d37539777
--- /dev/null
+++ b/packages/unsorry-archive-0008/archive-manifest.json
@@ -0,0 +1,179 @@
+{
+  "block_id": "unsorry-archive-0008",
+  "target_size": 40,
+  "proof_count": 40,
+  "status": "frozen",
+  "source_commit": "702e5645059f52ed95ea17158861cc0a6d766577",
+  "validation_commit": null,
+  "pins": {
+    "lean_toolchain": "leanprover/lean4:v4.30.0",
+    "mathlib": "v4.30.0"
+  },
+  "notes": [
+    "ADR-041 proof archive block 0008.",
+    "Whole decomposition trees + standalone proved goals only (invariant A).",
+    "Active goal records remain as archived metadata pointing at this package."
+  ],
+  "goals": [
+    {
+      "goal": "gcd-5n3-7n4-eq-one",
+      "module": "Unsorry.Gcd5n37n4EqOne"
+    },
+    {
+      "goal": "gcd-6n5-4n3-eq-one",
+      "module": "Unsorry.Gcd6n54n3EqOne"
+    },
+    {
+      "goal": "gcd-6n5-6n11-eq-one",
+      "module": "Unsorry.Gcd6n56n11EqOne"
+    },
+    {
+      "goal": "gcd-factorial-succ-eq-factorial",
+      "module": "Unsorry.GcdFactorialSuccEqFactorial"
+    },
+    {
+      "goal": "gcd-fib-add-two-eq-gcd-fib-succ",
+      "module": "Unsorry.GcdFibAddTwoEqGcdFibSucc"
+    },
+    {
+      "goal": "gcd-n-add-six-dvd-six",
+      "module": "Unsorry.GcdNAddSixDvdSix"
+    },
+    {
+      "goal": "gcd-n-factorial-succ-eq-one",
+      "module": "Unsorry.GcdNFactorialSuccEqOne"
+    },
+    {
+      "goal": "gcd-n1-n7-dvd-six",
+      "module": "Unsorry.GcdN1N7DvdSix"
+    },
+    {
+      "goal": "gcd-n2-2n5-eq-one",
+      "module": "Unsorry.GcdN22n5EqOne"
+    },
+    {
+      "goal": "gcd-n2-n4-dvd-two",
+      "module": "Unsorry.GcdN2N4DvdTwo"
+    },
+    {
+      "goal": "gcd-n2-n6-dvd-four",
+      "module": "Unsorry.GcdN2N6DvdFour"
+    },
+    {
+      "goal": "gcd-n2-n8-dvd-six",
+      "module": "Unsorry.GcdN2N8DvdSix"
+    },
+    {
+      "goal": "gcd-n2p1-n2p3-dvd-two",
+      "module": "Unsorry.GcdN2p1N2p3DvdTwo"
+    },
+    {
+      "goal": "gcd-n3-2n7-eq-one",
+      "module": "Unsorry.GcdN32n7EqOne"
+    },
+    {
+      "goal": "gcd-n3p1-np1-eq-np1",
+      "module": "Unsorry.GcdN3p1Np1EqNp1"
+    },
+    {
+      "goal": "gcd-n4p1-n2p1-dvd-two",
+      "module": "Unsorry.GcdN4p1N2p1DvdTwo"
+    },
+    {
+      "goal": "gcd-np1-2np1-eq-one",
+      "module": "Unsorry.GcdNp12np1EqOne"
+    },
+    {
+      "goal": "gcd-np1-n2p1-dvd-two",
+      "module": "Unsorry.GcdNp1N2p1DvdTwo"
+    },
+    {
+      "goal": "gcd-nsq1-n1-dvd-two",
+      "module": "Unsorry.GcdNsq1N1DvdTwo"
+    },
+    {
+      "goal": "gcd-nsq1-nsq3-dvd-two",
+      "module": "Unsorry.GcdNsq1Nsq3DvdTwo"
+    },
+    {
+      "goal": "gcd-quad-factored-n1-eq-n1",
+      "module": "Unsorry.GcdQuadFactoredN1EqN1"
+    },
+    {
+      "goal": "gcd-sq-n-sq-n-one",
+      "module": "Unsorry.GcdSqNSqNOne"
+    },
+    {
+      "goal": "gcd-three-pow-succ-three-pow-add-one",
+      "module": "Unsorry.GcdThreePowSuccThreePowAddOne"
+    },
+    {
+      "goal": "gcd-threen-n7-dvd-twentyone",
+      "module": "Unsorry.GcdThreenN7DvdTwentyone"
+    },
+    {
+      "goal": "gcd-two-pow-add-one-sub-one-dvd-two",
+      "module": "Unsorry.GcdTwoPowAddOneSubOneDvdTwo"
+    },
+    {
+      "goal": "gcd-twon-n5-dvd-ten",
+      "module": "Unsorry.GcdTwonN5DvdTen"
+    },
+    {
+      "goal": "lucas-succ-add-lucas-pred-eq-five-mul-fib",
+      "module": "Unsorry.LucasSuccAddLucasPredEqFiveMulFib"
+    },
+    {
+      "goal": "ninth-power-mod-nineteen-mem",
+      "module": "Unsorry.NinthPowerModNineteenMem"
+    },
+    {
+      "goal": "pair-sum-sq-ge-three-abc-sum",
+      "module": "Unsorry.PairSumSqGeThreeAbcSum"
+    },
+    {
+      "goal": "pairwise-product-sum-sq-ge-three-abc-sum",
+      "module": "Unsorry.PairwiseProductSumSqGeThreeAbcSum"
+    },
+    {
+      "goal": "pell-brahmagupta-composition-generic-d",
+      "module": "Unsorry.PellBrahmaguptaCompositionGenericD"
+    },
+    {
+      "goal": "pell-d10-fundamental-ladder-step-preserves",
+      "module": "Unsorry.PellD10FundamentalLadderStepPreserves"
+    },
+    {
+      "goal": "pell-d11-ladder-step-preserves",
+      "module": "Unsorry.PellD11LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d12-ladder-step-preserves",
+      "module": "Unsorry.PellD12LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d13-ladder-step-preserves",
+      "module": "Unsorry.PellD13LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d14-ladder-step-preserves",
+      "module": "Unsorry.PellD14LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d15-ladder-step-preserves",
+      "module": "Unsorry.PellD15LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d17-ladder-step-preserves",
+      "module": "Unsorry.PellD17LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d18-ladder-step-preserves",
+      "module": "Unsorry.PellD18LadderStepPreserves"
+    },
+    {
+      "goal": "pell-d2-form-product-telescope-step",
+      "module": "Unsorry.PellD2FormProductTelescopeStep"
+    }
+  ]
+}
diff --git a/backlog/gcd-5n3-7n4-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-5n3-7n4-eq-one.md
similarity index 100%
rename from backlog/gcd-5n3-7n4-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-5n3-7n4-eq-one.md
diff --git a/backlog/gcd-6n5-4n3-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-6n5-4n3-eq-one.md
similarity index 100%
rename from backlog/gcd-6n5-4n3-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-6n5-4n3-eq-one.md
diff --git a/backlog/gcd-6n5-6n11-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-6n5-6n11-eq-one.md
similarity index 100%
rename from backlog/gcd-6n5-6n11-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-6n5-6n11-eq-one.md
diff --git a/backlog/gcd-factorial-succ-eq-factorial.md b/packages/unsorry-archive-0008/backlog/gcd-factorial-succ-eq-factorial.md
similarity index 100%
rename from backlog/gcd-factorial-succ-eq-factorial.md
rename to packages/unsorry-archive-0008/backlog/gcd-factorial-succ-eq-factorial.md
diff --git a/backlog/gcd-fib-add-two-eq-gcd-fib-succ.md b/packages/unsorry-archive-0008/backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
similarity index 100%
rename from backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
rename to packages/unsorry-archive-0008/backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
diff --git a/backlog/gcd-n-add-six-dvd-six.md b/packages/unsorry-archive-0008/backlog/gcd-n-add-six-dvd-six.md
similarity index 100%
rename from backlog/gcd-n-add-six-dvd-six.md
rename to packages/unsorry-archive-0008/backlog/gcd-n-add-six-dvd-six.md
diff --git a/backlog/gcd-n-factorial-succ-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-n-factorial-succ-eq-one.md
similarity index 100%
rename from backlog/gcd-n-factorial-succ-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-n-factorial-succ-eq-one.md
diff --git a/backlog/gcd-n1-n7-dvd-six.md b/packages/unsorry-archive-0008/backlog/gcd-n1-n7-dvd-six.md
similarity index 100%
rename from backlog/gcd-n1-n7-dvd-six.md
rename to packages/unsorry-archive-0008/backlog/gcd-n1-n7-dvd-six.md
diff --git a/backlog/gcd-n2-2n5-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-n2-2n5-eq-one.md
similarity index 100%
rename from backlog/gcd-n2-2n5-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-n2-2n5-eq-one.md
diff --git a/backlog/gcd-n2-n4-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-n2-n4-dvd-two.md
similarity index 100%
rename from backlog/gcd-n2-n4-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-n2-n4-dvd-two.md
diff --git a/backlog/gcd-n2-n6-dvd-four.md b/packages/unsorry-archive-0008/backlog/gcd-n2-n6-dvd-four.md
similarity index 100%
rename from backlog/gcd-n2-n6-dvd-four.md
rename to packages/unsorry-archive-0008/backlog/gcd-n2-n6-dvd-four.md
diff --git a/backlog/gcd-n2-n8-dvd-six.md b/packages/unsorry-archive-0008/backlog/gcd-n2-n8-dvd-six.md
similarity index 100%
rename from backlog/gcd-n2-n8-dvd-six.md
rename to packages/unsorry-archive-0008/backlog/gcd-n2-n8-dvd-six.md
diff --git a/backlog/gcd-n2p1-n2p3-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-n2p1-n2p3-dvd-two.md
similarity index 100%
rename from backlog/gcd-n2p1-n2p3-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-n2p1-n2p3-dvd-two.md
diff --git a/backlog/gcd-n3-2n7-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-n3-2n7-eq-one.md
similarity index 100%
rename from backlog/gcd-n3-2n7-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-n3-2n7-eq-one.md
diff --git a/backlog/gcd-n3p1-np1-eq-np1.md b/packages/unsorry-archive-0008/backlog/gcd-n3p1-np1-eq-np1.md
similarity index 100%
rename from backlog/gcd-n3p1-np1-eq-np1.md
rename to packages/unsorry-archive-0008/backlog/gcd-n3p1-np1-eq-np1.md
diff --git a/backlog/gcd-n4p1-n2p1-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-n4p1-n2p1-dvd-two.md
similarity index 100%
rename from backlog/gcd-n4p1-n2p1-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-n4p1-n2p1-dvd-two.md
diff --git a/backlog/gcd-np1-2np1-eq-one.md b/packages/unsorry-archive-0008/backlog/gcd-np1-2np1-eq-one.md
similarity index 100%
rename from backlog/gcd-np1-2np1-eq-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-np1-2np1-eq-one.md
diff --git a/backlog/gcd-np1-n2p1-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-np1-n2p1-dvd-two.md
similarity index 100%
rename from backlog/gcd-np1-n2p1-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-np1-n2p1-dvd-two.md
diff --git a/backlog/gcd-nsq1-n1-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-nsq1-n1-dvd-two.md
similarity index 100%
rename from backlog/gcd-nsq1-n1-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-nsq1-n1-dvd-two.md
diff --git a/backlog/gcd-nsq1-nsq3-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-nsq1-nsq3-dvd-two.md
similarity index 100%
rename from backlog/gcd-nsq1-nsq3-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-nsq1-nsq3-dvd-two.md
diff --git a/backlog/gcd-quad-factored-n1-eq-n1.md b/packages/unsorry-archive-0008/backlog/gcd-quad-factored-n1-eq-n1.md
similarity index 100%
rename from backlog/gcd-quad-factored-n1-eq-n1.md
rename to packages/unsorry-archive-0008/backlog/gcd-quad-factored-n1-eq-n1.md
diff --git a/backlog/gcd-sq-n-sq-n-one.md b/packages/unsorry-archive-0008/backlog/gcd-sq-n-sq-n-one.md
similarity index 100%
rename from backlog/gcd-sq-n-sq-n-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-sq-n-sq-n-one.md
diff --git a/backlog/gcd-three-pow-succ-three-pow-add-one.md b/packages/unsorry-archive-0008/backlog/gcd-three-pow-succ-three-pow-add-one.md
similarity index 100%
rename from backlog/gcd-three-pow-succ-three-pow-add-one.md
rename to packages/unsorry-archive-0008/backlog/gcd-three-pow-succ-three-pow-add-one.md
diff --git a/backlog/gcd-threen-n7-dvd-twentyone.md b/packages/unsorry-archive-0008/backlog/gcd-threen-n7-dvd-twentyone.md
similarity index 100%
rename from backlog/gcd-threen-n7-dvd-twentyone.md
rename to packages/unsorry-archive-0008/backlog/gcd-threen-n7-dvd-twentyone.md
diff --git a/backlog/gcd-two-pow-add-one-sub-one-dvd-two.md b/packages/unsorry-archive-0008/backlog/gcd-two-pow-add-one-sub-one-dvd-two.md
similarity index 100%
rename from backlog/gcd-two-pow-add-one-sub-one-dvd-two.md
rename to packages/unsorry-archive-0008/backlog/gcd-two-pow-add-one-sub-one-dvd-two.md
diff --git a/backlog/gcd-twon-n5-dvd-ten.md b/packages/unsorry-archive-0008/backlog/gcd-twon-n5-dvd-ten.md
similarity index 100%
rename from backlog/gcd-twon-n5-dvd-ten.md
rename to packages/unsorry-archive-0008/backlog/gcd-twon-n5-dvd-ten.md
diff --git a/backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md b/packages/unsorry-archive-0008/backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md
similarity index 100%
rename from backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md
rename to packages/unsorry-archive-0008/backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md
diff --git a/backlog/ninth-power-mod-nineteen-mem.md b/packages/unsorry-archive-0008/backlog/ninth-power-mod-nineteen-mem.md
similarity index 100%
rename from backlog/ninth-power-mod-nineteen-mem.md
rename to packages/unsorry-archive-0008/backlog/ninth-power-mod-nineteen-mem.md
diff --git a/backlog/pair-sum-sq-ge-three-abc-sum.md b/packages/unsorry-archive-0008/backlog/pair-sum-sq-ge-three-abc-sum.md
similarity index 100%
rename from backlog/pair-sum-sq-ge-three-abc-sum.md
rename to packages/unsorry-archive-0008/backlog/pair-sum-sq-ge-three-abc-sum.md
diff --git a/backlog/pairwise-product-sum-sq-ge-three-abc-sum.md b/packages/unsorry-archive-0008/backlog/pairwise-product-sum-sq-ge-three-abc-sum.md
similarity index 100%
rename from backlog/pairwise-product-sum-sq-ge-three-abc-sum.md
rename to packages/unsorry-archive-0008/backlog/pairwise-product-sum-sq-ge-three-abc-sum.md
diff --git a/backlog/pell-brahmagupta-composition-generic-d.md b/packages/unsorry-archive-0008/backlog/pell-brahmagupta-composition-generic-d.md
similarity index 100%
rename from backlog/pell-brahmagupta-composition-generic-d.md
rename to packages/unsorry-archive-0008/backlog/pell-brahmagupta-composition-generic-d.md
diff --git a/backlog/pell-d10-fundamental-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d10-fundamental-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d10-fundamental-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d10-fundamental-ladder-step-preserves.md
diff --git a/backlog/pell-d11-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d11-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d11-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d11-ladder-step-preserves.md
diff --git a/backlog/pell-d12-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d12-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d12-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d12-ladder-step-preserves.md
diff --git a/backlog/pell-d13-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d13-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d13-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d13-ladder-step-preserves.md
diff --git a/backlog/pell-d14-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d14-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d14-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d14-ladder-step-preserves.md
diff --git a/backlog/pell-d15-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d15-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d15-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d15-ladder-step-preserves.md
diff --git a/backlog/pell-d17-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d17-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d17-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d17-ladder-step-preserves.md
diff --git a/backlog/pell-d18-ladder-step-preserves.md b/packages/unsorry-archive-0008/backlog/pell-d18-ladder-step-preserves.md
similarity index 100%
rename from backlog/pell-d18-ladder-step-preserves.md
rename to packages/unsorry-archive-0008/backlog/pell-d18-ladder-step-preserves.md
diff --git a/backlog/pell-d2-form-product-telescope-step.md b/packages/unsorry-archive-0008/backlog/pell-d2-form-product-telescope-step.md
similarity index 100%
rename from backlog/pell-d2-form-product-telescope-step.md
rename to packages/unsorry-archive-0008/backlog/pell-d2-form-product-telescope-step.md
diff --git a/packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.aisp
new file mode 100644
index 000000000..68bc9bee9
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-5n3-7n4-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-5n3-7n4-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-5n3-7n4-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-5n3-7n4-eq-one.lean
+  sha≜a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-5n3-7n4-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.lean
similarity index 100%
rename from goals/gcd-5n3-7n4-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-5n3-7n4-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.aisp
new file mode 100644
index 000000000..ac6097a34
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-6n5-4n3-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-6n5-4n3-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-6n5-4n3-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-6n5-4n3-eq-one.lean
+  sha≜da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-6n5-4n3-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.lean
similarity index 100%
rename from goals/gcd-6n5-4n3-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-6n5-4n3-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.aisp
new file mode 100644
index 000000000..7a163fc1f
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-6n5-6n11-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-6n5-6n11-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-6n5-6n11-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-6n5-6n11-eq-one.lean
+  sha≜058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-6n5-6n11-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.lean
similarity index 100%
rename from goals/gcd-6n5-6n11-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-6n5-6n11-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.aisp b/packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.aisp
new file mode 100644
index 000000000..66b25adf3
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-factorial-succ-eq-factorial@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-factorial-succ-eq-factorial
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-factorial-succ-eq-factorial.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-factorial-succ-eq-factorial.lean
+  sha≜2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-factorial-succ-eq-factorial.lean b/packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.lean
similarity index 100%
rename from goals/gcd-factorial-succ-eq-factorial.lean
rename to packages/unsorry-archive-0008/goals/gcd-factorial-succ-eq-factorial.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp b/packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
new file mode 100644
index 000000000..df67e7d69
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-fib-add-two-eq-gcd-fib-succ@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-fib-add-two-eq-gcd-fib-succ
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-fib-add-two-eq-gcd-fib-succ.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
+  sha≜6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-fib-add-two-eq-gcd-fib-succ.lean b/packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
similarity index 100%
rename from goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
rename to packages/unsorry-archive-0008/goals/gcd-fib-add-two-eq-gcd-fib-succ.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.aisp b/packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.aisp
new file mode 100644
index 000000000..9be7228d9
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n-add-six-dvd-six@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n-add-six-dvd-six
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n-add-six-dvd-six.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n-add-six-dvd-six.lean
+  sha≜4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n-add-six-dvd-six.lean b/packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.lean
similarity index 100%
rename from goals/gcd-n-add-six-dvd-six.lean
rename to packages/unsorry-archive-0008/goals/gcd-n-add-six-dvd-six.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.aisp
new file mode 100644
index 000000000..07be8b28f
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n-factorial-succ-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n-factorial-succ-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n-factorial-succ-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n-factorial-succ-eq-one.lean
+  sha≜e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n-factorial-succ-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.lean
similarity index 100%
rename from goals/gcd-n-factorial-succ-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-n-factorial-succ-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.aisp b/packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.aisp
new file mode 100644
index 000000000..977cbcc94
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n1-n7-dvd-six@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n1-n7-dvd-six
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n1-n7-dvd-six.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n1-n7-dvd-six.lean
+  sha≜2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n1-n7-dvd-six.lean b/packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.lean
similarity index 100%
rename from goals/gcd-n1-n7-dvd-six.lean
rename to packages/unsorry-archive-0008/goals/gcd-n1-n7-dvd-six.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.aisp
new file mode 100644
index 000000000..f7f511ae7
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n2-2n5-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n2-2n5-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n2-2n5-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n2-2n5-eq-one.lean
+  sha≜794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n2-2n5-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.lean
similarity index 100%
rename from goals/gcd-n2-2n5-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-n2-2n5-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.aisp
new file mode 100644
index 000000000..2caed74f0
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n2-n4-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n2-n4-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n2-n4-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n2-n4-dvd-two.lean
+  sha≜77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n2-n4-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.lean
similarity index 100%
rename from goals/gcd-n2-n4-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-n2-n4-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.aisp b/packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.aisp
new file mode 100644
index 000000000..aa938cf60
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n2-n6-dvd-four@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n2-n6-dvd-four
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n2-n6-dvd-four.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n2-n6-dvd-four.lean
+  sha≜1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n2-n6-dvd-four.lean b/packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.lean
similarity index 100%
rename from goals/gcd-n2-n6-dvd-four.lean
rename to packages/unsorry-archive-0008/goals/gcd-n2-n6-dvd-four.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.aisp b/packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.aisp
new file mode 100644
index 000000000..1c73e283a
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n2-n8-dvd-six@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n2-n8-dvd-six
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n2-n8-dvd-six.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n2-n8-dvd-six.lean
+  sha≜75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n2-n8-dvd-six.lean b/packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.lean
similarity index 100%
rename from goals/gcd-n2-n8-dvd-six.lean
rename to packages/unsorry-archive-0008/goals/gcd-n2-n8-dvd-six.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.aisp
new file mode 100644
index 000000000..26bc3c0fa
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n2p1-n2p3-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n2p1-n2p3-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n2p1-n2p3-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n2p1-n2p3-dvd-two.lean
+  sha≜8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n2p1-n2p3-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.lean
similarity index 100%
rename from goals/gcd-n2p1-n2p3-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-n2p1-n2p3-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.aisp
new file mode 100644
index 000000000..7eb69e98a
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n3-2n7-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n3-2n7-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n3-2n7-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n3-2n7-eq-one.lean
+  sha≜3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n3-2n7-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.lean
similarity index 100%
rename from goals/gcd-n3-2n7-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-n3-2n7-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.aisp b/packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.aisp
new file mode 100644
index 000000000..f87c0ce60
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n3p1-np1-eq-np1@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n3p1-np1-eq-np1
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n3p1-np1-eq-np1.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n3p1-np1-eq-np1.lean
+  sha≜5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n3p1-np1-eq-np1.lean b/packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.lean
similarity index 100%
rename from goals/gcd-n3p1-np1-eq-np1.lean
rename to packages/unsorry-archive-0008/goals/gcd-n3p1-np1-eq-np1.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.aisp
new file mode 100644
index 000000000..c0b15fd80
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-n4p1-n2p1-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-n4p1-n2p1-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-n4p1-n2p1-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-n4p1-n2p1-dvd-two.lean
+  sha≜a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-n4p1-n2p1-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.lean
similarity index 100%
rename from goals/gcd-n4p1-n2p1-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-n4p1-n2p1-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.aisp b/packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.aisp
new file mode 100644
index 000000000..8a88d301c
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-np1-2np1-eq-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-np1-2np1-eq-one
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-np1-2np1-eq-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-np1-2np1-eq-one.lean
+  sha≜ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-np1-2np1-eq-one.lean b/packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.lean
similarity index 100%
rename from goals/gcd-np1-2np1-eq-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-np1-2np1-eq-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.aisp
new file mode 100644
index 000000000..4fe1acd93
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-np1-n2p1-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-np1-n2p1-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-np1-n2p1-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-np1-n2p1-dvd-two.lean
+  sha≜410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-np1-n2p1-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.lean
similarity index 100%
rename from goals/gcd-np1-n2p1-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-np1-n2p1-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.aisp
new file mode 100644
index 000000000..edbac15c7
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-nsq1-n1-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-nsq1-n1-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-nsq1-n1-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-nsq1-n1-dvd-two.lean
+  sha≜43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-nsq1-n1-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.lean
similarity index 100%
rename from goals/gcd-nsq1-n1-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-nsq1-n1-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.aisp
new file mode 100644
index 000000000..a87852b27
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-nsq1-nsq3-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-nsq1-nsq3-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-nsq1-nsq3-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-nsq1-nsq3-dvd-two.lean
+  sha≜ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216
+  aff≜-9
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-nsq1-nsq3-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.lean
similarity index 100%
rename from goals/gcd-nsq1-nsq3-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-nsq1-nsq3-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.aisp b/packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.aisp
new file mode 100644
index 000000000..138763e06
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-quad-factored-n1-eq-n1@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-quad-factored-n1-eq-n1
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-quad-factored-n1-eq-n1.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-quad-factored-n1-eq-n1.lean
+  sha≜f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-quad-factored-n1-eq-n1.lean b/packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.lean
similarity index 100%
rename from goals/gcd-quad-factored-n1-eq-n1.lean
rename to packages/unsorry-archive-0008/goals/gcd-quad-factored-n1-eq-n1.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.aisp b/packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.aisp
new file mode 100644
index 000000000..05f1549d6
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-sq-n-sq-n-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-sq-n-sq-n-one
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-sq-n-sq-n-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-sq-n-sq-n-one.lean
+  sha≜ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-sq-n-sq-n-one.lean b/packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.lean
similarity index 100%
rename from goals/gcd-sq-n-sq-n-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-sq-n-sq-n-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.aisp b/packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.aisp
new file mode 100644
index 000000000..99520019e
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-three-pow-succ-three-pow-add-one@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-three-pow-succ-three-pow-add-one
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-three-pow-succ-three-pow-add-one.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-three-pow-succ-three-pow-add-one.lean
+  sha≜85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-three-pow-succ-three-pow-add-one.lean b/packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.lean
similarity index 100%
rename from goals/gcd-three-pow-succ-three-pow-add-one.lean
rename to packages/unsorry-archive-0008/goals/gcd-three-pow-succ-three-pow-add-one.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.aisp b/packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.aisp
new file mode 100644
index 000000000..46c92bded
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-threen-n7-dvd-twentyone@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-threen-n7-dvd-twentyone
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-threen-n7-dvd-twentyone.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-threen-n7-dvd-twentyone.lean
+  sha≜5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-threen-n7-dvd-twentyone.lean b/packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.lean
similarity index 100%
rename from goals/gcd-threen-n7-dvd-twentyone.lean
rename to packages/unsorry-archive-0008/goals/gcd-threen-n7-dvd-twentyone.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp b/packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp
new file mode 100644
index 000000000..aedd3b0a7
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-two-pow-add-one-sub-one-dvd-two@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-two-pow-add-one-sub-one-dvd-two
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-two-pow-add-one-sub-one-dvd-two.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-two-pow-add-one-sub-one-dvd-two.lean
+  sha≜136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-two-pow-add-one-sub-one-dvd-two.lean b/packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.lean
similarity index 100%
rename from goals/gcd-two-pow-add-one-sub-one-dvd-two.lean
rename to packages/unsorry-archive-0008/goals/gcd-two-pow-add-one-sub-one-dvd-two.lean
diff --git a/packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.aisp b/packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.aisp
new file mode 100644
index 000000000..ae1c04616
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.gcd-twon-n5-dvd-ten@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜gcd-twon-n5-dvd-ten
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/gcd-twon-n5-dvd-ten.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/gcd-twon-n5-dvd-ten.lean
+  sha≜b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/gcd-twon-n5-dvd-ten.lean b/packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.lean
similarity index 100%
rename from goals/gcd-twon-n5-dvd-ten.lean
rename to packages/unsorry-archive-0008/goals/gcd-twon-n5-dvd-ten.lean
diff --git a/packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp b/packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp
new file mode 100644
index 000000000..0f45f699e
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.lucas-succ-add-lucas-pred-eq-five-mul-fib@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜lucas-succ-add-lucas-pred-eq-five-mul-fib
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/lucas-succ-add-lucas-pred-eq-five-mul-fib.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean
+  sha≜f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a
+  aff≜-20
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean b/packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean
similarity index 100%
rename from goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean
rename to packages/unsorry-archive-0008/goals/lucas-succ-add-lucas-pred-eq-five-mul-fib.lean
diff --git a/packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.aisp b/packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.aisp
new file mode 100644
index 000000000..d0624e82c
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.ninth-power-mod-nineteen-mem@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜ninth-power-mod-nineteen-mem
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/ninth-power-mod-nineteen-mem.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/ninth-power-mod-nineteen-mem.lean
+  sha≜d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/ninth-power-mod-nineteen-mem.lean b/packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.lean
similarity index 100%
rename from goals/ninth-power-mod-nineteen-mem.lean
rename to packages/unsorry-archive-0008/goals/ninth-power-mod-nineteen-mem.lean
diff --git a/packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.aisp b/packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.aisp
new file mode 100644
index 000000000..667599c12
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pair-sum-sq-ge-three-abc-sum@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pair-sum-sq-ge-three-abc-sum
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pair-sum-sq-ge-three-abc-sum.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pair-sum-sq-ge-three-abc-sum.lean
+  sha≜806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b
+  aff≜-20
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pair-sum-sq-ge-three-abc-sum.lean b/packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.lean
similarity index 100%
rename from goals/pair-sum-sq-ge-three-abc-sum.lean
rename to packages/unsorry-archive-0008/goals/pair-sum-sq-ge-three-abc-sum.lean
diff --git a/packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp b/packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp
new file mode 100644
index 000000000..f9e0bed12
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pairwise-product-sum-sq-ge-three-abc-sum@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pairwise-product-sum-sq-ge-three-abc-sum
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/pairwise-product-sum-sq-ge-three-abc-sum.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pairwise-product-sum-sq-ge-three-abc-sum.lean
+  sha≜20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f
+  aff≜-20
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pairwise-product-sum-sq-ge-three-abc-sum.lean b/packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.lean
similarity index 100%
rename from goals/pairwise-product-sum-sq-ge-three-abc-sum.lean
rename to packages/unsorry-archive-0008/goals/pairwise-product-sum-sq-ge-three-abc-sum.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.aisp b/packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.aisp
new file mode 100644
index 000000000..a48705299
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-brahmagupta-composition-generic-d@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-brahmagupta-composition-generic-d
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-brahmagupta-composition-generic-d.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-brahmagupta-composition-generic-d.lean
+  sha≜5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-brahmagupta-composition-generic-d.lean b/packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.lean
similarity index 100%
rename from goals/pell-brahmagupta-composition-generic-d.lean
rename to packages/unsorry-archive-0008/goals/pell-brahmagupta-composition-generic-d.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.aisp
new file mode 100644
index 000000000..f14329639
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d10-fundamental-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d10-fundamental-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d10-fundamental-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d10-fundamental-ladder-step-preserves.lean
+  sha≜f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d10-fundamental-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d10-fundamental-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d10-fundamental-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.aisp
new file mode 100644
index 000000000..30d854eaf
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d11-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d11-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d11-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d11-ladder-step-preserves.lean
+  sha≜963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d11-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d11-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d11-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.aisp
new file mode 100644
index 000000000..6c030a746
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d12-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d12-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d12-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d12-ladder-step-preserves.lean
+  sha≜6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d12-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d12-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d12-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.aisp
new file mode 100644
index 000000000..bed852d65
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d13-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d13-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜3
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d13-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d13-ladder-step-preserves.lean
+  sha≜b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d13-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d13-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d13-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.aisp
new file mode 100644
index 000000000..268318b25
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d14-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d14-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d14-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d14-ladder-step-preserves.lean
+  sha≜3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d14-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d14-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d14-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.aisp
new file mode 100644
index 000000000..f3a2184ef
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d15-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d15-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d15-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d15-ladder-step-preserves.lean
+  sha≜a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d15-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d15-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d15-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.aisp
new file mode 100644
index 000000000..3938ed541
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d17-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d17-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d17-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d17-ladder-step-preserves.lean
+  sha≜f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d17-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d17-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d17-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.aisp b/packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.aisp
new file mode 100644
index 000000000..8aca65661
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d18-ladder-step-preserves@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d18-ladder-step-preserves
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d18-ladder-step-preserves.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d18-ladder-step-preserves.lean
+  sha≜4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d18-ladder-step-preserves.lean b/packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.lean
similarity index 100%
rename from goals/pell-d18-ladder-step-preserves.lean
rename to packages/unsorry-archive-0008/goals/pell-d18-ladder-step-preserves.lean
diff --git a/packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.aisp b/packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.aisp
new file mode 100644
index 000000000..0fe1f9875
--- /dev/null
+++ b/packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.aisp
@@ -0,0 +1,20 @@
+𝔸5.1.goal.pell-d2-form-product-telescope-step@2026-06-15
+γ≔unsorry.goal
+⟦Ω:Goal⟧{
+  id≜pell-d2-form-product-telescope-step
+  phase≜prove
+  status≜proved
+  difficulty≜2
+}
+⟦Σ:Source⟧{
+  src≜backlog/pell-d2-form-product-telescope-step.md
+}
+⟦Γ:Deps⟧{
+  deps≜⟨⟩
+}
+⟦Λ:Artifact⟧{
+  lean≜goals/pell-d2-form-product-telescope-step.lean
+  sha≜70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd
+  aff≜-10
+}
+⟦Ε⟧⟨δ≜0.60;τ≜◊⁺⟩
diff --git a/goals/pell-d2-form-product-telescope-step.lean b/packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.lean
similarity index 100%
rename from goals/pell-d2-form-product-telescope-step.lean
rename to packages/unsorry-archive-0008/goals/pell-d2-form-product-telescope-step.lean
diff --git a/packages/unsorry-archive-0008/lake-manifest.json b/packages/unsorry-archive-0008/lake-manifest.json
new file mode 100644
index 000000000..3292fed9a
--- /dev/null
+++ b/packages/unsorry-archive-0008/lake-manifest.json
@@ -0,0 +1,96 @@
+{"version": "1.2.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5ea00351c28e24afc9f0f84379aa41082b1188f",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "515cf9d0c00ece5e661f6de4326a53dedc1e8ea1",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a84b3e2475d5c5ab979567b1ad8aea21b764bcf8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.99",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "a6e6c34c4ef182f83b219a3a5a385f51f44bdc4c",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "32dc18cde3684679f3c003de608743b57498c56f",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "6b907cf12b2e445ccb7c24bc208ef04a1f39e84c",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "unsorryArchive0001",
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/packages/unsorry-archive-0008/lakefile.toml b/packages/unsorry-archive-0008/lakefile.toml
new file mode 100644
index 000000000..14c1dff6b
--- /dev/null
+++ b/packages/unsorry-archive-0008/lakefile.toml
@@ -0,0 +1,19 @@
+name = "unsorryArchive0008"
+version = "0.1.0"
+keywords = ["math", "archive", "unsorry"]
+defaultTargets = ["UnsorryArchive0008"]
+
+[leanOptions]
+pp.unicode.fun = true
+autoImplicit = false
+relaxedAutoImplicit = false
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "v4.30.0"
+
+[[lean_lib]]
+name = "UnsorryArchive0008"
+srcDir = "library"
+globs = ["Unsorry.+"]
diff --git a/packages/unsorry-archive-0008/lean-toolchain b/packages/unsorry-archive-0008/lean-toolchain
new file mode 100644
index 000000000..af9e5d339
--- /dev/null
+++ b/packages/unsorry-archive-0008/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.30.0
diff --git a/library/Unsorry/Gcd5n37n4EqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/Gcd5n37n4EqOne.lean
similarity index 100%
rename from library/Unsorry/Gcd5n37n4EqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/Gcd5n37n4EqOne.lean
diff --git a/library/Unsorry/Gcd6n54n3EqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/Gcd6n54n3EqOne.lean
similarity index 100%
rename from library/Unsorry/Gcd6n54n3EqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/Gcd6n54n3EqOne.lean
diff --git a/library/Unsorry/Gcd6n56n11EqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/Gcd6n56n11EqOne.lean
similarity index 100%
rename from library/Unsorry/Gcd6n56n11EqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/Gcd6n56n11EqOne.lean
diff --git a/library/Unsorry/GcdFactorialSuccEqFactorial.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdFactorialSuccEqFactorial.lean
similarity index 100%
rename from library/Unsorry/GcdFactorialSuccEqFactorial.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdFactorialSuccEqFactorial.lean
diff --git a/library/Unsorry/GcdFibAddTwoEqGcdFibSucc.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdFibAddTwoEqGcdFibSucc.lean
similarity index 100%
rename from library/Unsorry/GcdFibAddTwoEqGcdFibSucc.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdFibAddTwoEqGcdFibSucc.lean
diff --git a/library/Unsorry/GcdN1N7DvdSix.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN1N7DvdSix.lean
similarity index 100%
rename from library/Unsorry/GcdN1N7DvdSix.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN1N7DvdSix.lean
diff --git a/library/Unsorry/GcdN22n5EqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN22n5EqOne.lean
similarity index 100%
rename from library/Unsorry/GcdN22n5EqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN22n5EqOne.lean
diff --git a/library/Unsorry/GcdN2N4DvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN2N4DvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdN2N4DvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN2N4DvdTwo.lean
diff --git a/library/Unsorry/GcdN2N6DvdFour.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN2N6DvdFour.lean
similarity index 100%
rename from library/Unsorry/GcdN2N6DvdFour.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN2N6DvdFour.lean
diff --git a/library/Unsorry/GcdN2N8DvdSix.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN2N8DvdSix.lean
similarity index 100%
rename from library/Unsorry/GcdN2N8DvdSix.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN2N8DvdSix.lean
diff --git a/library/Unsorry/GcdN2p1N2p3DvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN2p1N2p3DvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdN2p1N2p3DvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN2p1N2p3DvdTwo.lean
diff --git a/library/Unsorry/GcdN32n7EqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN32n7EqOne.lean
similarity index 100%
rename from library/Unsorry/GcdN32n7EqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN32n7EqOne.lean
diff --git a/library/Unsorry/GcdN3p1Np1EqNp1.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN3p1Np1EqNp1.lean
similarity index 100%
rename from library/Unsorry/GcdN3p1Np1EqNp1.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN3p1Np1EqNp1.lean
diff --git a/library/Unsorry/GcdN4p1N2p1DvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdN4p1N2p1DvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdN4p1N2p1DvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdN4p1N2p1DvdTwo.lean
diff --git a/library/Unsorry/GcdNAddSixDvdSix.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdNAddSixDvdSix.lean
similarity index 100%
rename from library/Unsorry/GcdNAddSixDvdSix.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdNAddSixDvdSix.lean
diff --git a/library/Unsorry/GcdNFactorialSuccEqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdNFactorialSuccEqOne.lean
similarity index 100%
rename from library/Unsorry/GcdNFactorialSuccEqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdNFactorialSuccEqOne.lean
diff --git a/library/Unsorry/GcdNp12np1EqOne.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdNp12np1EqOne.lean
similarity index 100%
rename from library/Unsorry/GcdNp12np1EqOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdNp12np1EqOne.lean
diff --git a/library/Unsorry/GcdNp1N2p1DvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdNp1N2p1DvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdNp1N2p1DvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdNp1N2p1DvdTwo.lean
diff --git a/library/Unsorry/GcdNsq1N1DvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdNsq1N1DvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdNsq1N1DvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdNsq1N1DvdTwo.lean
diff --git a/library/Unsorry/GcdNsq1Nsq3DvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdNsq1Nsq3DvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdNsq1Nsq3DvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdNsq1Nsq3DvdTwo.lean
diff --git a/library/Unsorry/GcdQuadFactoredN1EqN1.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdQuadFactoredN1EqN1.lean
similarity index 100%
rename from library/Unsorry/GcdQuadFactoredN1EqN1.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdQuadFactoredN1EqN1.lean
diff --git a/library/Unsorry/GcdSqNSqNOne.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdSqNSqNOne.lean
similarity index 100%
rename from library/Unsorry/GcdSqNSqNOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdSqNSqNOne.lean
diff --git a/library/Unsorry/GcdThreePowSuccThreePowAddOne.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdThreePowSuccThreePowAddOne.lean
similarity index 100%
rename from library/Unsorry/GcdThreePowSuccThreePowAddOne.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdThreePowSuccThreePowAddOne.lean
diff --git a/library/Unsorry/GcdThreenN7DvdTwentyone.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdThreenN7DvdTwentyone.lean
similarity index 100%
rename from library/Unsorry/GcdThreenN7DvdTwentyone.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdThreenN7DvdTwentyone.lean
diff --git a/library/Unsorry/GcdTwoPowAddOneSubOneDvdTwo.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdTwoPowAddOneSubOneDvdTwo.lean
similarity index 100%
rename from library/Unsorry/GcdTwoPowAddOneSubOneDvdTwo.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdTwoPowAddOneSubOneDvdTwo.lean
diff --git a/library/Unsorry/GcdTwonN5DvdTen.lean b/packages/unsorry-archive-0008/library/Unsorry/GcdTwonN5DvdTen.lean
similarity index 100%
rename from library/Unsorry/GcdTwonN5DvdTen.lean
rename to packages/unsorry-archive-0008/library/Unsorry/GcdTwonN5DvdTen.lean
diff --git a/library/Unsorry/LucasSuccAddLucasPredEqFiveMulFib.lean b/packages/unsorry-archive-0008/library/Unsorry/LucasSuccAddLucasPredEqFiveMulFib.lean
similarity index 100%
rename from library/Unsorry/LucasSuccAddLucasPredEqFiveMulFib.lean
rename to packages/unsorry-archive-0008/library/Unsorry/LucasSuccAddLucasPredEqFiveMulFib.lean
diff --git a/library/Unsorry/NinthPowerModNineteenMem.lean b/packages/unsorry-archive-0008/library/Unsorry/NinthPowerModNineteenMem.lean
similarity index 100%
rename from library/Unsorry/NinthPowerModNineteenMem.lean
rename to packages/unsorry-archive-0008/library/Unsorry/NinthPowerModNineteenMem.lean
diff --git a/library/Unsorry/PairSumSqGeThreeAbcSum.lean b/packages/unsorry-archive-0008/library/Unsorry/PairSumSqGeThreeAbcSum.lean
similarity index 100%
rename from library/Unsorry/PairSumSqGeThreeAbcSum.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PairSumSqGeThreeAbcSum.lean
diff --git a/library/Unsorry/PairwiseProductSumSqGeThreeAbcSum.lean b/packages/unsorry-archive-0008/library/Unsorry/PairwiseProductSumSqGeThreeAbcSum.lean
similarity index 100%
rename from library/Unsorry/PairwiseProductSumSqGeThreeAbcSum.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PairwiseProductSumSqGeThreeAbcSum.lean
diff --git a/library/Unsorry/PellBrahmaguptaCompositionGenericD.lean b/packages/unsorry-archive-0008/library/Unsorry/PellBrahmaguptaCompositionGenericD.lean
similarity index 100%
rename from library/Unsorry/PellBrahmaguptaCompositionGenericD.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellBrahmaguptaCompositionGenericD.lean
diff --git a/library/Unsorry/PellD10FundamentalLadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD10FundamentalLadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD10FundamentalLadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD10FundamentalLadderStepPreserves.lean
diff --git a/library/Unsorry/PellD11LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD11LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD11LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD11LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD12LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD12LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD12LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD12LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD13LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD13LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD13LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD13LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD14LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD14LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD14LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD14LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD15LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD15LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD15LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD15LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD17LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD17LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD17LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD17LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD18LadderStepPreserves.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD18LadderStepPreserves.lean
similarity index 100%
rename from library/Unsorry/PellD18LadderStepPreserves.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD18LadderStepPreserves.lean
diff --git a/library/Unsorry/PellD2FormProductTelescopeStep.lean b/packages/unsorry-archive-0008/library/Unsorry/PellD2FormProductTelescopeStep.lean
similarity index 100%
rename from library/Unsorry/PellD2FormProductTelescopeStep.lean
rename to packages/unsorry-archive-0008/library/Unsorry/PellD2FormProductTelescopeStep.lean
diff --git a/library/index/058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541.aisp b/packages/unsorry-archive-0008/library/index/058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541.aisp
similarity index 100%
rename from library/index/058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541.aisp
rename to packages/unsorry-archive-0008/library/index/058a4449f56de601d4fa76445c8fcc883bf907094752825b176920ba04dca541.aisp
diff --git a/library/index/136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a.aisp b/packages/unsorry-archive-0008/library/index/136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a.aisp
similarity index 100%
rename from library/index/136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a.aisp
rename to packages/unsorry-archive-0008/library/index/136bf4677a9f6f4b6dd70cb52f9794a2c4869d8a033d7b6663a8fe019113075a.aisp
diff --git a/library/index/1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c.aisp b/packages/unsorry-archive-0008/library/index/1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c.aisp
similarity index 100%
rename from library/index/1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c.aisp
rename to packages/unsorry-archive-0008/library/index/1c2f619dfb9c302776ca5d4412ec650fa72713e697a977fae440c8206daa846c.aisp
diff --git a/library/index/20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f.aisp b/packages/unsorry-archive-0008/library/index/20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f.aisp
similarity index 100%
rename from library/index/20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f.aisp
rename to packages/unsorry-archive-0008/library/index/20de29a8789594664dc7f0bf035e3d5102ee0dfa45e7d93ad3a5d27081047e0f.aisp
diff --git a/library/index/2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53.aisp b/packages/unsorry-archive-0008/library/index/2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53.aisp
similarity index 100%
rename from library/index/2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53.aisp
rename to packages/unsorry-archive-0008/library/index/2d903d2fb7a0e6559af8725e813f879efeca95a7659fdcc455d82825d2b5eb53.aisp
diff --git a/library/index/2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0.aisp b/packages/unsorry-archive-0008/library/index/2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0.aisp
similarity index 100%
rename from library/index/2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0.aisp
rename to packages/unsorry-archive-0008/library/index/2e37000c5449248ba58b231974c96c2d1a7f66be09d9757ae7be7826b26b2ee0.aisp
diff --git a/library/index/3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2.aisp b/packages/unsorry-archive-0008/library/index/3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2.aisp
similarity index 100%
rename from library/index/3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2.aisp
rename to packages/unsorry-archive-0008/library/index/3911bba6d737da1acf1c4bdcc7b82ab947d163d4bf572d8aa1beb67f3ca3ddf2.aisp
diff --git a/library/index/3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4.aisp b/packages/unsorry-archive-0008/library/index/3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4.aisp
similarity index 100%
rename from library/index/3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4.aisp
rename to packages/unsorry-archive-0008/library/index/3fd43737ae2fe061a7d26331089437ade2204a79336534c418b82679d3b2a5c4.aisp
diff --git a/library/index/410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe.aisp b/packages/unsorry-archive-0008/library/index/410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe.aisp
similarity index 100%
rename from library/index/410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe.aisp
rename to packages/unsorry-archive-0008/library/index/410e9a067f7104a98c2f22696a386c99a00bb230f80bab431c71744e2e7913fe.aisp
diff --git a/library/index/43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49.aisp b/packages/unsorry-archive-0008/library/index/43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49.aisp
similarity index 100%
rename from library/index/43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49.aisp
rename to packages/unsorry-archive-0008/library/index/43b513bf79e0f7909d4e33cd0392a6bf7197d4721a37a0d3123ae268408b9c49.aisp
diff --git a/library/index/4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083.aisp b/packages/unsorry-archive-0008/library/index/4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083.aisp
similarity index 100%
rename from library/index/4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083.aisp
rename to packages/unsorry-archive-0008/library/index/4a642fb9ab75babdfc47c6c35f33cb785c124444f8cc83f0573f277a6b5a8083.aisp
diff --git a/library/index/4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218.aisp b/packages/unsorry-archive-0008/library/index/4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218.aisp
similarity index 100%
rename from library/index/4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218.aisp
rename to packages/unsorry-archive-0008/library/index/4a9553e1882190873c6e41e9ffcdfac9445450e0b1476cfbb17898e80abbc218.aisp
diff --git a/library/index/5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562.aisp b/packages/unsorry-archive-0008/library/index/5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562.aisp
similarity index 100%
rename from library/index/5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562.aisp
rename to packages/unsorry-archive-0008/library/index/5753ba3338af411b9e4a3fff7b9307ebdd7a08251c47abd62cbd314b82051562.aisp
diff --git a/library/index/5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b.aisp b/packages/unsorry-archive-0008/library/index/5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b.aisp
similarity index 100%
rename from library/index/5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b.aisp
rename to packages/unsorry-archive-0008/library/index/5b640a966144975b8b958a65e46f6fc546aaea76608b07dd9b5387dea1c3838b.aisp
diff --git a/library/index/5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2.aisp b/packages/unsorry-archive-0008/library/index/5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2.aisp
similarity index 100%
rename from library/index/5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2.aisp
rename to packages/unsorry-archive-0008/library/index/5e7e046b17bc0a279807df171d6fa5420d5b84799ec33173e3ad9f179eeab7f2.aisp
diff --git a/library/index/6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a.aisp b/packages/unsorry-archive-0008/library/index/6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a.aisp
similarity index 100%
rename from library/index/6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a.aisp
rename to packages/unsorry-archive-0008/library/index/6078a1d0a9e163095b8bf600311609308c6e1a7eb0e42c583aee984ca3e8072a.aisp
diff --git a/library/index/6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb.aisp b/packages/unsorry-archive-0008/library/index/6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb.aisp
similarity index 100%
rename from library/index/6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb.aisp
rename to packages/unsorry-archive-0008/library/index/6f4aa7b31addfc3f3f35799df348045c674dc4f1e78703074e4905c8f6d080cb.aisp
diff --git a/library/index/70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd.aisp b/packages/unsorry-archive-0008/library/index/70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd.aisp
similarity index 100%
rename from library/index/70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd.aisp
rename to packages/unsorry-archive-0008/library/index/70238bd30c936e7b29cfa5a32337c3dd915bedbfd8bc799804c38bb5c203f3dd.aisp
diff --git a/library/index/75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633.aisp b/packages/unsorry-archive-0008/library/index/75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633.aisp
similarity index 100%
rename from library/index/75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633.aisp
rename to packages/unsorry-archive-0008/library/index/75c1b679e29279dcfb6ad92dd629c0811a1e4e9525de6f8dc8b325cd5c68c633.aisp
diff --git a/library/index/77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad.aisp b/packages/unsorry-archive-0008/library/index/77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad.aisp
similarity index 100%
rename from library/index/77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad.aisp
rename to packages/unsorry-archive-0008/library/index/77bda8deb46e2f039468ff87285c91b8ee79a17b760017f45dd6487a226303ad.aisp
diff --git a/library/index/794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde.aisp b/packages/unsorry-archive-0008/library/index/794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde.aisp
similarity index 100%
rename from library/index/794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde.aisp
rename to packages/unsorry-archive-0008/library/index/794fa8da0a45a9837d2b583d4fdb85f21e58904b58f7ba1fee1ee15100b4dbde.aisp
diff --git a/library/index/806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b.aisp b/packages/unsorry-archive-0008/library/index/806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b.aisp
similarity index 100%
rename from library/index/806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b.aisp
rename to packages/unsorry-archive-0008/library/index/806fa7ee4f56d688c209a5e632d31a9b3e6e49faca199b59099661203575ac6b.aisp
diff --git a/library/index/85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866.aisp b/packages/unsorry-archive-0008/library/index/85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866.aisp
similarity index 100%
rename from library/index/85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866.aisp
rename to packages/unsorry-archive-0008/library/index/85fcc952e2a4189a5ab1a4f205bd93bcd33e22aa0b5e4a3c2326d1057c6bb866.aisp
diff --git a/library/index/8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca.aisp b/packages/unsorry-archive-0008/library/index/8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca.aisp
similarity index 100%
rename from library/index/8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca.aisp
rename to packages/unsorry-archive-0008/library/index/8fcb380df62f6ef15d3860deeafdff0433299992151f143fa01f7ccf221ae6ca.aisp
diff --git a/library/index/963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0.aisp b/packages/unsorry-archive-0008/library/index/963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0.aisp
similarity index 100%
rename from library/index/963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0.aisp
rename to packages/unsorry-archive-0008/library/index/963e8b56901beb58a0e51387d1e1f22c798ec68e88c1de770b1d2126703e91d0.aisp
diff --git a/library/index/a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310.aisp b/packages/unsorry-archive-0008/library/index/a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310.aisp
similarity index 100%
rename from library/index/a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310.aisp
rename to packages/unsorry-archive-0008/library/index/a3d035df5528945a44edf26b063fa207aebce2e771a2c76b6a63a6dd8add7310.aisp
diff --git a/library/index/a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274.aisp b/packages/unsorry-archive-0008/library/index/a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274.aisp
similarity index 100%
rename from library/index/a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274.aisp
rename to packages/unsorry-archive-0008/library/index/a48a1a5e7beadb4b8ebf98f47d8c5fed71c7c1d70e5d576c26523661f5ca6274.aisp
diff --git a/library/index/a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b.aisp b/packages/unsorry-archive-0008/library/index/a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b.aisp
similarity index 100%
rename from library/index/a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b.aisp
rename to packages/unsorry-archive-0008/library/index/a966b6ae8e0a8c236a9d91bcd9ced22f0b3bfce874cfb7265bf341aa1729205b.aisp
diff --git a/library/index/ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0.aisp b/packages/unsorry-archive-0008/library/index/ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0.aisp
similarity index 100%
rename from library/index/ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0.aisp
rename to packages/unsorry-archive-0008/library/index/ae9f8477715e75a88a3bba297c62b362cc632946435f2b1fd8075dcda5c64fb0.aisp
diff --git a/library/index/b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd.aisp b/packages/unsorry-archive-0008/library/index/b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd.aisp
similarity index 100%
rename from library/index/b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd.aisp
rename to packages/unsorry-archive-0008/library/index/b3974d3293a1bd75f8bed35e00f337721b38e10b087f44a1ff32aaf0550022cd.aisp
diff --git a/library/index/b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520.aisp b/packages/unsorry-archive-0008/library/index/b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520.aisp
similarity index 100%
rename from library/index/b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520.aisp
rename to packages/unsorry-archive-0008/library/index/b518f57c58adaa9dbbfae832db0878d978468849aea54fc8edd840e7f5d27520.aisp
diff --git a/library/index/ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337.aisp b/packages/unsorry-archive-0008/library/index/ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337.aisp
similarity index 100%
rename from library/index/ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337.aisp
rename to packages/unsorry-archive-0008/library/index/ba7009d4b7ba4f132e0813e4ea18cc9e5a3cce110d6335735be6d9ac6a6ee337.aisp
diff --git a/library/index/d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a.aisp b/packages/unsorry-archive-0008/library/index/d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a.aisp
similarity index 100%
rename from library/index/d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a.aisp
rename to packages/unsorry-archive-0008/library/index/d7db9810b4e482ee6e95bd9fdbe9177d86a426210872ec4133e31e01c160e44a.aisp
diff --git a/library/index/da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934.aisp b/packages/unsorry-archive-0008/library/index/da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934.aisp
similarity index 100%
rename from library/index/da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934.aisp
rename to packages/unsorry-archive-0008/library/index/da1871e4a2e2d1e9bf7c11b1526200fff6fdb19c077687d94e2a14da640c1934.aisp
diff --git a/library/index/e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528.aisp b/packages/unsorry-archive-0008/library/index/e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528.aisp
similarity index 100%
rename from library/index/e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528.aisp
rename to packages/unsorry-archive-0008/library/index/e0303a51da4839820f60058ea82bdc2c2123a91c94f73b657559774a68955528.aisp
diff --git a/library/index/ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216.aisp b/packages/unsorry-archive-0008/library/index/ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216.aisp
similarity index 100%
rename from library/index/ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216.aisp
rename to packages/unsorry-archive-0008/library/index/ecfd4e826bb0f0f51259a3d779fe7edd819573d85528bb7bc6a4e72579ae7216.aisp
diff --git a/library/index/f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f.aisp b/packages/unsorry-archive-0008/library/index/f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f.aisp
similarity index 100%
rename from library/index/f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f.aisp
rename to packages/unsorry-archive-0008/library/index/f3ebef0f1e56e964ec1ed9458227bc864a559198820ae251a46663498fb7943f.aisp
diff --git a/library/index/f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8.aisp b/packages/unsorry-archive-0008/library/index/f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8.aisp
similarity index 100%
rename from library/index/f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8.aisp
rename to packages/unsorry-archive-0008/library/index/f3f5db6b6d94637f6ba8e13001fbb369dd29d4a63e7c1fee0531ad30b30ffce8.aisp
diff --git a/library/index/f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a.aisp b/packages/unsorry-archive-0008/library/index/f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a.aisp
similarity index 100%
rename from library/index/f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a.aisp
rename to packages/unsorry-archive-0008/library/index/f560d5fd762d6df87a0d33a1528ffc147f193ac2e82f1d37ffbdf69d92d01c8a.aisp
diff --git a/library/index/f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874.aisp b/packages/unsorry-archive-0008/library/index/f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874.aisp
similarity index 100%
rename from library/index/f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874.aisp
rename to packages/unsorry-archive-0008/library/index/f7aa4469a3b4037c7258c4a599e808c67ae87454d2db4f429bde563ceac11874.aisp