The artifact mechanizes the paper’s soundness and locality theorems in two proof assistants:

Soundness (Rocq 9.0.1). Three theory files — typed-data foundation (Definitions.v), location-addressable memory (LAM.v), and content-addressable memory (CAM.v) — mechanize the paper’s main lemmas on serialization round-trips, deep-equality equivalence, shallow treeification, value-duplication bounds, GC-evacuation soundness, encode/decode determinism, and the CAM commit/load round-trip. The trusted base is the small set of paper-declared assumptions (primitive byte codec and its round-trip/locality laws, an abstract rolling-hash family, the chunking modulus κ and cap C, and the external content-addressable store’s get/put laws), enumerated in the README. No admitted goals.

Locality (Lean 4.27.0 + Mathlib4 v4.27.0). The CamLocality library mechanizes the locality theorem — expected and worst-case bounds on the number of chunks and the spillover affected by a depth-d edit under content-defined chunking — together with the supporting metafunctions. Mathlib4 supplies the expected-value framework (PMFs, Bochner integrals, linearity of expectation). No new axioms.

The artifact ships as a QEMU virtual-machine image built on the committee’s base image, with both toolchains pre-installed and the Mathlib4 olean cache pre-populated. A single make re-checks every proof in ~22 minutes from a clean state, entirely offline.