VR-Sets-ZFA is a foundational extension of VR-Sets providing operational reference semantics for non-well-founded sets in Lean 4, and the sixth work in the VR Cycle. It takes the coinductive parallel of mathlib's inductive PSet via PFunctor.M, defines an extensional cobisimulation quotient OSetZFA, proves Aczel's Anti-Foundation Axiom (AFA) as a theorem from the final coalgebra property rather than positing it, and establishes a faithful, membership-preserving embedding of the well-founded universe OSet into OSetZFA. It thereby resolves Conjecture IV.2 of VR-Sets constructively: a type satisfying AFA can be built in VR's operational universe. The Quine atom and an omega chain are machine-verified non-vacuity witnesses, and the bisimulation collapse identifying the two-cycle graph with the self-loop graph is proved as a theorem; the whole development stays within mathlib's standard axiom ceiling propext, Classical.choice, Quot.sound, introducing no new axiom. The accompanying machine-checked Lean 4 formalisation is published separately (DOI 10.5281/zenodo.20368268). 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 — and adds Observation 11 on finite axiomatization, noting that both infinite ZF schemas (Separation and Replacement) collapse to single machine-checked closure theorems and that the set-theory arc replaces postulates (choice, anti-foundation) with theorems on the operational universe; no part of the ZFA construction is 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. Sixth work in the VR Cycle. Companion to Lean 4 formalisation: DOI 10.5281/zenodo.20368268.
Vitaly Reznik (Sun,) studied this question.