The preprint (§ III.5) asserts that \(\mathcal{P}(\omega )\) in VR-Sets is countable: each element is a describable functionality (a finite algorithm over a finite alphabet), and the set of such algorithms is countable. Cantor’s diagonal \(D = \{ n : n \notin S_n\} \) requires a complete enumeration of describable subsets — operationally unattainable (equivalent to solving the Halting Problem). \(D\) does not specify a describable functionality, hence \(D\) is not a set in the operational universe. The diagonal is absent from the operational \(\mathcal{P}(\omega )\) not by prohibition but because its premise is unrealisable. Lean’s osetPower contains all classical subsets; the countability claim is metatheoretic.

The preprint (§ III.9) derives AC from Dependent Choice plus countability of the operational universe. AC is thus a theorem, not an axiom; the Banach–Tarski paradox is excluded not by weakening AC but because the uncountable subsets of \(\mathbb {R}\) on which it relies do not exist in the operational universe. Lean records AC via Classical.choice for all families; the countability argument is metatheoretic.

In classical ZF, Replacement is an axiom schema (one axiom per formula). In VR-Sets and in Lean/mathlib, a single theorem quantifies over all functions \(F\). The schema collapses because Lean functions are first-class objects: the meta-level quantification over formulas disappears. See Observation D.1.

Classical.choice enters through four distinct mechanisms: (1) Lemma_II_3_DepthMono via Ordinal.iSup (ordinal supremum); (2) Theorem_III_7_Replacement via Classical.allZFSetDefinable (all Lean functions declared definable); (3) Theorem_III_8_Foundation via WellFounded.has_min (minimal element); (4) Theorem_III_9_Choice via Classical.choice directly. None is a direct application of AC to a set-theoretic family. Contrast with VR-Numbers where Classical.choice entered through a single source (Rat.add via Nat.gcd).

The preprint’s operational identity \(\equiv \) (Definition 4, bisimulation) is not a separate proof step but is definitionally absorbed into the quotient construction: \(a \equiv b\) is exactly \(a = b : \texttt{OSet} = \texttt{ZFSet} = \texttt{Quotient PSet.setoid}\). This is more economical than VR-Numbers, where each isomorphism required explicit forward/backward round-trip proofs. Here, the bisimulation is the quotient.

The preprint (§ II.2) says union reveals elements «without repetitions up to \(\equiv \)». In ZFSet, duplicate suppression requires no separate predicate or decidability instance: the quotient automatically identifies extensionally equivalent elements. ZFSet.sUnion and ZFSet.powerset return ZFSet values, so membership is already modulo PSet.Equiv.

Lean’s osetPower contains all classical subsets. The preprint’s \(\mathcal{P}(A)\) contains only operationally describable subsets. For \(A = \omega \), Lean gives an uncountable set; the preprint gives a countable set. The operational restriction is metatheoretic.

osetReplacement admits all Lean functions \(F\). The preprint restricts to operationally definable functions. Classical.allZFSetDefinable records the gap: «all Lean functions are definable» is the non-operational assumption.

Lean proves AC for all families via Classical.choice. The preprint argues AC from countability: in a countable universe, a choice function can be constructed algorithmically (DC suffices). Lean cannot express the countability restriction; the argument is metatheoretic.

On OSet = ZFSet, Foundation holds unconditionally (Lean is narrower than the preprint). The preprint treats Foundation as mode-dependent (fails in ZFA-mode). In Lean, there is no ZFA-mode to speak of; the type pre-commits to well-foundedness. This is the opposite direction from boundaries B.1–B.3.

A systematic search of all of mathlib4 for AFA, AntiFoundation, non-well-founded, coinductive sets, NonWellFounded, and Quine returned zero results. PSet is an inductive (not coinductive) Lean type; membership is well-founded by its elimination rule. The Quine atom and AFA are not merely hard to construct — they are provably impossible in PSet with empty axiom profiles. This boundary is categorically stronger than B.1–B.4 and stronger than the VR-Numbers § VIII.6 boundary: the ZFA-mode universe has no representation at all in the mathlib type hierarchy.

See Remark 110 for details.

Conjecture_IV_1_Statement: Axiom profile: [propext, Quot.sound] (references OSet = ZFSet, a specific quotient type). Conjecture_IV_2_Statement: Axiom profile: [] (stated over abstract \((U, \mathrm{mem})\), no reference to any specific mathlib type). The difference is not incidental: Conjecture IV.1 asks about a countable submodel of an existing type; Conjecture IV.2 asks about the existence of a type outside the current mathlib hierarchy. The axiom profiles witness this structural distinction at the level of dependency closures.

On OSet = ZFSet, isZFCmode is universally true; the predicate is trivial here. Its conceptual content becomes operative only at the PSet level (Stage 10), where elements representing the Quine atom would fail Acc PSet.Mem (the membership chain \(A \ni A \ni A \ni \ldots \) does not terminate). The predicate is defined at OSet-level as a syntactic template for that future analysis.

Lemma II.3 in the preprint has three cases: finite depth, infinite non-cyclic depth (e.g. \(\omega \)), and cyclic/undefined depth (e.g. Quine atom). In OSet = ZFSet, the third case is structurally absent: PSet is inductive, so cyclic objects do not exist. operationalDepth is well-defined (total) on all OSet elements; the preprint’s undefined case simply does not arise in the type.

Classical ZF has Replacement as a schema (one axiom per formula). VR-Sets has a single closure theorem over describable functions. Lean/mathlib has a single theorem parametric in \(F : \texttt{ZFSet} \to \texttt{ZFSet}\). Three systems, three different motivations (classical meta-level quantification / operational describability / type-theoretic first-class functions), same formal result: one theorem.

VR-Numbers produced only positive results (theorems proved). VR-Sets produces a structurally richer three-tier outcome: (1) 16 proved theorems (including Theorem_IV_1_ZFCAxioms, Theorem_V_2); (2) 2 refuted claims (AFA_Refuted, quineAtom_impossible), both axiom-free; (3) 2 open formulations (Conjecture_IV_1_Statement, Conjecture_IV_2_Statement). The refuted claims are structural boundary theorems, not logical inconsistencies. The open formulations are the first instances in the VR Lean cycle where the system records a claim it cannot resolve.

OSet is declared as abbrev (@[reducible]), not def. This means all mathlib operations on ZFSet apply directly to OSet without wrappers. VR-Numbers used def with explicit wrappers (IntVRIntIso, iaddQ, etc.) because VR-Numbers built its own arithmetic independently. VR-Sets relies on mathlib’s ZFSet infrastructure completely; abbrev reflects this dependency.

Conjecture_IV_2_Statement is stated with classical AFA (all Lean types \(V\), all relations \(E\)) — strictly stronger than the preprint’s operational AFA (only describable graphs). If the conjecture is false, it does not refute the preprint’s weaker form. If true, it implies the preprint’s form. Classical AFA is used because operational AFA (like computability of Cauchy sequences in VR-Numbers) is not Lean-expressible: the condition «describable graph» is metatheoretic.

VR_OSet_iso has five fields: embed, preserve_zero, preserve_succ, preserve_mem, injective. Arithmetic preservation (vadd, vmul, vpow at OSet level) is deliberately excluded. It follows by composition: \(\mathrm{VRObj} \xrightarrow {\texttt{Theorem\_ 11\_ VR\_ PA}} \mathbb {N} \xrightarrow {\texttt{embedVR} \circ O} \mathrm{OSet}\). Re-proving at the OSet level would duplicate VR.lean without adding mathematical content. Contrast with VR_PA_iso (Chapter 2): that is a bijection; VR_OSet_iso is an embedding (OSet contains vastly more than the image of VRObj).

The preprint’s closure principle (§ II.3): «if a functionality is operationally describable, then there exists a set \(A\) such that \(A\) is that functionality» is not expressible as a Lean predicate. Individual closure theorems (Pairing, Union, …) are proved separately, each as a wrapper over a mathlib ZFSet lemma. The general principle — «every describable functionality is a set» — lies in the metatheory.