VR-Numbers: Operational Superstructures of Integers, Rationals, Reals, and Complex Numbers over the Natural Numbers of VR

Building on VR (an axiom-free reconstruction of arithmetic from two primitive operations ∅, t), VR-Numbers develops ℤ, ℚ, ℝ, ℂ as operational superstructures over VR's natural numbers. Each extension is a formal language of expressions with an equivalence relation and operations; there are no set-theoretic (Kuratowski) ordered pairs — pairing is a syntactic operation, not an object. ℤ is the Grothendieck construction, ℚ the field of fractions, ℝVR is built from Cauchy sequences with a computable modulus of convergence (isomorphic to the field of computable reals, a countable subfield of classical ℝ), and ℂVR is the standard two-component construction over ℝVR with i² = ⊖1. Classical actual infinity is replaced by operational infinity (induction read as universal applicability of an operation, agreeing with actual infinity on arithmetical consequences via VR ≃ first-order PA, while positing no completed totality). This is a constructive/operational foundation in the Bishop–Martin-Löf tradition, not an economical ZF. Version 1. 1. 1 re-synchronises with the parent work VR v1. 1. 1, which removed the propositional implication → (and the principles A1, A2): VR is now pure arithmetic on ∅, t, generating no logic of its own. Accordingly, Part V no longer grounds the two-dimensionality of ℂ in "the duality of A1" — that grounding rested on the now-removed F→F / F→⊤ axes and was an over-claim (i² = ⊖1 was always a separate postulate, so A1 gave a coincidence of count, not a derivation). ℂ is presented as the standard two-component construction. No construction, equivalence, operation, or theorem is altered. Honest boundaries (Part VIII): the Lean companion's axiom profile is not inherited from VR's empty — the superstructures rest on quotient types (propext, Quot. sound), and isomorphism bridges to the standard library (Lean Core's Rat) pull Classical. choice; the operational ℚVR construction itself is choice-free. The machine-checked isomorphism for ℝVR is with the full classical ℝ (the Lean type ℕ→ℚVR contains every total function), so the formalisation certifies more than the operational thesis claims — the restriction to the computable reals is metatheoretic, and the same gap carries to ℂ. Lean 4 companion (Parts II–V): DOI 10. 5281/zenodo. 20352057. Prepared with the assistance of Claude (Anthropic, Opus 4. 8) in the cycle's Variant A architecture; all mathematical content and positions are due to the author, Vitaly Reznik.