The preprint (§ IV.1) restricts Cauchy sequences to those with finite algorithmic descriptions. Lean 4 does not distinguish computable from non-computable functions at the type level: the type \(\mathbb {N} \to \mathbb {Q}_{\mathrm{VR}}\) includes all total functions. The operational restriction is a metatheoretic claim, not expressible as a Lean type predicate. The formal isomorphism Theorem_IV_7_RealVR_Real is proved without this restriction; the computable-reals interpretation is the operational reading of the same structure.

The classical-free boundary in VR-Numbers lies between \(\mathbb {Z}_{\mathrm{VR}}\) and \(\mathbb {Q}_{\mathrm{VR}}\):

• \(\mathbb {Z}_{\mathrm{VR}}\) (§ II – § III, objects through Theorem_II_6_IntVR_Int): Axiom profile: [propext, Quot.sound].

• \(\mathbb {Q}_{\mathrm{VR}}\) and all subsequent levels: Axiom profile: [propext, Classical.choice, Quot.sound].

The cause is structural: Lean 4 Core’s Rat.add normalises via Nat.gcd coprimality, whose proof chain depends on Classical.choice. Confirmed via #print axioms Theorem_III_6_RatVR_Rat.

This dependency is in the target type Rat, not in any VR-Numbers proof technique: replacing individual lemmas or tactics cannot remove it. The boundary is a structural fact about how mathlib encodes rational arithmetic, not a defect of the VR construction.

Following § VI.5 of the preprint, the following objects are absent as independent objects: (1) ordered pairs (both IntExpr.mk and RatExpr.mk are formal binary operators accessed via pattern matching only); (2) negative numbers (classes of \(a \ominus b\), not a distinct primitive); (3) fractions (classes of \(a \oslash b\) with \(b \ne 0\)); (4) real numbers (equivalence classes of Cauchy sequences of rationals); (5) complex numbers (pairs of reals, but not primitive pairs—a plain Lean structure whose fields are real components); (6) zero (emerges as the class \([0_{\mathbb {Z}} \oslash 1_{\mathbb {Z}}]\) or as the constant sequence at \(0_{\mathbb {Q}}\), not as a primitive object). Each level is an operational construction of increasing depth over \(\emptyset \).

Transitivity of intEq reduces to right cancellation of vadd: if \(\texttt{vadd}\, a\, c = \texttt{vadd}\, b\, c\) then \(a = b\). This cancellation law (vadd_cancel, private) is proved by induction on \(c\) using P4_succ_inj. The preprint’s “direct verification” conceals this dependency; the formalisation makes it explicit.

T3 (T3_vmul_distrib) gives right distributivity \(a \times (b + c) = a \times b + a \times c\). Left distributivity \((a + b) \times c = a \times c + b \times c\) requires a separate inductive argument (vmul_distrib_right). Its absence from T1–T4 is a formalization finding parallel to Remark O1.

Quot.sound is the only axiom beyond Part I’s axiom-free profile that enters VR-Numbers. It appears at the first quotient construction (IntVR) and is unavoidable: without it, equivalence classes would be distinguishable as terms, destroying the mathematical content of the quotient. Quot.sound is not Classical.choice and does not break computability.

propext appears in \(\mathbb {Z}_{\mathrm{VR}}\) (profile [propext, Quot.sound]) because Lean’s Setoid API uses it internally. It is not invoked as an inference principle in any VR proof; it surfaces as a kernel-level dependency of the quotient infrastructure.

The left-inverse proof (left_inv_int) splits on whether \(\texttt{O\_ inv}(b) \le \texttt{O\_ inv}(a)\) using by_cases. This is a decidable inequality on Nat (via instDecidableNatLe) and does not invoke Classical.choice. The [propext, Quot.sound] profile of Theorem_II_6_IntVR_Int is preserved.

Transitivity of ratEq requires right cancellation in \(\mathbb {Z}\). The standard mathlib lemma mul_right_cancel₀ pulls Classical.choice via the integral domain instance. The private Int_mul_right_cancel avoids this by the route \((a - b) \times c = 0 \Rightarrow \texttt{natAbs}(a - b) \times \texttt{natAbs}(c) = 0 \Rightarrow a = b\), using only core lemmas Int.natAbs_mul, Int.natAbs_eq_zero, Nat.mul_eq_zero, and sub_eq_zero. Profile: [propext, Quot.sound].

Classical.choice in \(\mathbb {Q}_{\mathrm{VR}}\) is inherited from the target type Rat, not introduced by any VR tactic or lemma. Confirmed by #print axioms Rat.add (no mathlib import needed). No rewriting of individual lemmas in VR-Numbers can remove it.

Each isomorphism theorem targets mathlib’s Int, Rat, Real, Complex as destinations, not re-derived structures. VR-Numbers is built on mathlib, not parallel to it. The isomorphisms provide the operational superstructure; mathlib provides the classical substrate.

Neither IntExpr nor RatExpr has named accessor functions corresponding to “first” and “second” components. Lean projections (.1, .2) exist but are not used; all access is via pattern matching. The constructors .mk denote syntactic juxtaposition under a binary operator (\(\ominus \), \(\oslash \)), not ordered-pair structure.

The VR-Numbers hierarchy has three operational depths above \(\emptyset \): depth 1 (IntExpr: formal subtractions of VRObj); depth 2 (RatExpr: formal divisions of \(\mathbb {Z}_{\mathrm{VR}}\)); depth 3 (FundSeqVR: sequences of \(\mathbb {Q}_{\mathrm{VR}}\) values). \(\mathbb {C}_{\mathrm{VR}}\) is depth 3 (a plain structure of two \(\mathbb {R}_{\mathrm{VR}}\) values, no additional quotienting).

The preprint restricts Cauchy sequences in \(\mathbb {R}_{\mathrm{VR}}\) to those with finite algorithmic descriptions (§ IV.1). This restriction cannot be expressed as a Lean 4 type predicate: the type \(\mathbb {N} \to \mathbb {Q}_{\mathrm{VR}}\) includes all total functions. Theorem_IV_7_RealVR_Real proves the structural isomorphism without this restriction. The computable-reals reading is the operational interpretation of the isomorphism, verified at the metatheoretic level.

The two-dimensionality of \(\mathbb {C}_{\mathrm{VR}}\) is carried by its two real components fst, snd, not by posited ordered pairs. The algebraic coupling between the components—the joining rule \(i \otimes i := \ominus 1\)—is an independent postulate encoded in cmul via the term \(\ominus (b \times d)\) in the real part. Without cmul, \(\mathbb {C}_{\mathrm{VR}}\) is two independent copies of \(\mathbb {R}_{\mathrm{VR}}\); cmul makes it a field. The preprint (§ V.9) distinguishes these two contributions explicitly.