VR-Forms: An Operational Two-Register Apparatus over VR-Sets

VR-Forms is the fourth work in the cycle developing the VR programme(Reznik 2026, preprints VR. A Formal System, VR-Numbers, VR-Sets). Itintroduces a two-register apparatus on top of VR-Sets: an ontologicalregister (operational sets of VR-Sets, with closure principle andreference-based ∈) and a formal register (syntactic descriptionswithout ontological commitment). The formal register provides a universal language for everything thatis not in the operational ontology — classical uncountable objects,paradoxical classes, mythological and theological terms, philosophicalcategories. The two registers are connected by a conservativity theorem(Theorem III.1): the formal register is a conservative extension of theoperational, generating no new ontological commitments and provingnothing in the ontological register that VR-Sets could not alreadyprove. The transit rule allows formal reasoning over uncountableintermediaries, with results automatically translating into theoperational register when the conclusion is itself ontological. The apparatus closes the ontological contour of the VR cycle: VR cannow speak about everything, with only ∅ in its ontology. Classicalparadoxes (Russell, Vitali, Skolem) and classical uncountable objects(ℝ, ℘(ℕ), proper classes) receive a clear status — formal termswithout operational correlate. The same status, by uniform applicationof the principle of forms, extends to mythological, theological, andliterary descriptions, demonstrating the universality of the formalregister beyond mathematics. Changes in version 1.0.1. A new Part IX has been added: "Lean 4 Formalisation of VR-Forms:Methodological Observations." This part documents the Lean 4formalisation of the formalisable core of the apparatus — Parts II–IV(formal language, realisability, transit) plus mixed formulas of §VII.2(Reznik 2026, Lean VR-Forms, Software DOI 10.5281/zenodo.20355757;Git tag v1.3-vr-forms). The formalisation is a shallow embedding overmathlib with one explicit structural boundary at conservativity(Theorem III.1), which would require deep-embedded Formula andDerivation types beyond the scope of this cycle. Ten methodological observations are reported in four thematic clusters:foundation-level properties (§IX.1, two observations on import-freedomand inheritance from VR-Sets Classical-free closure layer); the centralboundary at conservativity and its four substructural manifestations(§IX.2, five observations on the equation-compiler catch-all,realisability/π-translation as complementary layers, two-level negativecases, and the three-category structure of formal terms); structuralpatterns in the apparatus (§IX.3, two observations on universe handlingacross cycle boundaries and the cross-register manifestation of the ZFAboundary); and cross-cycle integration (§IX.4, one observation closingthe cycle with the finding that zero Classical.choice usage is achievedthroughout). Section §IX.5 compares the boundary structure of VR-FormsLean (one proof-theoretic boundary with four substructuralmanifestations) with that of VR-Sets Lean (five mathematical-contentboundaries), and §IX.6 summarises the ten observations together withwhat they resolve relative to §VIII.1 questions. The Lean formalisation contains 18 public objects across 5 files(Forms/Language.lean, Forms/Realisability.lean, Forms/Transit.lean,Forms/Bridge.lean, Forms/Examples.lean) totalling approximately 1,545lines of Lean code, with no sorry and no admit. The full axiom auditshows: 3 objects (Stage 1) are axiom-free (empty axiom profile),15 objects sit at [propext, Quot.sound], and 0 objects requireClassical.choice. This is the most axiom-minimal of the four VR Leancycles — a stricter result than the original cycle plan predicted, andstructurally consequent on the fact that the realisable cases ofVR-Forms correspond to the Classical-free closure theorems of VR-Sets. Part IX resolves Question 1 of §VIII.1 (machine formalisation inLean/Coq/Agda) for the formalisable core of the apparatus. The centralconservativity theorem (Theorem III.1) is documented as the explicitstructural boundary of the Lean cycle, with verbatim citation in theLean source comments and external reference to the preprint's §III.2proof. Other changes: §I.8 (Structure of the work) updated to list nine partsinstead of eight, with the description of Part IX added. Referencesupdated with the new Lean VR-Forms entry. Acknowledgement of AIassistance expanded to describe the parent-child review architecture(Opus 4.7 reviewer, Sonnet 4.6 in Claude Code writing Lean code) usedfor the formalisation — identical to that used in VR-Sets v1.0.1. No mathematical content of Parts I–VIII has been revised; the changesare additive (Part IX is new) and editorial. Companion publications. Preprint VR-Sets v1.0.1 (DOI10.5281/zenodo.20354628) similarly documents the Lean 4 formalisationof its mathematical core in Part X. The full VR cycle in its v1.0.1form consists of four preprints (VR, VR-Numbers, VR-Sets, VR-Forms) andfour Lean formalisations, all available on Zenodo with cross-references.