VR-Numbers: A Lean 4 Formalisation of Parts II–V

This is a Lean 4 formalisation of Parts II–V of the preprint "VR-Numbers:Operational Superstructures of Integers, Rationals, Reals, and ComplexNumbers over the Natural Numbers of VR" (Reznik, 2026; concept DOI10.5281/zenodo.20272743). It extends the formalisation of Part I"VR. A Formal System" (Reznik, 2026; DOI 10.5281/zenodo.20324240). The formalisation constructs four numerical superstructures over VR:- ℤ_VR (Part II): integers as a quotient of formal subtraction expressions- ℚ_VR (Part III): rationals as a quotient of formal division expressions- ℝ_VR (Part IV): reals as Cauchy sequences of ℚ_VR-values- ℂ_VR (Part V): complexes via the A1-duality of VR For each construction, the file proves a structural isomorphism with thecorresponding mathlib type (Int, Rat, Real, Complex), instantiated asexplicit isomorphism records (IntVRIntIso, RatVRRatIso, RealVRRealIso,ComplexVRComplexIso). The formalisation contains approximately 3,600 lines of Lean 4 code acrosssix files, with 206 theorems and definitions. No sorry or admit. Allaxiom dependencies are documented: - Part I (VR.lean): axiom-free- ℤ_VR (Integers.lean): [propext, Quot.sound]- ℚ_VR, ℝ_VR, ℂ_VR (Rationals, Reals, Complex.lean): [propext, Classical.choice, Quot.sound] The boundary between Classical-free and Classical-required formalisationfalls between ℤ and ℚ, reflecting the structural dependency of Lean 4Core's Rat type on Nat.gcd normalisation. This is documented in detailin the source. The formalisation respects all six items of the preprint's §VI.5 listof objects that should not be introduced as ontological primitives(ordered pairs, negative numbers, fractions, reals, complex numbers). Twelve methodological observations from the formalisation are collectedfor inclusion in §VIII of the next preprint version (v1.0.2). GitHub repository: https://github.com/inventor1975/VRCycleGit tag for this release: v1.1-vr-numbers