VR-Apparatus: A Machine-Verified Apparatus for the Operational Methodology of the VR Cycle

Preprint accompanying the Lean 4 formalisation of VR-Apparatus (DOI 10.5281/zenodo.20380344), the seventh work in the VR Cycle. Meta-work formalising the methodological apparatus used implicitly through the prior six works (VR, VR-Numbers, VR-Sets, VR-Forms, VR-Audit, VR-Sets-ZFA). The apparatus introduces two apparatus typeclasses (PredicateOperationality, ReferenceOperationality) distinguishing predicate-wrapping from reference semantics, two transit modes (Mode A for operations within the operational register, Mode B for classical operations yielding operational results), and a five-tier layered architecture organising the methodology. Contents:- Part I — Position: meta-work scope, recognition theme, architectural summary- Part II — Architecture: two apparatus modes, IdentityNature, five-tier layered structure- Part III — Mode A: closure theorem, productive triviality, apparatus-structure-independence, composition, two variants- Part IV — Mode B: schema, Factorisable canonical witness, spectrum of witnesses, self-witnessing, two-level Factorisable, Riesz instance- Part V — Apparatus instances and morphisms: predicate-wrapping instances, reference semantics instances, InterApparatusMorphism, VR-Forms integration, numbers as hybrid- Part VI — Compositional algebra and findings: two parallel tracks, composition rules, axiom asymmetry, twelve findings catalogued- Part VII — Position relative to existing frameworks: proof mining, constructive analysis, computable analysis, reverse mathematics Twelve methodological findings catalogued: two parallel tracks (predicate, reference), layered structure (quotient vs representative levels), sub-ceiling [Quot.sound] tier, operand-not-operation theorem, spectrum of witnesses, self-witnessing, two-level Factorisable, lens applicability depends on natural structure, axiom asymmetry between tracks, endomorphism constraint type-enforced, generic Register abstraction unnecessary, three-way identity nature contrast. Three honest scope limitations documented: no ReferenceOperationality for Cauchy sequences (no natural membership), no DirectionalMorphism (Mode B captures asymmetry), no generic Register structure (Lean typeclass system already provides it implicitly). Companion to Lean 4 formalisation: DOI 10.5281/zenodo.20380344. Source repository: https://github.com/inventor1975/VRCycle, tag v1.7-vr-apparatus-1.0.0. Seventh work in the VR Cycle. Developed using Claude Opus 4.7 (architectural review) and Claude Sonnet 4.6 (Lean implementation), Variant A.