This artifact is a Lean 4 mechanisation of the Package Calculus: a core calculus of dependency resolution, its extensions and their reductions to the core (with soundness and completeness), a composition of two extensions, and a 3-SAT reduction for the NP-completeness of resolution. It is a proof-script artifact – there is no executable to run; the contribution is the machine-checked development itself. It has no special hardware or software requirements beyond the pinned Lean toolchain and Mathlib.