These tables map each definition and theorem in the paper to its mechanised counterpart in this development. All file paths are relative to the PackageCalculus/ source directory.

Where the paper writes structured names like ⟨n, vs⟩ ∈ N or ⟨n, f⟩, the Lean uses dedicated inductive name/version types and Has*Names / Has*Versions typeclasses to inject them.

The paper states one standing condition on every dependency relation: Functional in Name (Def 3.1.2). In Lean it appears as an explicit hypothesis (DepRel.FunctionalInName) on the theorems that consume it. The paper's normalisation remark -- merging same-name entries per depender by intersecting their version sets -- is mechanised as DepRel.merge (merge_functionalInName, merge_resolution_iff), alongside DepRel.restrictReal (restrictReal_resolution_iff) for restricting version sets to real packages; both preserve the set of resolutions.

3. The Package Calculus#

4. Package Managers, Mise en Place#

4.1 Conflicts#

4.2 Concurrent Versions#

4.3 Peer Dependencies#

4.4 Dependency Visibility#

4.5 Features#

4.6 Package Formulae#

4.7 Variable Formulae#

4.8 Virtual Packages#

5. Package Managers, à la Carte#

5.1 Composition of Extensions#

5.2 Transpiling Packaging Languages#

Lifting is mechanised per extension under Extensions/<Extension>/Lifting/ (and Versions/Lifting/): Definition.lean defines lift, Retraction.lean proves the round trip, and Soundness.lean/Completeness.lean carry core resolutions back to extension resolutions.

Where the statement is weaker than lift ∘ reduce = id, the loss is syntactic rather than semantic: the lift recovers a normal form that is proven faithful. Formulae are recovered as their NNF atom sets, and satisfies_iff_atoms shows a resolution satisfies a formula iff it satisfies its atoms; a variable comparison is recovered as its extension, which is all evaluation consults; virtual and version-formula dependencies are recovered up to restrictReal, which removes only versions no resolution can select. The Virtual provides relation is likewise recovered as a normal form, its instantiation on Δ -- the admissible (provider, name, depender) triples -- and instantiate_resolution_congr shows resolutions consult it only through this instantiation; only the guards' behaviour on dependencies outside Δ is lost. Each side condition's docstring in the Lean states why it is needed.

Appendix B -- DependencyResolution complexity#

The paper's NP-completeness result (Thm 3.1.4) combines NP-hardness -- a polynomial-time reduction from 3SAT -- with NP-membership, which the paper establishes by direct polynomial-time verification of a candidate resolution (root inclusion, dependency closure, version uniqueness). In Lean we mechanise the reduction's soundness and completeness (below); the polynomial-time bound and the membership verification are argued by inspection in the paper, not formalised. The SAT encoding in Appendix C is a separate SAT-based solving method (formalised in SATEncoding.lean).

Appendix C -- SAT-based resolution#

Appendix D -- Singular Dependencies#

Defs C.5 and C.6 (resolution ordering, ordered SAT encoding) and Appendix E (build graph, optional dependencies) are definitional discussion with no accompanying theorems, and are not mechanised.