Artifact for "Unscanning by Möbius Inversion"

This artifact contains the Rocq formalization accompanying the paper "Unscanning by Möbius Inversion". The record contains two files: Unscan.tgz: the source archive, containing the Rocq proof scripts, README, LICENSE, _CoqProject, and generated HTML documentation. Unscan-VM.tar.xz: the prepared virtual machine image for artifact evaluation, including the same sources, prebuilt proof objects, generated HTML documentation, and the required dependencies. The prepared VM includes Rocq 9.0.0, MathComp 2.4.0, and Hierarchy Builder 1.10.1. The recommended validation command is `make validate`, which checks the compiled development with `rocqchk`; the expected final summary includes `Axioms: `.