6 VR-Forms
6.1 Position
VR-Forms is the two-register apparatus over the operational sets. The operational register (L0) describes operational sets in the sense of Chapter 14: revealing functionalities, identical when bisimilar by witness. The formal register (L1) accommodates syntactic descriptions without operational obligation—classically uncountable objects, paradoxical classes, and any correctly built term regardless of operationality or consistency. The two registers are connected by the translation \(\pi \) and by Theorem III.1 (conservativity).
Clarification on register language. The registers describe modes of description, not separate operational levels. All descriptions are operational acts; the distinction is whether the described referent has an operational correlate.
Two readings of the operational register (2026-09-12, integrity programme, step 3). Until 2026-09-12 the operational register of the Lean formalisation was Mathlib’s well-founded ZFC universe OSet = ZFSet (Chapter 4), and every object above the language layer carried [propext, Quot.sound]. The formalisation now lives in the core library VR over the operational universe OpSet (Chapter 14) — VR/Forms/Realisability.lean, Transit.lean, Examples.lean, Substrate.lean — and every declaration is on the empty axiom list, enforced by the core’s build-time guard. The ZFC reading is kept, named as such, in VRClassical/Forms/Bridge.lean: the predicate isRealisableZFC (§ 6.5) is realisability with the operational register taken to be ZFSet. The two readings disagree on exactly one named term, \(\ulcorner \mathrm{AFA}\urcorner \), and their disagreement is itself a theorem (§ 6.6): the ZFA boundary of VR-Sets is a boundary of groundedness (a mode), not of operationality. Axioms that appear in the bridge are Mathlib’s (ZFSet/PSet) — the bridge’s, not VR’s.
Architectural note. The Lean formalisation is a shallow embedding: formal terms are Lean strings carrying a register tag; \(\pi \) is a total Lean function; realisability is a Lean predicate. Theorem III.1 (conservativity), proved in the preprint, is formalised beside the shallow embedding by a separate deep embedding (Forms/Conservativity.lean, ConservativityFOL.lean, ConservativityComprehension.lean): Formula over de Bruijn terms, a classical Hilbert Provable, the translation \(\pi \), and the conservativity theorem by induction on derivations, with a concrete VR instance. See § 6.4.1.
Axiom profile: [] for every object of the core files (language, realisability, transit, conservativity in all three storeys, examples, substrate); the ZFC bridge inherits Mathlib’s Axiom profile: [propext, Quot.sound] and, through PSet, no Classical.choice.
6.2 Formal language (Part II)
Register is an inductive type with two constructors: .operational (the operational register L0) and .formal (the formal register L1). Axiom profile: [] — no imports; pure Lean 4 prelude.
FormalTerm is a structure with fields description : String and register : Register. The notation \(\ulcorner \tau \urcorner \) always produces FormalTerm.mk \(\tau \) .formal. The Principle of Forms (§ II.4): any syntactically correct string specifies a formal term — no operationality, consistency, or constructivity is required. Injectivity of the constructor is proved by hand (FormalTerm.mk_eq_iff); the auto-generated injEq is not produced, since it would carry propext. Axiom profile: [] — Language.lean imports nothing.
6.3 Realisability (Part II § II.7)
Realisability is defined in two steps. A closed-world classifier \(\texttt{named} : \texttt{FormalTerm} \to \texttt{Named}\) sends a term, by decidable equality of its description, to one of \(\{ \texttt{empty}, \texttt{omega}, \texttt{pair}, \texttt{afa}, \texttt{other}\} \); then \(\texttt{isRealisableN} : \texttt{Named} \to \mathrm{Prop}\) gives each class its existential proposition over OpSet:
|
\(\ulcorner \)"∅"\(\urcorner \) |
\(\exists \, s : \mathrm{OpSet},\; \forall x,\; \lnot \, x \mathrel {\mathtt{Mem}} s\) |
|
\(\ulcorner \)"omega"\(\urcorner \) |
\(\exists \, s : \mathrm{OpSet},\; \mathtt{vn}\, 0 \mathrel {\mathtt{Mem}} s \land \forall n,\; n \mathrel {\mathtt{Mem}} s \to \mathtt{succ}\, n \mathrel {\mathtt{Mem}} s\) |
|
\(\ulcorner \)"pair"\(\urcorner \) |
\(\forall a\, b : \mathrm{OpSet},\; \exists \, s,\; \forall x,\; x \mathrel {\mathtt{Mem}} s \leftrightarrow x \mathrel {\mathtt{Equiv}} a \lor x \mathrel {\mathtt{Equiv}} b\) |
|
\(\ulcorner \)"AFA"\(\urcorner \) |
\(\forall \, (V : \mathrm{Type})\, (E : V\to V\to \mathrm{Prop}),\; \exists \, d : V \to \mathrm{OpSet},\; \mathtt{IsDecoration}\, E\, d\) |
|
any other |
False |
\(\texttt{isRealisable}\, t := \texttt{isRealisableN}\, (\texttt{named}\, t)\). Membership is read as Mem and identity as Equiv: the pair \(\{ a,b\} \) has members identical to \(a\) or \(b\) by witness, not by extension. Each realisable case is an existential Lean Prop (not True), preserving the mathematical content of the witness. The two-step form replaces the earlier match on string literals: a match with overlapping literal patterns generates a splitter that carries propext; the if-chain of named does not. Axiom profile: [].
\(\texttt{isRealisable\_ empty}\): witness OpSet.empty, which reveals nothing (not_mem_empty). \(\texttt{isRealisable\_ omega}\): witness OpSet.omega (empty_mem_omega, omega_succ_closed). \(\texttt{isRealisable\_ pair}\): witness OpSet.pair a b (mem_pair, up to Equiv). \(\texttt{isRealisable\_ AFA}\): witness OpSet.decorate E (decorate_isDecoration) — every graph has a decoration in the operational universe. All four on Axiom profile: [].
Across the two readings the formal terms fall into three categories: (a) Provably realisable in the operational universe — \(\ulcorner \)"∅"\(\urcorner \), \(\ulcorner \)"omega"\(\urcorner \), \(\ulcorner \)"pair"\(\urcorner \), \(\ulcorner \)"AFA"\(\urcorner \), with concrete OpSet witnesses; (b) Open realisability in the ZFC reading — \(\ulcorner \)"Conjecture_IV_X_Statement"\(\urcorner \): realisability is mathematically open, mirroring VR-Sets Conjectures IV.1/IV.2 (only isRealisableZFC names these terms; in the operational reading they fall to the catch-all); (c) Provably non-realisable — split into trivially-False (the catch-all: Russell, Vitali, classical \(\mathbb {R}\), classical \(\mathcal{P}(\mathbb {N})\), no set theorem needed) and ZFC-refutable (\(\ulcorner \)"AFA_Statement"\(\urcorner \) via AFA_Refuted, in the ZFC reading only). The term \(\ulcorner \mathrm{AFA}\urcorner \) is the one that changes category with the reading — see Theorem 176.
6.4 Transit (Part III)
\(\texttt{translate\_ pi} : \texttt{FormalTerm} \to \mathrm{Prop}\) is the specific layer (rule (ii) of § III.2): for each named formal term, the defining predicate of the concrete operational set. For \(\ulcorner \)"∅"\(\urcorner \): \(\forall x,\; \lnot \, x \mathrel {\mathtt{Mem}} \texttt{OpSet.empty}\) (not an existential). For \(\ulcorner \)"omega"\(\urcorner \): \(\mathtt{vn}\, 0 \mathrel {\mathtt{Mem}} \texttt{OpSet.omega} \land \ldots \). For \(\ulcorner \)"pair"\(\urcorner \): \(\forall a\, b\, x,\; x \mathrel {\mathtt{Mem}} \texttt{OpSet.pair}\, a\, b \leftrightarrow x \mathrel {\mathtt{Equiv}} a \lor x \mathrel {\mathtt{Equiv}} b\). For \(\ulcorner \)"AFA"\(\urcorner \): \(\forall V\, E,\; \mathtt{IsDecoration}\, E\, (\texttt{OpSet.decorate}\, E)\). Catch-all: False. Contrast with isRealisable (existential layer). Axiom profile: [].
Direct proofs for the four named terms by the SetsOp theorems not_mem_empty, empty_mem_omega with omega_succ_closed, mem_pair, decorate_isDecoration. All on Axiom profile: [].
\(\forall t : \texttt{FormalTerm},\; \texttt{translate\_ pi}(t) \Rightarrow \texttt{isRealisable}(t)\). Proved class by class on Named (translateN_implies_realisableN): in each realisable class the specific predicate names the witness, and existential introduction closes the goal; the catch-all is vacuous. The converse does not hold: from \(\exists \, s,\; \ldots \) one cannot recover the specific named object without Skolemisation — the T\(\to \)O asymmetry (TR-R1). The transit pattern operates exclusively in the forward direction. Axiom profile: [].
6.4.1 The conservativity boundary (Theorem III.1)
Theorem III.1 (preprint § III.2, verbatim): «The theory \(T_1\) (VR-Forms) is conservative over \(T_0\) (VR-Sets) in the operational register: any formula \(\varphi \in L_0\) that is derivable in \(T_1\) is already derivable in \(T_0\). Equivalently: formal terms do not produce new operational theorems.»
Formalised (2026-06) by a deep embedding via relative interpretation, in Forms/Conservativity.lean (propositional floor) and Forms/ConservativityFOL.lean (full FOL). The two-register language \(L_1\) consists of operational atoms and \(0\)-ary formal atoms over de Bruijn terms (variables, constants such as \(\emptyset \), and \(n\)-ary function symbols such as \(t\)); provability is classical Hilbert (K, S, Peirce, MP, \(\forall \)-elim, \(\forall \)-distribution, generalization); the translation \(\pi \) sends each formal atom to its closed operational meaning. The proof is by induction on derivations — \(\pi \) commutes with every rule, and piTr_subst shows \(\pi \) commutes with substitution (kept trivial by \(0\)-ary formal atoms and closed \(\pi \)-images, so no de-Bruijn substitution composition arises). A concrete VR instance (VRExample: \(\emptyset \), \(\in \), \(t\), the formal term \(\ulcorner \emptyset \urcorner \mapsto \forall x\, \lnot (x\in \emptyset )\)) discharges the hypothesis end-to-end (conservativity_empty_concrete).
Comprehension storey (full fidelity to the preprint’s \(\pi \), 2026-06). The FOL floor models formal atoms as \(0\)-ary; the preprint’s \(\pi \) (§ III.2, rule for \(\ulcorner x\in \tau \urcorner \) with \(\tau =\{ y:\psi (y)\} \)) is the genuine comprehension translation \(\pi (\ulcorner x\in \tau \urcorner )=\psi (x)\), which substitutes the argument. This is machine-checked in Forms/ConservativityComprehension.lean: terms and formulas are mutually recursive (\(\mathtt{Tm}\) carries set-builders \(\{ y:\psi \} \)), so \(\pi \) substituting \(\psi (x)\) forces the full de-Bruijn substitution calculus — \(\mathtt{subst\_ lift}\), \(\mathtt{lift\_ lift}\), \(\mathtt{lift\_ subst}\), and the substitution lemma \(\mathtt{subst\_ subst}\). The keystone \(\mathtt{piFml\_ subst}\) (\(\pi \) commutes with substituting a variable) closes precisely via \(\mathtt{subst\_ subst}\) on the comprehension case; conservativity then follows as before, with a non-vacuous instance whose hypothesis is proved (\(\pi \) of a comprehension axiom is the Hilbert theorem \(X\to X\)). This is course A: set-builders occur only as the right member of \(\in \), so the left member of every membership is operational (a variable). A total \(\pi \) unfolding set-builders in every position (course B) is provably ill-defined — it diverges on self-membered formal terms (the Russell term \(\ulcorner \{ x:x\notin x\} \urcorner \) gives \(\pi (\ulcorner R\in R\urcorner )=\lnot \pi (\ulcorner R\in R\urcorner )\), no fixpoint). This is the formal-register counterpart of why VR holds paradoxes safely: they cannot be unfolded into operational theorems — \(\pi \) is simply undefined on them, not defined-and-false.
Axiom profile (2026-09-12 sweep). All three storeys are on Axiom profile: []: the de Bruijn lemmas that had been closed by simp/omega (both reach propext) were re-proved by hand (NatAux, explicit rw [if_pos …]), and the auto-generated injEq lemmas are switched off.
What was the cycle’s one premeditated boundary — a proof-theory project beyond the shallow embedding — is a machine-checked result. Two documented refinements remain, by choice, and are polish rather than gaps in the theorem: gen is stated without the eigenvariable side-condition (it would match standard first-order soundness, but is not needed for the syntactic \(\pi \)-transport that conservativity is), and the worked VR instance covers \(\emptyset \) (richer instances such as \(\omega \) are marginal).
6.5 The ZFC reading and the bridge theorems (Part V)
The bridge file VRClassical/Forms/Bridge.lean keeps the reading VR-Forms had until 2026-09-12: realisability with the operational register taken to be Mathlib’s OSet = ZFSet. It is a second predicate, isRealisableZFC, over the same formal terms; its three positive cases are the ZFC-era witnesses (osetEmpty, omega_OSet, osetPair, Chapter 4), and it alone names the three statements about Mathlib’s universes.
\(\lnot \, \texttt{isRealisableZFC}\, \ulcorner \)"AFA_Statement"\(\urcorner \). Proof: isRealisableZFC reduces definitionally to VR.Sets.AFA_Statement; the theorem is exactly AFA_Refuted from Chapter 4. The cross-cycle chain: PSet.mem_irrefl \(\to \) AFA_Refuted \(\to \) bridge_AFA. This is a statement about Mathlib’s well-founded universe; in the operational universe the same description is realised (Theorem 165, isRealisable_AFA). Axiom profile: [propext, Quot.sound] (Mathlib’s, via ZFSet).
\(\texttt{isRealisableZFC}\, \ulcorner \)"Conjecture_IV_1_Statement"\(\urcorner \leftrightarrow \texttt{Conjecture\_ IV\_ 1\_ Statement}\), and likewise for IV.2. Both iff proofs are \(\langle \texttt{id},\texttt{id}\rangle \) (definitional equality); the mathematical content is open. Status: open realisability (category (b) of the triadic structure), in the ZFC reading.
6.6 Examples and mixed formulas (Parts V–VII)
\(\lnot \, \texttt{isRealisable}\, \ulcorner \)"Russell_class"\(\urcorner \), \(\lnot \, \texttt{isRealisable}\, \ulcorner \)"Vitali"\(\urcorner \), \(\lnot \, \texttt{isRealisable}\, \ulcorner \)"classical_R"\(\urcorner \), \(\lnot \, \texttt{isRealisable}\, \ulcorner \)"classical_powerset_N"\(\urcorner \). All four proofs are id: the closed world of named sends each description to other, hence to False. Non-realisability is metatheoretic (category (c), Level 1): no set theorem is needed. Contrast with bridge_AFA (Level 2: refutable in the ZFC reading). Axiom profile: [].
\(\mathtt{vn}\, 0 \mathrel {\mathtt{Mem}} \texttt{OpSet.omega} \land \texttt{isRealisable}\, \ulcorner \)"omega"\(\urcorner \). Proof: \(\langle \texttt{OpSet.empty\_ mem\_ omega},\, \texttt{isRealisable\_ omega}\rangle \). Both registers affirm \(\omega \): operational membership and formal realisability agree on the same object. Mixed formulas combine operational statements about OpSet with realisability predicates on formal terms — Lean Props at the meta level, not a third register. Axiom profile: [].
\(\texttt{isRealisable}\, \ulcorner \)"AFA"\(\urcorner \land \lnot \, \texttt{isRealisableZFC}\, \ulcorner \)"AFA_Statement"\(\urcorner \). Proof: \(\langle \texttt{isRealisable\_ AFA},\, \texttt{bridge\_ AFA}\rangle \) (afa_two_registers).
Junction theorem of VR-Forms. The formal register’s anti-foundation description has an operational correlate — OpSet.afa: every graph is decorated in the operational universe, since a set is a pointed graph and identity is bisimulation — while its ZFC-register reading is refuted in Mathlib’s well-founded universe (PSet.mem_irrefl \(\to \) AFA_Refuted). Both conjuncts are theorems; they speak of different universes. What Chapter 4 recorded as Boundary B.5 (“ZFA total absence”) is thereby located: it is a boundary of groundedness — IsGrounded is a predicate on the graph, the ZFC-mode (§ 14.4) — not a boundary of operationality. See Observation 9.
6.7 Substrate (Stage 6)
\(\texttt{Carrier}\) is an inductive type with two constructors: \(\texttt{.obj} : \mathrm{OpSet}.\{ 0\} \to \texttt{Carrier}\) (operational objects in the operational register) and \(\texttt{.term} : \texttt{FormalTerm} \to \texttt{Carrier}\) (formal terms).
\(\texttt{Operational} : \texttt{Carrier} \to \mathrm{Prop}\) by: \(\texttt{Operational}(\texttt{.obj}\, a) := a \mathrel {\mathtt{Equiv}} a\) — the substrate of an operational set is the act it is, its revealing functionality, witnessed minimally by the identity bisimulation (the diagonal relation with its two simulation proofs: a construction, not True); \(\texttt{Operational}(\texttt{.term}\, \_ ) := \texttt{True}\) — for a formal term the substrate is the act of inscription (Principle of Forms, § II.4).
Why not well-foundedness. The 2026-05-28 gate chose \(\texttt{Acc}({\cdot }\in {\cdot })\) as the substrate predicate on OSet = ZFSet, where it is total because Mathlib’s universe is well-founded by construction. On OpSet that choice is refuted as a substrate: AFA holds there, so groundedness (IsGrounded) is not total — it is a mode, separately available. The frozen statement («operationality is a total substrate; every operand and every result, including the empty result \(\emptyset \), carries operational substrate») survives with the correct predicate.
\(\texttt{operational\_ total}\): \(\forall c : \texttt{Carrier},\; \texttt{Operational}(c)\). Proof: .obj branch by OpSet.Equiv.refl; .term branch by trivial.
\(\texttt{operational\_ empty}\): \(\texttt{Operational}(\texttt{.obj}\, \texttt{OpSet.empty})\) — the primordial object \(\emptyset \), the limit case the curator insisted on, carries operational substrate.
\(\texttt{omega\_ substrate}\): \(\texttt{Operational}(\texttt{.obj}\, \texttt{OpSet.omega}) \land \texttt{Operational}(\texttt{.term}\, \ulcorner \)"omega"\(\urcorner )\) — \(\omega \) carries substrate in both registers, connecting Stage 6 to mixed_omega_two_register.
Axiom profile: [] for all three.
6.8 Conservativity: from boundary to formalised result (§ IX.2)
VR-Forms Lean originally had one explicit structural boundary (at conservativity), in contrast to VR-Sets Lean’s five mathematical-content boundaries. That boundary has since been closed: conservativity is formalised by a deep embedding (§ 6.4.1).
Theorem III.1 was mathematically proved in the preprint (full inductive proof via \(\pi \)); the shallow embedding deliberately did not formalise it, documenting the boundary in Transit.lean and declining a def Conjecture_Conservativity (which would misrepresent a proved result as open). It is machine-checked by a separate deep embedding (Forms/ConservativityFOL.lean): a classical Hilbert calculus over de Bruijn terms with \(n\)-ary functions and predicates, the \(\pi \)-translation, and conservativity by induction on derivations, with a concrete VR \(\emptyset \) instance — on the empty axiom list. The shallow embedding remains the working layer; the deep embedding stands beside it as the proof.
The original match on description strings had two costs: its catch-all | _ => False did not reduce in term mode for a schematic variable, forcing by_cases discrimination; and the splitter Lean generates for overlapping literal patterns carries propext (measured in the 2026-09-12 sweep). The classifier named (an if-chain over DecidableEq FormalTerm into the finite Named) removes both: every theorem about isRealisable is a case analysis on five constructors, and the module is on [].
isRealisable (existential: \(\exists \) witness) and translate_pi (specific: named concrete object) form two complementary layers connected by translate_implies_realisable via existential introduction. The converse (specific \(\Leftarrow \) existential) is not provable: Skolemisation is unavailable from the existential in the shallow embedding. The transit pattern of § IV.2 operates exclusively in the forward direction — the same asymmetry that governs the apparatus (Chapter 8, T\(\to \)O has no mechanism).
Two levels of non-realisability: Level 1 (trivially False): Russell, Vitali, classical \(\mathbb {R}\), classical \(\mathcal{P}(\mathbb {N})\) — the closed world sends them to False, proof is id, no set theorem needed; this level lives in the core on []. Level 2 (refutable in a reading): \(\ulcorner \)AFA_Statement\(\urcorner \) — isRealisableZFC returns a mathematically formulated Prop; non-realisability requires AFA_Refuted from VR-Sets, and lives in the bridge. The operational reading has no Level 2: every description it names is realised.
The triadic classification of formal terms (provably realisable / open / provably non-realisable) parallels VR-Sets Stage 11’s three-tier formalisation result (proved theorems / refuted claims / open formulations), but localised at the level of formal terms within the formal register. With two readings of the operational register the middle and the refutable tier are exhibited by the ZFC reading; the operational reading has only the first tier and the trivial part of the third.
6.9 Methodological observations (Part IX)
§ IX.1 Foundation-level properties
Language.lean introduces the syntactic skeleton without importing any module at all. Since 2026-09-12 the rest of the core module imports only VR.SetsOp (itself Mathlib-free), and since 2026-09-13 the whole core library imports nothing but Lean. What was true of the base layer in 2026-05 — axiom-free [] — is now true of every declaration of VR-Forms in the core, by the build-time guard.
The realisable cases are exactly as clean as the universe that supplies their witnesses. Over ZFSet they were [propext, Quot.sound] (the Classical-free closure layer of VR-Sets); over OpSet they are []. Nothing in the realisability layer itself introduces an axiom: it names witnesses and reads their defining properties.
§ IX.3 Structural patterns
VR-Forms is a cross-cycle module, and universe inference does not propagate across cycle boundaries without explicit annotation: OpSet.{0} is pinned explicitly in isRealisableN and in Carrier (as OSet.{0} was before), and the witnesses are taken at that universe.
mixed_AFA_two_registers states in a single Lean Prop what the two readings of the operational register say about one formal description: realised in the operational universe, refuted in the well-founded one. What appeared in VR-Sets Part X as Boundary B.5 (“ZFA total absence”) is thus not a limit of operationality but the choice of a mode — IsGrounded, a predicate on the graph, ZFC-mode inside the one universe (Chapter 14). The two-register apparatus is precisely the instrument that lets this be said as a theorem rather than as a remark.
§ IX.4 Cross-cycle integration
The cycle plan predicted [propext, Classical.choice, Quot.sound] or stricter; the 2026-05 result was [propext, Quot.sound] with zero Classical.choice. The 2026-09 result is sharper: every object of VR-Forms that speaks about VR’s own universe is in the core library VR on [], and the two theorems that speak about Mathlib’s universes (bridge_AFA, the Conjecture bridges) together with the junction that compares the two readings are in VRClassical/Forms/ Bridge.lean, at Mathlib’s [propext, Quot.sound] and still without Classical.choice. The perimeter is drawn in code: nothing in the core depends on the bridge.
6.10 Axiom profile
Axiom profile: [] for every public object of the core module (VR/Forms/): the language, the classifier and both realisability layers, all four base lemmas, the transit theorem, the three storeys of conservativity, the four non-realisable terms, the positive mixed formula, and the substrate results. Enforced at build time by VR/Guard.lean.
Axiom profile: [propext, Quot.sound] for the ZFC bridge (VRClassical/Forms/Bridge.lean): isRealisableZFC and its three positive cases, bridge_AFA, the two Conjecture bridges, afa_two_registers and mixed_AFA_two_registers. Zero Classical.choice anywhere in VR-Forms.
Comparison with VR-Sets (Chapter 4): VR-Sets has 6 objects at the full ceiling [propext, Classical.choice, Quot.sound] through four structurally distinct mechanisms (ordinal-valued constructions, definability, foundation, choice). VR-Forms has none, and since the move onto OpSet it has no axiom at all where it speaks for itself; the only axioms left are those of the universe it is compared against.
6.11 References
The preprint for this chapter is VR-Forms, v1.0.1 (23 May 2026).
The Lean 4 formalisation is archived at VR-Forms Lean, v1.0.0 (23 May 2026), git tag v1.3-vr-forms; the move of the operational register onto OpSet and the split into core and bridge are in the repository history of 2026-09-12/13 (CHANGELOG.md).