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.