VR-Sets: An Operational Set Theory Unifying ZFC and ZFA (Brouwer Edition)

A reconstruction of set theory inside the VR programme as an operational universe. A set is a functionality that, on a query, reveals its members — formally a pointed graph — and the identity of sets is a witnessed bisimulation, carried as a relation and never collapsed to a quotient. On this carrier, machine-checked in Lean 4 and below the Classical.choice floor, the development obtains: membership, strong extensionality (identity is exactly co-membership), and every axiom of ZF without Foundation — the empty set, pairing, union, power set, the von Neumann naturals and ω, Separation and Replacement. Well-foundedness is not an axiom but a predicate (IsGrounded): ZFC and ZFA are two fragments of one operational domain — the grounded sets and the whole universe — not a foundational choice one is forced to make. Anti-Foundation is a theorem, and axiom-free: a member is the same graph re-pointed, so nesting — including self-membership, the Quine atom being a one-vertex self-loop — is native, and decoration of any graph is almost definitional. The earlier §VI error (operational universe countable ⇒ Axiom of Choice free) is corrected: the universe as becoming is genuinely non-enumerable (a choice-free Cantor diagonal), while the describable register (sets given by a finite rule) is countable; full AC is therefore not an operational theorem — only dependent choice is. The absence of Banach–Tarski is re-explained through conservativity and anchored in Solovay's model. Version 1.1.0 (minor — new mathematics added, none altered) adds: the operational power set (choice-free, though impredicative — isolating the obstruction to power set as impredicativity, not choice); Anti-Foundation as an axiom-free theorem on the pointed-graph carrier, with the cost-of-quotient bridge to VR-Sets-ZFA (the same content costs an empty axiom profile in relational form versus the full classical ceiling once quotiented); the Solovay anchor for Banach–Tarski; and two named boundaries (the standing setoid discipline; impredicativity's invisibility to the axiom audit). Foundational work of the VR Cycle; Lean 4 module VRCycle.SetsOp. Prepared with the assistance of Claude (Anthropic, Opus 4.8) in the cycle's Variant A architecture; all mathematical content and positions are due to the author, Vitaly Reznik.