VR-Audit is an open-ended programme of operational audits of classical theorems of mathematics and the fifth work in the VR Cycle, its first applied one. It applies the two-register apparatus of VR-Forms: each audit establishes an operational corollary of a classical theorem through the transit pattern, in which the classical machinery is invoked as a black box in the formal register while operationality of the result is established separately, in the operational register, through wrapping predicates and explicit witness construction. The preprint accumulates the programme, each version superseding the previous as a complete record to date. Version 1.0.0 contains the first audit — the Hahn–Banach extension theorem for operational Hilbert spaces, proved via Riesz representation — exhibiting precisely where the classical tool is used and where the operational content is built. The accompanying machine-checked Lean 4 formalisation is published separately (DOI 10.5281/zenodo.20363739). Version 1.0.1 reframes the exposition to the cycle's no-ontology position — the empty set is taken as a nullary operation and "operational ontology" is renamed the operational universe/foundation — with no mathematics altered. The work was produced with AI assistance under Variant A (interactive parent-child architecture), human curator Vitaly Reznik, consistent with all works of the VR Cycle. Accompanying Lean 4 formalisation: DOI 10.5281/zenodo.20363739.