8 VR-Apparatus
8.1 Position
VR-Apparatus is the seventh work of the cycle and the methodological meta-work: it formalises the apparatus implicitly used across the six preceding works (VR, VR-Numbers, VR-Sets, VR-Forms, VR-Audit, VR-Sets-ZFA). Structurally it belongs to Layer II (Methodology); the Applications (Layer III) depend on it.
Recognition theme. The apparatus was not invented for this work; it was present throughout the cycle. The formalisation makes it explicit and reusable. Recognition discipline governs the chapter: new abstractions are introduced only where the prior cycle genuinely requires them. Three planned abstractions were explicitly dropped (Generic Register, DirectionalMorphism, ReferenceOperationality for Cauchy sequences) after reconnaissance showed they did not fit.
Architecture in brief. Two apparatus modes (PredicateOperationality, ReferenceOperationality), two transit modes (Mode A, Mode B), InterApparatusMorphism, Factorisable as canonical Mode B witness, and HasSeparabilityStructure as formal domain hypothesis. Five architectural levels. 68 public objects across 12 files.
Axiom profile: []: 40 objects (59%). Axiom profile: [Quot.sound]: 7 objects (10%, new sub-ceiling tier in v1.0.0). Axiom profile: [propext, Quot.sound]: 4 objects. Axiom profile: [propext, Classical.choice, Quot.sound]: 17 objects.
8.2 Architecture
IdentityNature is an inductive type with two constructors:
AsPoint — identity = position in a classical type. Apparatus: predicate-wrapping. A type \(T\) provides the substrate; a predicate \(P : T \to \mathrm{Prop}\) selects the operational sub-collection. Example: IsComputableReal : ℝ → Prop.
AsReference — identity = position in a membership graph. Apparatus: reference semantics. A pre-set type \(Q\) with setoid \([s : \texttt{Setoid}\, Q]\); the quotient \(\texttt{Quotient}\, s\) is the operational type. Example: OSetZFA = Quotient CoPSet.instSetoid.
AsPoint_ne_AsReference: the two constructors are distinct, proved by decide. Axiom profile: [] for both.
IdentityNature is a usage-mode indicator, not a type property. The same type may appear as AsPoint in one context and AsReference in another (numbers are a canonical hybrid).
\(\texttt{PredicateOperationality}\, (T : \mathrm{Type}^*)\, (P : T \to \mathrm{Prop})\) is a class (Prop-valued, no fields) marking that \(T\) with predicate \(P\) is used in the predicate-wrapping apparatus. \(\texttt{identityNature} := \texttt{AsPoint}\). Instances: ℝ with IsComputableReal; FormalTerm with isRealisable; FormalTerm with translate_pi. All marker instances at Axiom profile: [].
\(\texttt{ReferenceOperationality}\, (Q : \mathrm{Type}^*)\, [\texttt{Setoid}\, Q]\) is a class with two fields: membership and ext (extensionality at the quotient level). \(\texttt{identityNature} := \texttt{AsReference}\). Instances: CoPSet with CoPSet.instSetoid (Axiom profile: [propext, Classical.choice, Quot.sound], M-type); PSet with PSet.setoid (Axiom profile: [propext, Quot.sound], inductive — lighter).
The apparatus is organised in five tiers:
Tier 1 (Apparatus instances): PredicateOperationality and ReferenceOperationality markers.
Tier 2 (Domain structures): HasSeparabilityStructure (formal domain hypothesis; see § 8.4).
Tier 3 (Morphism levels): Mode A (endomorphisms at quotient level, intra-apparatus) and InterApparatusMorphism (congruence at representative level, inter-apparatus).
Tier 4 (Conditional extraction): Mode B with IsModeBOp and Factorisable as canonical witness.
Tier 5 (Cross-cycle recognition): VR-Forms transit as Mode B; Numbers as hybrid apparatus subjects.
8.3 Mode A (Part III)
\(\texttt{IsModeAOp}\, f := \forall x,\; P\, x \Rightarrow P\, (f\, x)\). \(\texttt{IsModeAOp₂}\, f := \forall x\, y,\; P\, x \to P\, y \to P\, (f\, x\, y)\). \(\texttt{modeA\_ liftFn}\): lifts \(f\) to \(\{ x \mid P\, x\} \to \{ x \mid P\, x\} \). \(\texttt{modeA\_ lift}\) (@[simp]): \(\texttt{modeA\_ liftFn}\, f\, \langle x, h\rangle = \langle f\, x, \ldots \rangle \). Composition: \(\texttt{IsModeAOp.compose}\) — Mode A is closed under composition. All seven objects at Axiom profile: [].
\(\texttt{IsModeAOp}\, f := \forall a\, b,\; a \approx b \Rightarrow f\, a = f\, b\) (where \(f : Q \to \texttt{Quotient}\, s\)). \(\texttt{modeA\_ liftFn}\): Quotient.lift f hf: lifts to \(\texttt{Quotient}\, s \to \texttt{Quotient}\, s\). Composition: Mode A is closed under composition. Axiom profile: [] for all four.
Addition of computable reals is Mode A (isComputableReal_add_isModeA). OSetZFA singleton is Mode A (osetZFA_singleton_isModeA). Negation, subtraction of computable reals; empty set in OSetZFA. All concrete instances at Axiom profile: [propext, Classical.choice, Quot.sound].
Neither IsModeAOp definition requires the other apparatus class in its signature. Mode A is apparatus-structure-independent: the same predicate-level definition applies uniformly to predicate and reference apparatus, with parallel structures and parallel proofs.
8.4 Mode B and Factorisable (Part IV)
\(\texttt{IsModeBOp}\, PA\, PB\, W\, f := \forall a,\; PA\, a \to W\, a \to PB\, (f\, a)\). Parameters: \(PA : A \to \mathrm{Prop}\) (operand predicate), \(PB : B \to \mathrm{Prop}\) (result predicate), \(W : A \to \mathrm{Prop}\) (witness: why extraction works for this operand), \(f : A \to B\) (possibly classical operation).
Mode A is Mode B with \(W = \texttt{fun}\, \_ \Rightarrow \texttt{True}\): \(\texttt{IsModeAOp\_ iff\_ IsModeBOp}\). IsModeBOp.compose: Mode B is closed under composition. \(\texttt{lift}\), \(\texttt{lift\_ val}\): lifts \(f\) to subtypes. All six core objects at Axiom profile: [].
\(\texttt{Factorisable}\, PA\, PB\, f\, a := \exists g : \{ x \mid PA\, x\} \to \{ x \mid PB\, x\} ,\; g\, \langle a, h \rangle = \langle f\, a, \ldots \rangle \).
\(\texttt{operand\_ determines\_ operational}\): operationality of \(f\, a\) is determined by the operand \(a\), not by the operation \(f\).
\(\texttt{factorisable\_ implies\_ isModeBOp}\): every Factorisable witness gives a Mode B operation.
\(\texttt{IsModeBOp\_ of\_ factorisable}\): converse (requires choice in general).
All six core objects at Axiom profile: [].
\(\texttt{HasSeparabilityStructure}\, (T : \mathrm{Type}^*)\, [\texttt{TopologicalSpace}\, T]\) is a typeclass with a single field: a dense sequence denseSeq : ℕ → T with dense range.
\(\texttt{instHasSepStructOfOpHilbert}\): any OperationalHilbertSpace is a HasSeparabilityStructure (the denseSeq field provides the separability witness).
\(\texttt{separability\_ provides\_ factorisable}\): from separability structure, a Factorisable witness can be extracted for the Riesz extension. Axiom profile: [] for the class and the factorisable lemma; Axiom profile: [propext, Classical.choice, Quot.sound] for the instance.
\(\texttt{riesz\_ extension\_ map}\): the Riesz extension map \(f \mapsto g = \texttt{innerSL}\, \mathbb {R}\, (\xi : E)\). \(\texttt{riesz\_ extension\_ isModeBOp}\): the Riesz extension is a Mode B operation with \(W = \texttt{fun}\, \_ \Rightarrow \texttt{True}\). \(\texttt{riesz\_ extension\_ factorisable}\): with \(W = \texttt{Factorisable}\) (stronger, explicit structural reason). \(\texttt{riesz\_ mode\_ b\_ lift}\): the lifted subtype map. All five at Axiom profile: [propext, Classical.choice, Quot.sound].
8.5 Apparatus instances and morphisms (Part V)
\(\texttt{InterApparatusMorphism}\, f\) (where \(f : Q_1 \to Q_2\)): \(\forall a\, b,\; a \approx _1 b \Rightarrow f\, a \approx _2 f\, b\).
Operates at the representative level (not quotient level); lifts to \(\texttt{Quotient}\, s_1 \to \texttt{Quotient}\, s_2\) via \(\texttt{lift}\) (Axiom profile: [Quot.sound]).
Canonical instance: \(\texttt{embedPSet\_ isInterApparatus}\) (\(\texttt{embedPSet} : \texttt{PSet} \to \texttt{CoPSet}\), crossing from ZFC apparatus to ZFA apparatus). \(\texttt{embedOSet\_ eq\_ interApparatus\_ lift}\): \(\texttt{embedOSet}\) equals the IAM lift.
One-way bridge: same-setoid IAM \(\Rightarrow \) Mode A (IsModeAOp_of_interApparatus); the converse does not hold (type mismatch: Mode A targets quotients, IAM targets representatives).
\(\texttt{instPredicateOpFormalTerm}\): FormalTerm with isRealisable is a predicate-wrapping apparatus instance (AsPoint). \(\texttt{instPredicateOpTranslatePi}\): FormalTerm with translate_pi is a predicate-wrapping apparatus instance (AsPoint). \(\texttt{vr\_ forms\_ transit\_ isModeBOp}\): the VR-Forms transit (translate_implies_realisable) is a Mode B operation with \(PA = \texttt{translate\_ pi}\), \(PB = \texttt{isRealisable}\), \(W = \texttt{True}\), \(f = \texttt{id}\). This is the recognition finding of VR-Apparatus Stage 1: the Mode B schema from v0.1.0 already captured VR-Forms transit without extension.
\(\texttt{cauchy\_ abs\_ isQuotient}\): \(\mathbb {R} \simeq \texttt{Quotient CauSeq.equiv}\) (Cauchy completion as quotient). \(\texttt{real\_ cauchy\_ bridge}\): bridge \(\mathbb {R} \simeq \texttt{Cauchy abs}\). \(\texttt{natEqSetoid}\): discrete setoid on \(\mathbb {N}\) (equality). \(\texttt{nat\_ vonNeumann\_ isInterApparatus}\): PSet.ofNat : ℕ → PSet is an IAM from \((\mathbb {N}, =)\) to \((\texttt{PSet}, \texttt{PSet.Equiv})\).
\(\mathbb {R}\) with predicate lens (IsComputableReal) is natural. \(\mathbb {R}\) with reference lens (Cauchy) is artificial: Cauchy sequences carry no natural membership relation; ReferenceOperationality instance is NOT constructed (methodological honesty). \(\mathbb {N}\) with reference lens (von Neumann ordinals) is natural: ordinals ARE sets with membership.
8.6 Compositional algebra and twelve findings
The four morphism levels are closed under identity: predicate Mode A identity (Axiom profile: []), reference Mode A identity via Quotient.mk (Axiom profile: [Quot.sound]), IAM identity (Axiom profile: []), Mode B identity (Axiom profile: []). Cross-level: IAM composed with Mode A lifts correctly (Axiom profile: [Quot.sound]).
The twelve findings that emerged during implementation are catalogued below. They are labeled by the stage in which they were discovered (S = Stage of the v1.0.0 implementation).
The witness \(W\) in \(\texttt{IsModeBOp}\) is \(\texttt{Factorisable}\, PA\, PB\, f\, a\): existence of an operational function \(g\) matching \(f\) on the specific operand \(a\). Operationality of the result \(f\, a\) is determined by the operand \(a\), not by the classical operation \(f\). This localises the Mode B witness to the operand, not the operation.
Factorisable witnesses are computability-like conditions: existence of a computable \(g\) matching \(f\) on the operand. Mode B with Factorisable is strictly stronger than plain \(\texttt{IsModeBOp}\): every Factorisable gives Mode B; the converse requires Choice in general. The spectrum of witnesses (minimal \(W = \texttt{True}\); canonical \(W = \texttt{Factorisable}\)) is a feature, not a gap.
HasSeparabilityStructure provides, via separability_provides_factorisable, a Factorisable witness for the Riesz extension. Domain-specific structure (separability) flows into the apparatus as a formal hypothesis, not as a classical axiom. This is the Tier 2 \(\to \) Tier 3 connection in the five-tier architecture.
Mode A (quotient level, intra-apparatus endomorphisms) and InterApparatusMorphism (representative level, inter-apparatus) are distinct levels, not a subset hierarchy. IsModeAOp_of_interApparatus is a one-way bridge (same-setoid IAM \(\Rightarrow \) Mode A after post-composition with Quotient.mk); Mode A operations cannot be directly read as IAMs (type mismatch). The type system enforces the layering.
IAM lift infrastructure uses only Quot.sound: \(\texttt{lift\_ mk}\) and its consequences sit at Axiom profile: [Quot.sound], strictly between axiom-free and [propext, Quot.sound]. IAM lift needs Quotient.sound to identify quotient representatives but neither propext (no iff-to-eq reasoning) nor Classical.choice. This sub-ceiling tier is absent from v0.1.0 and is a new discovery of v1.0.0.
The apparatus framework has two structurally distinct tracks (predicate track: Type with predicate; reference track: quotient of pre-sets) that do not naturally compose cross-track. This is not an oversight: it reflects the genuine structural asymmetry between predicate-selecting and setoid-quotienting. Cross-track composition requires additional structure (a predicate tracking setoid equivalence classes).
ReferenceOperationality.IsModeAOp requires \(f : Q \to \texttt{Quotient}\, s\) where the target quotient uses the same setoid \(s\) as the source. Cross-apparatus endomorphisms (\(s_1 \ne s_2\)) cannot use IsModeAOp; they are handled as raw propositions in composition theorems. The type system makes this constraint explicit.
Identity elements for all four morphism levels are proved by trivially-simple proofs (fun _ hx => hx, etc.). The accumulation of identity and composition instances IS the mathematical content: it demonstrates the apparatus framework is closed under identity and composition. Simplicity of proof is not weakness but witness to the framework’s coherence.
The two apparatus lenses are not uniformly applicable. \(\mathbb {R}\) with IsComputableReal (predicate lens): natural. \(\mathbb {R}\) with Cauchy reference lens: artificial (Cauchy sequences carry no natural membership relation; instance not constructed). \(\mathbb {N}\) with von Neumann ordinals (reference lens): natural (ordinals ARE sets with membership). Apparatus framework does not force uniform applicability; methodological honesty wins.
Analysis track (\(\mathbb {R}\), Cauchy): even trivially-proved objects inherit standard ceiling [propext, Classical.choice, Quot.sound] through type elaboration of \(\texttt{Field}\, \mathbb {Q}\) / \(\texttt{IsAbsoluteValue}\). Set-theory track (\(\mathbb {N}\), \(\texttt{PSet}\)): axiom-free throughout. The asymmetry mirrors the general pattern: analysis-based apparatus (ceiling); set-theoretic apparatus (constructive).
The planned generic Register structure and DirectionalMorphism typeclass were dropped after reconnaissance: (a) VR-Forms already has Register as a two-constructor mode-of-consideration marker; (b) DirectionalMorphism type-mismatches VR-Forms transit (predicate implication \(\ne \) morphism between setoid types); (c) translate_implies_realisable IS Mode B with \(W = \texttt{True}\). Stage 1 of v1.0.0 = recognition that the v0.1.0 apparatus already captures VR-Forms transit without extension.
VR-Forms apparatus anatomy: (a) instPredicateOpTranslatePi (AsPoint, specific predicate); (b) instPredicateOpFormalTerm (AsPoint, existential predicate); (c) instRefOpPSet (AsReference, operational register). Two predicate-wrapping instances for the formal register; one reference- semantics instance for the operational register. The Mode B transit (vr_forms_transit_isModeBOp) connects (a) \(\to \) (b). Realisability says (b) has an operational correlate in (c).
8.7 Position relative to existing frameworks (Part VII)
Mode B is conceptually adjacent to proof mining (Kohlenbach 2008): both extract operational/computable content from classical proofs. Proof mining uses the Dialectica interpretation and explicit bounds; Mode B uses the witness \(W\) and Factorisable. The Riesz extension is an example where both approaches reach the same conclusion. VR-Apparatus does not claim to subsume proof mining: the logical machinery differs.
Bishop rejects classical mathematics; VR-Forms places it in the formal register as a conservative extension. These are different strategies. Mode B is not Bishop’s approach: it does not reconstruct classical proofs constructively; it extracts operational content from classical objects by working with the operand’s structure.
IsComputableReal follows the Pour-El & Richards 1989 formulation. The Weihrauch framework classifies classical theorems by degree; VR-Apparatus classifies the operational extractability of their instances. Both approaches overlap on computability of analysis results; they differ in logical framework (oracle Turing machines vs. Lean type-theoretic predicates).
Reverse mathematics locates theorems in subsystem hierarchies (WKL\(_0\), ACA\(_0\), …). VR-Apparatus performs an axiom profile audit that is structurally related: it locates each object in a four-tier axiom hierarchy. The goals differ: reverse mathematics asks what is needed to prove a theorem; VR-Apparatus asks what axioms a proof term inherits from its environment.
8.8 Honest scope limitations
ReferenceOperationality.IsModeAOp handles endomorphisms only (\(f : Q \to \texttt{Quotient}\, s\), same setoid). Cross-apparatus maps (\(\texttt{PSet} \to \texttt{CoPSet}\), inducing \(\texttt{ZFSet} \to \texttt{OSetZFA}\)) are handled via IAM, which operates at the representative level, not the quotient level. A cross-apparatus quotient morphism concept remains future work.
Mode B (predicate track, Tier 4) and IAM (reference track, Tier 3) cannot be composed without additional structure. This is a genuine architectural boundary, not an implementation gap. Three structural non-composabilities are documented in Composition.lean.
Cauchy sequences carry no natural membership relation. The reference lens for \(\mathbb {R}\) is not constructed; the bridge \(\mathbb {R} \simeq \texttt{Cauchy abs}\) is documented as a carrier without a ReferenceOperationality instance. Forcing synthetic membership would violate methodological honesty.
8.9 Axiom profile
68 public objects (35 from v0.1.0, 33 new in v1.0.0).
Axiom profile: []: 40 objects (59%). Core abstract structure (IdentityNature, apparatus marker classes, all Mode A and Mode B definitions, Factorisable core, IAM definition and composition).
Axiom profile: [Quot.sound]: 7 objects (10%, new tier in v1.0.0). IAM lift infrastructure: InterApparatusMorphism.lift, lift_mk, IsModeAOp_of_interApparatus, lift_compose, and three composition identity lemmas. IAM lift needs Quot.sound (to identify representatives) but not propext or Classical.choice. This tier is Finding S2-B.
Axiom profile: [propext, Quot.sound]: 4 objects. VR-Forms integration instances (instPredicateOpFormalTerm, instPredicateOpTranslatePi) and ZFC reference apparatus (instRefOpPSet).
Axiom profile: [propext, Classical.choice, Quot.sound]: 17 objects. Concrete Riesz instances, analysis-based Mode A instances, CoPSet instance.
Axiom asymmetry (Finding S5-B): set-theory track is constructive; analysis track inherits classical ceiling through type elaboration.
8.10 References
The preprint for this chapter is VR-Apparatus, v1.0.0 (25 May 2026).
The Lean 4 formalisation is archived at VR-Apparatus Lean, v1.0.0 (25 May 2026), git tag v1.7-vr-apparatus-1.0.0.